Merge branch 'feature/publis-e-acsl-vortex' into 'master'

2 new E-ACSL publis

See merge request pub.frama-c.com!125

_fc-publications/e-acsl/2021-vmcai-vjks.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: http://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.

_fc-publications/e-acsl/2021-vortex-s.md

+---
+plugin: "e-acsl"
+authors: "Julien Signoles"
+title: " The E-ACSL Perspective on Runtime Assertion Checking"
+book: "International Workshop on Verification and mOnitoring at Runtime EXecution (VORTEX)"
+link: http://julien.signoles.free.fr/publis/2021_vortex.pdf
+year: 2021
+category: other
+---
+
+Runtime Assertion Checking (RAC) is the discipline of verifying program
+assertions at runtime, i.e. when executing the code. Nowadays, RAC usually
+relies on Behavioral Interface Specification Languages (BISL) à la Eiffel for
+writing powerful code specifications. Since now more than 20 years, several
+works have studied RAC. Most of them have focused on BISL. Some others have also
+considered combinations of RAC with others techniques, e.g. deductive
+verification (DV). Very few tackle RAC as a verification technique that soundly
+generates efficient code from formal annotations. Here, we revisit these three
+RAC's research areas by emphasizing the works done in E-ACSL, which is both a
+BISL and a RAC tool for C code. We also compare it to others languages and
+tools.