2 new E-ACSL publis

_fc-publications/e-acsl/2021-vmcai.md

+---
+plugin: "e-acsl"
+authors: "Franck Védrine, Maxime Jacquemin, Nikolai Kosmatov, and Julien Signoles"
+title: " Runtime abstract interpretation for numerical accuracy and robustness."
+book: "International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)"
+link: https://julien.signoles.free.fr/publis/2021_vmcai.pdf
+year: 2021
+category: other
+---
+
+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 un- stable 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 imple-
+mentation 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.