Advertisement

A Few Graph-Based Relational Numerical Abstract Domains

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

Abstract

This article presents the systematic design of a class of relational numerical abstract domains from non-relational ones. Constructed domains represent sets of invariants of the form (v j - v i ∈ C), where vj and vi are two variables, and C lives in an abstraction of \( \mathcal{P}(\mathbb{Z}) \) , \( \mathcal{P}(\mathbb{Q}) \) , or \( \mathcal{P}(\mathbb{R}) \) . We will call this family of domains weakly relational domains. The underlying concept allowing this construction is an extension of potential graphs and shortest-path closure algorithms in exotic-like algebras. Example constructions are given in order to retrieve well-known domains as well as new ones. Such domains can then be used in the Abstract Interpretation framework in order to design various static analyses. A major benefit of this construction is its modularity, allowing to quickly implement new abstract domains from existing ones.

Keywords

Relational Domain Abstract Domain Program Point Constraint Logic Programming Constraint Matrice 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    F. Bourdoncle. Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In Springer-Verlag, editor, PLILP’90, volume 456 of LNCS, pages 307–323, 1990.Google Scholar
  2. [2]
    F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In FMPA’ 93, number 735 in LNCS, 1993.Google Scholar
  3. [3]
    M. Codish and C. Taboch. A semantic basis for termination analysis of logic programs and its realization using symbolic norm constraints. In ALP’98, volume 1298 of LNCS, pages 31–45. Springer-Verlag, September 1997.Google Scholar
  4. [4]
    T. Cormen, C. Leiserson, and R. Rivest. Introduction to Algorithms. The MIT Press, 1990.Google Scholar
  5. [5]
    P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In ISOP’76, pages 106–130. Dunod, Paris, France, 1976.Google Scholar
  6. [6]
    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM POPL’77, pages 238–252. ACM Press, 1977.Google Scholar
  7. [7]
    P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, August 1992.Google Scholar
  8. [8]
    P. Cousot and R. Cousot. Modular static program analysis, invited paper. In CC’02, number 2304 in LNCS, pages 159–178, 2002.Google Scholar
  9. [9]
    P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In A CM POPL’78, pages 84–97. ACM Press, 1978.Google Scholar
  10. [10]
    A. Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In ACM PLDI’94, pages 230–241. ACM Press, 1994.Google Scholar
  11. [11]
    N. Dor, M. Rodeh, and M. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In SAS’01, number 2126 in LNCS, July 2001.Google Scholar
  12. [12]
    J. Feret. Occurrence counting analysis for the π-calculus. In GETCO’00, volume 39.2 of BRICS NS-00-3, 2001.Google Scholar
  13. [13]
    M. Gondran and M. Minoux. Graphs and Algorithms. Wiley, 1984.Google Scholar
  14. [14]
    P. Granger. Static analysis of arithmetical congruences. In International Journal of Computer Mathematics, volume 30, pages 165–190, 1989.CrossRefzbMATHGoogle Scholar
  15. [15]
    P. Granger. Static analysis of linear congruence equalities among variables of a program. In TAPSOFT’91, number 493 in LNCS, pages 169–192, 1991.Google Scholar
  16. [16]
    P. Granger. Static analyses of congruence properties on rational numbers. In SAS’97, volume 1302 of LNCS, pages 278–292, 1997.Google Scholar
  17. [17]
    W. Harvey and P. Stuckey. A unit two variable per inequality integer constraint solver for constraint logic programming. In ACSC’97, volume 19, pages 102–111, February 1997.Google Scholar
  18. [18]
    M. Karr. Affine relationships among variables of a program. Acta Informatica, pages 133–151, 1976.Google Scholar
  19. [19]
    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
  20. [20]
    F. Masdupuy. Semantic analysis of interval congruences. In FMPTA’ 93, volume 735 of LNCS, pages 142–155, 1993.Google Scholar
  21. [21]
    L. Mauborgne. Representation of Sets of Trees for Abstract Interpretation. PhD thesis, École Polytechnique, Palaiseau, France, November 1999.Google Scholar
  22. [22]
    A. Miné. A new numerical abstract domain based on difference-bound matrices. In PADO II, volume 2053 of LNCS, pages 155–172. Springer-Verlag, May 2001.Google Scholar
  23. [23]
    A. Miné. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, pages 310–319. IEEE CS Press, October 2001.Google Scholar
  24. [24]
    D. Monniaux. An abstract Monte-Carlo method for the analysis of probabilistic programs. In POPL’01, number 1824 in ACM, pages 93–101, 2001.Google Scholar
  25. [25]
    V. Pratt. Two easy theories whose combination is hard. Technical report, Massachusetts Institute of Technology, Cambridge, September 1977.Google Scholar
  26. [26]
    R. Shostak. Deciding linear inequalities by computing loop residues. Journal of the ACM, 28(4):769–779, October 1981.Google Scholar
  27. [27]
    D. Toman and J. Chomicki. Datalog with integer periodicity constraints. In Journal of Logic Programming, pages 189–203. The MIT Press, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

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

Personalised recommendations