2012-01-28 Verification day
- 1 Program
- 1.1 Julien Henry: Big steps for static analysis
- 1.2 David Monniaux: A short tutorial on policy iteration
- 1.3 Thao Dang: Reachability analysis for polynomial dynamical systems using the Bernstein expansion
- 1.4 Marie-Laure Potet: Les besoins pour l'analyse de vulnérabilités
- 1.5 Laurent Mounier: Analyse de teinte sur du code binaire
- 1.6 Radu Iosif: Acceleration Techniques for Program Verification
- 1.7 Nicolas Halbwachs: When the decreasing sequence fails
Julien Henry: Big steps for static analysis
Static analysis by abstract interpretation traditionally follows the control-flow graph of the programs, with one inductive invariant being computed for every control node, computed by forward (or backward) propagation along control edges. One weakness of such an approach is that it enforces that the invariants at all nodes belong to the set of abstractions chosen; for instance, if one uses convex polyhedra, it enforces that all invariants are convex, thus conditions such as |x|≥1 cannot be represented, which may lead to imprecision and spurious warnings. We instead take big steps in the control graph, using SMT-solving to enumerate paths as needed (an explicit enumeration would lead to exponential blowup). We propose, in addition to the basic path-focused analysis some variant iteration scheme based on guided static analysis, and another for disjunctive invariants.
Joint work with Laure Gonnord, Julien Henry and Matthieu Moy.
David Monniaux: A short tutorial on policy iteration
Thao Dang: Reachability analysis for polynomial dynamical systems using the Bernstein expansion
This paper is concerned with the reachability computation problem for polynomial discrete-time dynamical systems. Such computations constitute a crucial component in algorithmic verification tools for hybrid systems and embedded software with polynomial dynamics, which have found applications in many engineering domains. We describe two methods for over-approximating the reachable sets of such systems; these methods are based on a combination of the Bernstein expansion of polynomial functions and a representation of reachable sets by template polyhedra. Using a prototype implementation, the performance of the methods was demonstrated on a number of examples of control systems and biological systems.
Marie-Laure Potet: Les besoins pour l'analyse de vulnérabilités
Nous présentons nos travaux en cours dans le cadre de l'analyse de code vulnérable, en insistant notamment sur :
- les particularités de ce type d'analyse : code binaire, modèle mémoire ad hoc
- les conséquences sur les techniques d'analyse à utiliser ou développer
Laurent Mounier: Analyse de teinte sur du code binaire
(~ 20 minutes)
Nous présentons un exemple concret d'analyse développée pour la recherche de vulnérabilités : l'analyse de teinte.
Radu Iosif: Acceleration Techniques for Program Verification
By acceleration we understand the class of techniques based on a precise computation of the transitive closure of (a part of) the transition relation of the program. In the first part of this talk we show how acceleration can be combined with interpolation to generate inductive interpolants which are crucial in abstraction refinement. This combined method applies to sequential non-recursive programs. In the second part of this talk, we show how acceleration can be applied, in a modular fashion, to recursive program schemes. The result is a Newtonian underapproximation sequence that converges to the tuple of summary relations of all procedures in the program. We also define a class of programs for which our method is shown to be complete i.e. terminate with the precise result.
Joint work with EPFL (Lausanne), IMDEA (Madrid), FIT BUT (Brno)
Nicolas Halbwachs: When the decreasing sequence fails
The classical method for program analysis by abstract interpretation consists in computing an increasing sequence with widening, which converges towards a correct solution, then computing a decreasing sequence of correct solutions without widening. It is generally admitted that, when the decreasing sequence reaches a fixpoint, it cannot be improved further. As a consequence, all efforts for improving the precision of an analysis have been devoted to improving the limit of the increasing sequence. In this paper, we propose a method to improve a fixpoint after its computation. The method consists in projecting the solution onto well-chosen components and to start again increasing and decreasing sequences from the result of the projection.