Advertisement

A New Numerical Abstract Domain Based on Difference-Bound Matrices

  • Antoine Miné
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2053)

Abstract

This paper presents a new numerical abstract domain for static analysis by abstract interpretation. This domain allows us to represent invariants of the form (xy = 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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In FMPA’ 93, number 735 in LNCS, pages 128–141. Springer-Verlag, 1993.Google Scholar
  2. [2]
    T. Cormen, C. Leiserson, and R. Rivest. Introduction to Algorithms. The MIT Press, 1990.Google Scholar
  3. [3]
    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
  4. [4]
    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
  5. [5]
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In ACM POPL’ 79, pages 269–282. ACM Press, 1979.Google Scholar
  6. [6]
    P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2-3):103–179, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  7. [7]
    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
  8. [8]
    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
  9. [9]
    L. Lamport. A new solution of dijkstra’s concurrent programming problem. Communications of the ACM, 8(17):453–455, August 1974.CrossRefMathSciNetGoogle Scholar
  10. [10]
    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
  11. [11]
    K. Larsen, C. Weise, W. Yi, and J. Pearson. Clock difference diagrams. Nordic Journal of Computing, 6(3):271–298, October 1999.zbMATHMathSciNetGoogle Scholar
  12. [12]
    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.
  13. [13]
    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
  14. [14]
    S. Yovine. Model-checking timed automata. In Embedded Systems, number 1494 in LNCS, pages 114–152. Springer-Verlag, October 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Antoine Miné
    • 1
  1. 1.École Normale Supérieure de ParisFrance

Personalised recommendations