From 5778ffb2ae0ae6f0c957a1f13df405fc46b4ce3b Mon Sep 17 00:00:00 2001 From: Julien Signoles <julien.signoles@cea.fr> Date: Tue, 13 Jul 2021 11:08:54 +0200 Subject: [PATCH] [publis] 2 new E-ACSL publis --- _fc-publications/e-acsl/2021-vmcai.md | 30 ++++++++++++++++++++++++ _fc-publications/e-acsl/2021-vortex-s.md | 21 +++++++++++++++++ 2 files changed, 51 insertions(+) create mode 100644 _fc-publications/e-acsl/2021-vmcai.md create mode 100644 _fc-publications/e-acsl/2021-vortex-s.md diff --git a/_fc-publications/e-acsl/2021-vmcai.md b/_fc-publications/e-acsl/2021-vmcai.md new file mode 100644 index 00000000..b5838b1d --- /dev/null +++ b/_fc-publications/e-acsl/2021-vmcai.md @@ -0,0 +1,30 @@ +--- +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. diff --git a/_fc-publications/e-acsl/2021-vortex-s.md b/_fc-publications/e-acsl/2021-vortex-s.md new file mode 100644 index 00000000..ed9328ce --- /dev/null +++ b/_fc-publications/e-acsl/2021-vortex-s.md @@ -0,0 +1,21 @@ +--- +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: https://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. -- GitLab