Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 17:00 - 17:15 at VMCAI - Abstract Interpretation Chair(s): Xavier Rival

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 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30: Abstract InterpretationVMCAI at VMCAI
Chair(s): Xavier RivalINRIA/CNRS/ENS Paris
17:00 - 17:15
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
Franck VédrineCEA LIST, Maxime JacqueminCEA LIST, France, Nikolai KosmatovThales Research and Technology, Julien SignolesCEA LIST
Media Attached
17:15 - 17:30
Twinning automata and regular expressions for string static analysis
Luca NegriniCa’ Foscari University of Venice, Julia S.r.l., Vincenzo ArceriCa’ Foscari University of Venice, Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Agostino CortesiUniversità Ca' Foscari Venezia
Media Attached