salle A. Turing CE4
10 septembre 2015 - 14h00
Combinations of Static and Dynamic Analyses in Frama-C: An Overview
par Julien Signoles Nikolai Kosmatov de CEA6LIST
Abstract: Initially considered as orthogonal research fields, static and dynamic
analysis techniques have been for a long time used separately to improve
the quality of software. However, the development of both approaches
has lead to the discovery of common issues and to the realization of
potential synergies. The present talk gives an overview of
combinations between static and dynamic verification approaches that
were realized in the context of Frama-C, a framework for
analysis of C programs developed at CEA LIST.
First, we illustrate how static analysis can be used to help test
generation. The SANTE tool takes advantage of abstract interpretation
and program slicing in order to achieve more precise detection of
runtime errors.
Then we show how the LTEST tool optimizes automatic test generation
through the detection of infeasible test objectives using abstract interpretation
and weakest precondition calculus.
Next, we illustrate how test generation can in turn help static
analysis. We explore in the StaDy tool how program proof and test
generation can be combined in order to help the validation engineer to
understand and to fix proof failures during deductive verification of
programs.
Finally, we show how runtime verification can take benefit of static
analysis in order to avoid the monitoring of irrelevant variables and
statements (E-ACSL tool).
