2021-vmcai-vjks.md 1.84 KB
Newer Older
Julien Signoles's avatar
Julien Signoles committed
1
2
3
4
5
---
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)"
Julien Signoles's avatar
Julien Signoles committed
6
link: http://julien.signoles.free.fr/publis/2021_vmcai.pdf
Julien Signoles's avatar
Julien Signoles committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
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.