Runtime Abstract Interpretation for Numerical Accuracy and Robustness
Verification of numerical accuracy properties in modern software remains an important and challenging task. One of its difficulties is related to unstable tests, where the execution can take different branches for real and floating-point numbers. This paper presents a new verification technique for numerical properties, named Runtime Abstract Interpretation (RAI), that, given an annotated source code, embeds into it an abstract analyzer in order to analyze the program behavior at runtime. RAI is a hybrid technique combining abstract interpretation and runtime verification that aims at being sound as the former while taking benefit from the concrete run to gain greater precision from the latter when necessary. It solves the problem of unstable tests by surrounding an unstable test by two carefully defined program points, forming a so-called split-merge section, for which it separately analyzes different executions and merges the computed domains at the end of the section. The implementation of this technique relies on two basic tools, FLDCompiler, that performs a source-to-source transformation of the given program and defines the split-merge sections, and an instrumentation library FLDLib that provides necessary primitives to explore relevant (partial) executions of each section and propagate accuracy properties. Initial experiments show that the proposed technique can efficiently and soundly analyze numerical accuracy for industrial programs on thin numerical scenarios.
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
17:00 - 17:30
|Runtime Abstract Interpretation for Numerical Accuracy and Robustness|
Franck Védrine CEA LIST, Maxime Jacquemin CEA LIST, France, Nikolai Kosmatov Thales Research and Technology, Julien Signoles CEA LISTMedia Attached
|Twinning automata and regular expressions for string static analysis|
Luca Negrini Ca’ Foscari University of Venice, Julia S.r.l., Vincenzo Arceri Ca’ Foscari University of Venice, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari VeneziaMedia Attached