Seminar details

Abstract: Jury
- Andreas Podelski Professeur, Université de Freiburg Rapporteur
- Antoine Miné Professeur, Sorbonne Université Rapporteur
- Cesare Tinelli Professeur, University of Iowa Examinateur
- Corinne Ancourt Maître de recherche, Mines ParisTech Examinatrice
- Olivier Bouissou Ingénieur, Mathworks Examinateur
- Susanne Graf Directrice de recherche, CNRS Examinatrice
- Nicolas Halbwachs Directeur de recherche, CNRS Directeur de thèse
Abstract
Any software bug in safety-critical systems can have catastrophic consequences.
The validation and analysis of programs in critical systems is of paramount importance to guarantee
that the software satisfies its specification and that it is devoided of runtime errors. Static program
analysis by abstract interpretation computes a sound approximation of the set of reachable states of a
program. It discovers invariant properties of programs which are represented by elements of an abstract
domain. Most industrial static analysis tools do not use expressive relational numerical abstract domains
like convex polyhedra due to their computational cost.
We propose a new modular analysis for the automatic discovery of numerical properties based on the
computation of disjunctive relational summaries of procedures. Procedure summaries are computed once and
for all, and used to compute the effect of procedure calls, in a bottom-up fashion. Our approach is
especially applied to improve the scalability of Linear Relation Analysis, or abstract interpretation
with convex polyhedra. Disjunctive relational summaries are finite sets of abstract input-output relations
represented by elements of a relational abstract domain. They are computed based on a partitioning of
procedure preconditions.
We give heuristics to compute an abstract partition of a procedure precondition. We also give ways to
improve the precision of summary computation, notably through a careful treatment of preconditions during
analysis. Our approach also applies to recursive procedures where summaries are computed recursively in
terms of themselves.
We implemented our approach in a new static analysis platform for C programs called mars. We conducted
experiments on programs from the Mälardalen benchmark showing that our approach can significantly reduce
the analysis time for Linear Relation Analysis compared to a full context-sensitive analysis where
procedures are analyzed completely in each call context. Analysis precision is not significantly damaged
and can even be improved due to the use of disjunction.
In a second part, we present an approach for the modular analysis of reactive systems for numerical
properties. We propose a flexible representation of the behavior of reactive components called
Relational Mode Automata (RMA), which allows the analysis of reactive systems behavior at various levels
of abstraction. RMA can be constructed automatically from disjunctive summaries of the procedures implementing component reactions. The analysis results of individual components using RMA can be reused to
analyze larger reactive systems with multiple component instantiations in a modular way. We give an
application of this approach to the analysis of a simplified automated subway control system.