Accelerated Abstract Lattices

Advisors : Jérôme Leroux & Grégoire Sutre

Telephone : 05 40 00 35 09 & 05 40 00 33 36

e-mail : {Jerome.Leroux, Gregoire.Sutre}@labri.fr

Team : Formal Methods

Group : Modeling and Verification

 

Keywords : verification, data-flow analysis, infinite-state systems, symbolic representations, acceleration, abstract interpretation

 

Scientific context :

System verification often reduces to the effective computation of the reachability set. In general, this set is infinite since the system variables take values in an infinite domain (integers, clocks, queue channels, and so on). Nevertheless, infinite sets can be effectively manipulated by symbolic representations. For instance, sets of integer vectors can be manipulated either by linear constraints [CH-POPL78] or by arithmetic automata [BW-ICALP02].

Actually, there exists two families of verification methods based on symbolic computations : the ones based on exact computations and the other ones based on abstract refinements. These two families are complementary. The first ones allow the computation of the reachability set X by an increasing sequence of sets included in X. The second ones, guided by the property to be verified, compute a precise over-approximation of X by a decreasing sequence of sets containing X.

Goals :

Used separately, these techniques do not scale up to complex large systems. The main objective of this thesis consists in reducing the gap between the two methods families, for instance by providing techniques that limit the loss of precision during approximated computations [GH-SAS06]. In a recent paper [LS-SAS07], we have studied the problem of computing the most precise fix-point in an abstract lattice. That means we try to effectively compute the most precise inductive invariant of a system that can be represented by an abstract value. The loss of precision is controlled here by the choice of the abstract lattice (intervals, octagons, octahedra, and so on) and does not depend on the way the abstract value is computed. This approach has provided efficient algorithms for the interval lattice. Extending this approach to other abstract lattices is the first chalenging problem of this thesis proposal.

 

References :

[BW-ICALP02] B. Boigelot and P. Wolper. Representing Arithmetic Constraints with Automata: An Overview. In Proc. Proc. 18th International Conference on Logic Programming, volume 2401, Lecture Notes in Computer Science, pages 1-19, Copenhagen, July 2002, Springer-Verlag.
[CH-POPL78] Patrick Cousot and Nicholas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth annual ACM Symposium on Principles of Programming Languages, pages 84--96. ACM, ACM, January 1978.
[FAST] Fast homepage. http://www.lsv.ens-cachan.fr/fast/
[GH-SAS06] L. Gonnord and N. Halbwachs. Combining widening and acceleration in Linear Relation Analysis. Proc. In Int. Symp. of Static Analysis (SAS'06), volume 4134, Lecture Notes in Computer Science, Seoul, Korea, August 2006, Springer-Verlag.
[LS-CONCUR04] J. Leroux and G. Sutre. On flatness for 2-dimensional vector addition systems with states. In Proc. 15th Int. Conf. Concurrency Theory (CONCUR'04), London, UK, Aug.-Sep. 2004, volume 3170 of Lecture Notes in Computer Science, pages 402-416. Springer, 2004.
[LS-SAS07] J. Leroux and G. Sutre. Accelerated Data-flow Analysis. In Proc. 15th Int. Static Analysis Symposium (SAS'07), Kongens Lyngby, Denmark, Aug. 2007, volume of Lecture Notes in Computer Science (to appear). Springer, 2007.