Skip to main content
SpringerLink
Log in

Partial Completeness of Abstract Fixpoint Checking

Invited Paper

  • Conference paper
  • First Online:
Abstraction, Reformulation, and Approximation (SARA 2000)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1864))

Abstract

Abstract interpretation is used in program static analysis and model checking to cope with infinite state spaces and/or with computer resource limitations. One common problem is to check abstract fixpoints for specifications. The abstraction is partially complete when the checking algorithm is exact in that, if the algorithm ever terminates, its answer is always affirmative for correct specifications. We characterize partially complete abstractions for various abstract fixpoint checking algorithms, including new ones, and show that the computation of complete abstract domains is essentially equivalent to invariance proofs that is to concrete fixpoint checking.

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

Access this chapter

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

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P.A. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl, and L. Lakhnech. Verification of infinite-state systems by combining abstraction and reachability analysis. In N. Halbwachs and D. Peled, editors, Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV’ 99, Trento, Italy, Lecture Notes in Computer Science 1633, pages 146–159. Springer-Verlag, Berlin, Germany, 6–10 July 1999.

    Google Scholar 

  2. S. Bensalem, Y. Lakhnech, and S. Owre. Computing abstractions of infinite state systems compositionally and automatically. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the Tenth International Conference on Computer Aided Verification, CAV’ 98, Vancouver, British Columbia, Canada, Lecture Notes in Computer Science 1427, pages 319–331. Springer-Verlag, Berlin, Germany, 28 June–2 July 1998.

    Google Scholar 

  3. E.M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In IBM Workshop on Logics of Programs, Lecture Notes in Computer Science 131. Springer-Verlag, Berlin, Germany, May 1981.

    Google Scholar 

  4. E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512–1542, september 1994.

    Google Scholar 

  5. M. Colón and T.E. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the Tenth International Conference on Computer Aided Verification, CAV’ 98, Vancouver, British Columbia, Canada, Lecture Notes in Computer Science 1427, pages 293–304. Springer-Verlag, Berlin, Germany, 28 June–2 July 1998.

    Google Scholar 

  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. Thése d’État es sciences mathématiques, Université scientifique et médicale de Grenoble, Grenoble, 21 mars 1978.

    Google Scholar 

  7. P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, United States, 1981.

    Google Scholar 

  8. P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electronic Notes in Theoretical Computer Science, 6, 1997. URL: http://www.elsevier.nl/locate/entcs/volume6.html, 25 pages.

  9. P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science, To appear (Preliminary version in [8]).

    Google Scholar 

  10. 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, New York, United States.

    Google Scholar 

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

    MATH  MathSciNet  Google Scholar 

  12. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269–282, San Antonio, Texas, 1979. ACM Press, New York, New York, United States.

    Google Scholar 

  13. P. Cousot and R. Cousot. Induction principles for proving invariance properties of programs. In D. Néel, editor, Tools & Notions for Program Construction, pages 43–119. Cambridge University Press, Cambridge, United Kindom, 1982.

    Google Scholar 

  14. P. Cousot and R. Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2–3):103–179, 1992. (The editor of Journal of Logic Programming has mistakenly published the unreadable galley proof. For a correct version of this paper, see http://www.di.ens.fr/~cousot).

    Article  MATH  MathSciNet  Google Scholar 

  15. 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.

    Google Scholar 

  16. P. Cousot and R. Cousot. Parallel combination of abstract interpretation and model-based automatic analysis of software. In R. Cleaveland and D. Jackson, editors, Proceedings of the First ACM SIGPLAN Workshop on Automatic Analysis of Software, AAS’ 97, pages 91–98, Paris, France, January 1997. ACM Press, New York, New York, United States.

    Google Scholar 

  17. P. Cousot and R. Cousot. Refining model checking by abstract interpretation. Automated Software Engineering, 6:69–95, 1999.

    Article  Google Scholar 

  18. P. Cousot and R. Cousot. Temporal abstract interpretation. In Conference Record of the Twentyseventh Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 12–25, Boston, Massachusetts, January 2000. ACM Press, New York, New York, United States.

    Google Scholar 

  19. D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems, 19(2):253–291, 1997.

    Article  Google Scholar 

  20. S. Das, D.L. Dill, and S. Park. Experience with predicate abstraction. In N. Halbwachs and D. Peled, editors, Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV’ 99, Trento, Italy, Lecture Notes in Computer Science 1633, pages 160–171. Springer-Verlag, Berlin, Germany, 6–10 July 1999.

    Google Scholar 

  21. R.W. Floyd. Assigning meaning to programs. In J.T. Schwartz, editor, Proceedings of the Symposium in Applied Mathematics, volume 19, pages 19–32. American Mathematical Society, Providence, Rhode Island, United States, 1967.

    Google Scholar 

  22. R. Giacobazzi, F. Ranzato, and F. Scozzari. Complete abstract interpretations made constructive. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of the Twentythird International Symposium on Mathematical Foundations of Computer Science, MFCS’98, volume 1450 of Lecture Notes in Computer Science, pages 366–377. Springer-Verlag, Berlin, Germany, 1998.

    Google Scholar 

  23. R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract intrepretations complete. Journal of the Association for Computing Machinary, 2000. To appear.

    Google Scholar 

  24. S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In C. Courcoubetis, editor, Proceedings of the Fifth International Conference on Computer Aided Verification, CAV’ 93, Elounda, Greece, Lecture Notes in Computer Science 697, pages 71–84. Springer-Verlag, Berlin, Germany, 28 June–1 July 1993.

    Google Scholar 

  25. S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In O. Grumberg, editor, Proceedings of the Ninth International Conference on Computer Aided Verification, CAV’97, Haifa, Israel, Lecture Notes in Computer Science 1254, pages 72–83. Springer-Verlag, Berlin, Germany, 22–25 July 1997.

    Google Scholar 

  26. T.A. Henzinger, O. Kupferman, and S. Qadeer. From Pre-historic to Post-modern symbolic model checking. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the Tenth International Conference on Computer Aided Verification, CAV’ 98, Vancouver, British Columbia, Canada, Lecture Notes in Computer Science 1427, pages 195–206. Springer-Verlag, Berlin, Germany, June /July 1998.

    Google Scholar 

  27. Y. Kesten and A. Pnueli. Modularization and abstraction: The keys to formal verification. In L. Brim, J. Gruska, and J. Zlatuska, editors, Twentythird International Symposium on Mathematical Foundations of Computer Science 1998, Lecture Notes in Computer Science 1450, pages 54–71. Springer-Verlag, Berlin, Germany, 1998.

    Chapter  Google Scholar 

  28. C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. Property preserving abstractions for the verification of concurrent systems. Formal Methods in System Design, 6(1), 1995.

    Google Scholar 

  29. D. Monniaux. Réalisation mécanisée d’interpréteurs abstraits. Rapport de stage, DEA “Sémantique, Preuve et Programmation”, July 1998.

    Google Scholar 

  30. J.H. Morris and B. Wegbreit. Sungoal induction. Communications of the Association for Computing Machinary, 20(4):209–222, April 1977.

    Google Scholar 

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

    Article  Google Scholar 

  32. J.-P. Queille and J. Sifakis. Verification of concurrent systems in Cesar. In Proceedings of the International Symposium on Programming, Lecture Notes in Computer Science 137, pages 337–351. Springer-Verlag, Berlin, Germany, 1982.

    Google Scholar 

  33. H. Saïdi and N. Shankar. Abstract and model check while you prove. In N. Halbwachs and D. Peled, editors, Proceedings of the Eleventh International Conference on Computer Aided Verification, CAV’99, Trento, Italy, Lecture Notes in Computer Science 1633, pages 443–454. Springer-Verlag, Berlin, Germany, 6–10 July 1999.

    Google Scholar 

  34. A. Tarski. 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. Département d’informatique, École normale supérieure, 45 rue d’Ulm, 75230, Paris cedex 05, France

    Patrick Cousot

Authors
  1. Patrick Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, University of Nebraska - Lincoln, 115 Ferguson Hall, Lincoln, NE, 68588-0115

    Berthe Y. Choueiry

  2. Department of Computer Science, University of York, Heslington, York, Y010 5DD, UK

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cousot, P. (2000). Partial Completeness of Abstract Fixpoint Checking. In: Choueiry, B.Y., Walsh, T. (eds) Abstraction, Reformulation, and Approximation. SARA 2000. Lecture Notes in Computer Science(), vol 1864. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44914-0_1

Download citation

  • DOI: https://doi.org/10.1007/3-540-44914-0_1

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67839-7

  • Online ISBN: 978-3-540-44914-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation