![[Domain Sample]](dbm.gif)
This work was done as part of the DEA (Diplômes d'études avancées) Semantics, Proofs and Languages within the LIENS (Computer Science Laboratory at the ENS, Paris, France) supervised by Patrick Cousot.
Keywords: Program Analysis, Abstract Interpretation, Difference Bound Matrices (DBM), Numerical Invariants.
In this report, we present a new method for the automatic static analysis of programs. As with the standard intervals and linear inequalities analysis, this analysis discovers numeric invariants in a program. More precisely, we discover invariants of the form ±x ±y ≤ c (which we call a two-variable difference or sum constraint), where x and y are values of variables and c is a numerical constant.
We use difference bound matrices to represent two-variable difference and sum constraints. They have a O(n2) space costs in the worst case, where n is the number of variables in the program, and the algorithms to manipulate them have a worst-case time complexity of O(n3). The soundness of this analysis is proved in the abstract interpretation framework by using Galois connections between complete lattices.
Difference bound matrices are widely used in the model-checking of automata but we had to design many new operators (widening, assignment, guard,\ldots) in order to adapt them to abstract interpretation. We also extended difference bound matrices in order to represent sums or differences of two variables ±x ±y ≤ c as they were used, until now, only to represent difference of two variables x-y ≤ c.
|
| Domain of a two-variable sum or difference constraint set. |
This theoretical work lead to the implementation of a library called The Octagon Abstract Domain Library and is freely available.
| [1] | Thomas Cormen, Charles Leiserson, and Ronald Rivest.
Introduction to Algorithms.
The MIT Press, 1990. |
| [2] | Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi.
Efficient verification of real-time systems : Compact data structure
and state-space reduction.
http://www.docs.uu.se/docs/rtmv/papers/llpw-rtss97.ps.gz. |
| [3] | S. Yovine.
Model-checking timed automata.
In Embedded Systems, Lecture Notes in Computer Science.
G.Rozenberg and F.Vaandrager eds., 1998.
http://www-verimag.imag.fr/~yovine/articles/rts_embedded98.html. |
| [4] | P. Cousot and R. Cousot.
Abstract interpretation and application to logic programs.
Journal of Logic Programming, 13(2-3):103-179, 1992.
http://www.di.ens.fr/~cousot/COUSOTpapers/JLP92.shtml. |
| [5] | P. Cousot.
The calculational design of a generic abstract interpreter.
In M. Broy and R. Steinbrüggen, editors, Calculational
System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999.
http://www.di.ens.fr/~cousot/COUSOTpapers/Marktoberdorf98.shtml. |
| [6] | P. Cousot.
Méthodes itératives de construction et d'approximation de
points fixes d'opérateurs monotones sur un treillis, analyse sémantique
de programmes.
PhD thesis, Thse d'état ès sciences mathématiques,
Université scientifique et medicale de Grenoble,France, 1978. |
| [7] | P. Cousot and R. Cousot.
Static determination of dynamic properties of programs.
In Proceedings of the Second International Symposium on
Programming, pages 106-130. Dunod, Paris, France, 1976.
http://www.di.ens.fr/~cousot/COUSOTpapers/ISOP76.shtml. |
| [8] | P. Cousot and R. Cousot.
Comparing the Galois connection and widening/narrowing approaches
to abstract interpretation, invited paper.
In M. Bruynooghe and M. Wirsing, editors, Proceedings of the
International Workshop Programming Language Implementation and Logic
Programming, PLILP'92,, Leuven, Belgium, 13-17 August 1992, Lecture
Notes in Computer Science 631, pages 269-295. Springer-Verlag, Berlin,
Germany, 1992.
http://www.di.ens.fr/~cousot/COUSOTpapers/PLILP92.shtml. |
| [9] | P. Cousot and N. Halbwachs.
Automatic discovery of linear restraints among variables of a
program.
In Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, pages 84-97, Tucson,
Arizona, 1978. ACM Press, New York, NY. |
| [10] | P. Cousot.
Constructive design of a hierarchy of semantics of a transition
system by abstract interpretation.
Theoretical Computer Science, 2000.
http://www.di.ens.fr/~cousot/COUSOTpapers/TCS00.shtml. |
| [11] | P. Cousot and R. Cousot.
Abstract interpretation: a unified lattice model for static analysis
of programs by construction or approximation of fixpoints.
In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, pages 238-252, Los
Angeles, California, 1977. ACM Press, New York, NY.
http://www.di.ens.fr/~cousot/COUSOTpapers/POPL77.shtml. |
| [12] | R. Bellman.
On a routing problem.
In Quarterly of Applied Mathematics, volume 16, pages 87-90,
1958. |
| [13] | David Monniaux.
Abstract interpretation of probabilistic semantics.
In Seventh International Static Analysis Symposium (SAS'00),
number 1824 in Lecture Notes in Computer Science. Springer-Verlag, 2000.
http://www.di.ens.fr/~monniaux/biblio/Monniaux_SAS00.ps.gz. |
| [14] | François Bourdoncle.
Abstract debugging of higher-order imperative languages.
In SIGPLAN '93 Conference on Programming Language Design and
Implementation, pages 46-55, 1993.
http://www.cma.ensmp.fr/Francois.Bourdoncle/pldi93.html. |
| [15] | Hassen Saïdi.
Model checking guided abstraction and analysis.
In Jens Palsberg, editor, Seventh International Static Analysis
Symposium (SAS'00), number 1824 in Lecture Notes in Computer Science,
pages 377-396. Springer-Verlag, 2000.
http://www.csl.sri.com/~saidi/PAPERS/sas00.html. |