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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

17:00 - 17:30
Abstract InterpretationVMCAI at VMCAI
Chair(s): Xavier Rival INRIA/CNRS/ENS Paris
17:00
15m
Talk
Runtime Abstract Interpretation for Numerical Accuracy and Robustness
VMCAI
Franck Védrine CEA LIST, Maxime Jacquemin CEA LIST, France, Nikolai Kosmatov Thales Research and Technology, Julien Signoles CEA LIST
Media Attached
17:15
15m
Talk
Twinning automata and regular expressions for string static analysis
VMCAI
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 Venezia
Media Attached