Skip to main content
SpringerLink
Log in
Book cover

The Future of Software Engineering pp 48–71Cite as

Logical Abstract Domains and Interpretations

  • Chapter
  • First Online:

Abstract

We give semantic foundations to abstract domains consisting in first order logic formulæ in a theory, as used in verification tools or methods using SMT-solvers or theorem provers.We exhibit conditions for a sound usage of such methods with respect to multi-interpreted semantics and extend their usage to automatic invariant generation by abstract interpretation.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   54.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ball, T., Podelski, A., Rajamani, S.: Relative completeness of abstraction refinement for software model checking. In: Katoen, J.P., Stevens, P. (eds.) Proc. 8th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2002). pp. 158—172. LNCS 2280, Springer, Heidelberg, Grenoble (April 8–12, 2002)

    Chapter  Google Scholar 

  2. Bertrane, J., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min´e, A., Rival, X.: Static analysis and verification of aerospace software by abstract interpretation. In: AIAA Infotech@ Aerospace 2010, Atlanta, Georgia. pp. AIAA 2010–3385. AIAA (20–22 April 2010)

    Google Scholar 

  3. Boucher, D., Feeley, M.: Abstract compilation: a new implementation paradigm for static analysis. In: Gyimothy, T. (ed.) Proc. 6th Int. Conf. on Compiler Construction, CC ’96. pp. 192–207. Linköoping, Lecture Notes in Computer Science 1060, Springer, Heidelberg (April 24–26, 1996)

    Google Scholar 

  4. Bradley, A., Manna, Z.: The Calculus of Computation, Decision procedures with Applications to Verification. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  5. Bryant, R.E.: Graph based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35, 677–691 (August 1986)

    Google Scholar 

  6. Chang, C., Keisler, H.: Model theory. Studies in logic and the foundation of mathematics, vol. 73. Elsevier Science, New York (1990)

    Google Scholar 

  7. Clarke, E., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods in System Design 19(1), 7–34 (2001)

    Article  MATH  Google Scholar 

  8. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  9. Codish, M., Søndergaard, H.: Meta-circular abstract interpretation in Prolog. In: Mogensen, T., Schmidt, D., Sudburough, I. (eds.) The Essence of Computation: Complexity, Analysis, Transformation. LNCS, vol. 2566, pp. 109–134. Springer-Verlag (2002)

    Google Scholar 

  10. Cook, S.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 70–80 (1978)

    Article  MATH  MathSciNet  Google Scholar 

  11. Cooper, D.: Theorem proving in arithmetic without multiplication. Machine Intelligence 91(7), 91–99 (1972)

    Google Scholar 

  12. Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes (in French). Th`ese d’ É tat `es sciences mathématiques, Université scientifique et médicale de Grenoble, Grenoble (21 March, 1978)

    Google Scholar 

  13. Cousot, P.: Methods and logics for proving programs. In: van Leeuwen, J. (ed.) Formal Models and Semantics, Handbook of Theoretical Computer Science, vol. B, chap. 15, pp. 843– 993. Elsevier Science Publishers B.V., Amsterdam (1990)

    Google Scholar 

  14. Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Proc. 23rd Int. Col., ICALP ’96, pp. 1–3. LNCS 1099, Springer, Heidelberg, Paderborn, Germany (July 8–12, 1996)

    Google Scholar 

  15. Cousot, P.: Abstract interpretation based static analysis parameterized by semantics. In: Van Hentenryck, P. (ed.) Pro. 4th Int. Symp. on Static Analysis, SAS ’97, pp. 388–394. Paris, LNCS 1302, Springer, Heidelberg (September 8–10, 1997)

    Google Scholar 

  16. Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science 277(1—2), 47–103 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  17. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. 2nd Int. Symp. on Programming. pp. 106–130. Dunod, Paris, Paris (1976)

    Google Scholar 

  18. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th POPL. pp. 238–252. ACM Press, Los Angeles (1977)

    Google Scholar 

  19. Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pacific Journal of Mathematics 82(1), 43–57 (1979)

    MATH  MathSciNet  Google Scholar 

  20. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: 6th POPL. pp. 269–282. ACM Press, San Antonio (1979)

    Google Scholar 

  21. Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation 2(4), 511–547 (August 1992)

    Article  MATH  MathSciNet  Google Scholar 

  22. Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) Proc. 4th Int. Symp. Programming Language Implementation and Logic Programming, PLILP ’92. pp. 269–295. Leuven, 26–28 August 1992, LNCS 631, Springer, Heidelberg (1992)

    Google Scholar 

  23. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Minée, A., Monniaux, D., Rival, X.: The ASTRÉE analyser. In: Sagiv, M. (ed.) Proc. 14th European Symp. on Programming Languages and Systems, ESOP ’2005, Edinburg, pp. 21–30. LNCS 3444, Springer, Heidelberg (April 2–10, 2005)

    Google Scholar 

  24. Detlefs, D., Nelson, G., Saxe, J.: Simplify: a theorem prover for program checking. Journal of the ACM (JACM) 52(3), 365–473 (2005)

    Article  MathSciNet  Google Scholar 

  25. Ehrenfeucht, A.: Decidability of the theory of one function. Notices Amer. Math. Soc. 6, 268 (1959)

    Google Scholar 

  26. Ferrante, J., Geiser, J.: An efficient decision procedure for the theory of rational order. Theoretical Computer Science 4(2), 227–233 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  27. Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM Journal of Computation 4(1), 69–76 (1975)

    Article  MATH  MathSciNet  Google Scholar 

  28. Floyd, R.: Assigning meaning to programs. In: Schwartz, J. (ed.) Pro. Symp. in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society, Providence (1967)

    Google Scholar 

  29. Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. Conf. on Automated Deduction, CADE 21 4603 of LNAI, 167–182 (2007)

    Google Scholar 

  30. Ge, Y., de Moura, L.: Complete instantiation of quantified formulas in satisfiability modulo theories. Computer Aided Verification, CAV’2009 5643 of LNCS, 306–320 (2009)

    Google Scholar 

  31. Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: 35th POPL. pp. 235–246. ACM Press, San Francisco (2008)

    Google Scholar 

  32. Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Schwartzbach, M., Ball, T. (eds.) PLDI 2006. pp. 376–386. ACM Press, Ottawa, Ontario, Canada (11–14 June 2006)

    Google Scholar 

  33. Hitchcock, P., Park, D.: Induction rules and termination proofs. In: Nivat, M. (ed.) Proc. 1st Int. Colloq. on Automata, Languages and Programming. pp. 225–251. North-Holland (1973)

    Google Scholar 

  34. Hoare, C.: An axiomatic basis for computer programming. Communications of the Association for Computing Machinery 12(10), 576–580 (oct 1969)

    MATH  Google Scholar 

  35. King, J.: A Program Verifier. Ph.D. thesis, Carnegie-Mellon University (1969)

    Google Scholar 

  36. Luckham, D., Park, D., Paterson, M.: On formalized computer programs. J. of Computer and System Science 4(3), 220–240 (June 1970)

    MATH  MathSciNet  Google Scholar 

  37. Mauborgne, L.: Abstract interpretation using typed decision graphs. Science of Computer Programming 31(1), 91–112 (May 1998)

    Article  MATH  MathSciNet  Google Scholar 

  38. McMillan, K.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K. (eds.) Computer Aided Verification, CAV’2002. vol. 2404 of LNCS, pp. 250–264 (2002)

    Google Scholar 

  39. de Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: Voronkov, A. (ed.) Proc. 15th Computer-Aided Verification conf. (CAV’03). LNCS, vol. 2725, pp. 14–26. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  40. Naur, P.: Proofs of algorithms by general snapshots. BIT 6, 310–316 (1966)

    Google Scholar 

  41. Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (oct 1979)

    Article  MATH  Google Scholar 

  42. Pratt, V.: Two easy theories whose combination is hard. Tech. rep., MIT (september 1, 1977), http://boole.stanford.edu/pub/sefnp.pdf

  43. Reps, T., Sagiv, S., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) Proc. 5th Int. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI 2004). pp. 252–266. LNCS 2937, Springer, Heidelberg, Venice (January 11–13, 2004)

    Chapter  Google Scholar 

  44. Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Transactions on Programming Languages and Systems 29(5) (August 2007)

    Article  Google Scholar 

  45. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: 26th POPL. pp. 238–252. ACM Press, an Antonio (1999)

    Google Scholar 

  46. Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5, 285–310 (1955)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre National de la Recherche Scientifique, Paris, France

    Radhia Cousot

  2. Courant Institute of Mathematical Sciences, New York University, New York, USA

    Patrick Cousot

  3. École Normale Supérieure, Paris, France

    Patrick Cousot, Radhia Cousot & Laurent Mauborgne

  4. Instituto Madrileño de Estudios Avanzados, Madrid, Spain

    Laurent Mauborgne

Authors
  1. Patrick Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Radhia Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Laurent Mauborgne
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. , Department of Computer Science, ETH Zürich, Clausiusstr. 59, Zürich, 8092, Switzerland

    Sebastian Nanz

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Cousot, P., Cousot, R., Mauborgne, L. (2011). Logical Abstract Domains and Interpretations. In: Nanz, S. (eds) The Future of Software Engineering. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15187-3_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15187-3_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15186-6

  • Online ISBN: 978-3-642-15187-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation