A New Numerical Abstract Domain Based on Difference-Bound Matrices
- 210 Downloads
This paper presents a new numerical abstract domain for static analysis by abstract interpretation. This domain allows us to represent invariants of the form (x − y = c) and (±x = c) , where x and y are variables values and c is an integer or real constant.
Abstract elements are represented by Difference-Bound Matrices, widely used by model-checkers, but we had to design new operators to meet the needs of abstract interpretation. The result is a complete lattice of infinite height featuring widening, narrowing and common transfer functions. We focus on giving an efficient O(n 2)re presentation and graph-based O(n 3)algorit hms—where n is the number of variables—and claim that this domain always performs more precisely than the well-known interval domain.
To illustrate the precision/cost tradeoff of this domain, we have implemented simple abstract interpreters for toy imperative and parallel languages which allowed us to prove some non-trivial algorithms correct.
Unable to display preview. Download preview PDF.
- F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In FMPA’ 93, number 735 in LNCS, pages 128–141. Springer-Verlag, 1993.Google Scholar
- T. Cormen, C. Leiserson, and R. Rivest. Introduction to Algorithms. The MIT Press, 1990.Google Scholar
- 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. Thèse d’état ès sciences mathématiques, Université scientifique et médicale de Grenoble, France, 1978.Google Scholar
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. of the 2 d Int. Symposium on Programming, pages 106–130. Dunod, Paris, France, 1976.Google Scholar
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In ACM POPL’ 79, pages 269–282. ACM Press, 1979.Google Scholar
- P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, invited paper. In PLILP’92, number 631 in LNCS, pages 269–295. Springer-Verlag, August 1992.Google Scholar
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In ACM POPL’78, pages 84–97. ACM Press, 1978.Google Scholar
- K. Larsen, F. Larsson, P. Pettersson, and W. Yi. Efficient verification of real-time systems: Compact data structure and state-space reduction. In IEEE RTSS’97, pages 14–24. IEEE CS Press, December 1997.Google Scholar
- A. Miné. Representation of Two-Variable Difference or Sum Constraint Set and Application to Automatic Program Analysis. Master’s thesis, ENS, 2000. http://www.eleves.ens.fr:8080/home/mine/stage_dea/index.shtml.en.
- J. Møller, J. Lichtenberg, R. Andersen, H., and H. Hulgaard. Difference decision diagrams. In CSL’99, volume 1683 of LNCS, pages 111–125. Springer-Verlag, September 1999.Google Scholar
- S. Yovine. Model-checking timed automata. In Embedded Systems, number 1494 in LNCS, pages 114–152. Springer-Verlag, October 1998.Google Scholar