Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
pub
Colibri WebSite
Commits
5778ffb2
Commit
5778ffb2
authored
Jul 13, 2021
by
Julien Signoles
Browse files
[publis] 2 new E-ACSL publis
parent
29605cac
Changes
2
Hide whitespace changes
Inline
Side-by-side
_fc-publications/e-acsl/2021-vmcai.md
0 → 100644
View file @
5778ffb2
---
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.
_fc-publications/e-acsl/2021-vortex-s.md
0 → 100644
View file @
5778ffb2
---
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.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment