Transition predicate abstraction and fair termination

ABSTRACT

Predicate abstraction is the basis of many program verification tools. Until now, the only known way to overcome the inherent limitation of predicate abstraction to safety properties was to manually annotate the finite-state abstraction of a program. We extend predicate abstraction to transition predicate abstraction. Transition predicate abstraction goes beyond the idea of finite abstract-state programs (and checking the absence of loops). Instead, our abstraction algorithm transforms a program into a finite abstract-transition program. Then a second algorithm checks fair termination. The two algorithms together yield an automated method for the verification of liveness properties under full fairness assumptions (impartiality, justice, and compassion). In summary, we exhibit principles that extend the applicability of predicate abstraction-based program verification to the full set of temporal properties.

REFERENCES

• 1: Thomas Arts , Jürgen Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, v.236 n.1-2, p.133-178, April 6, 2000 [doi>10.1016/S0304-3975(99)00207-8]
• 2: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1998
• 3: Ball, T. 2005. A theory of predicate-complete test coverage and generation. In FMCO'2004: Symposium on Formal Methods for Components and Objects. Lecture Notes in Computer Science, vol. 3657. Springer, Berlin, Germany, 1--22.
• 4: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, ACM SIGPLAN Notices, v.36 n.5, p.203-213, May 2001
• 5: Thomas Ball , Andreas Podelski , Sriram K. Rajamani, Boolean and Cartesian Abstraction for Model Checking C Programs, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.268-283, April 02-06, 2001
• 6: François Bourdoncle, Abstract debugging of higher-order imperative languages, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.46-55, June 21-25, 1993, Albuquerque, New Mexico, United States
• 7: Bradley, A. R., Manna, Z., and Sipma, H. B. 2005. Linear ranking with reachability. In CAV'2005: Computer Aided Verification. Lecture Notes in Computer Science, vol. 3576. Springer, Berlin, Germany, 491--504.
• 8: I. A. Browne , Zohar Manna , Henny Sipma, Generalized Temporal Verification Diagrams, Proceedings of the 15th Conference on Foundations of Software Technology and Theoretical Computer Science, p.484-498, December 18-20, 1995
• 9: Büchi, J. R. 1960. On a decision method in restricted second order arithmeric. In Proceedings of the International Congress on Logic, Methodology and Philosophy of Science. Stanford University Press, Stanford, CA, 1--11.
• 10: Sagar Chaki , Edmund Clarke , Alex Groce , Somesh Jha , Helmut Veith, Modular verification of software components in C, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
• 11: Codish, M., Genaim, S., Bruynooghe, M., Gallagher, J., and Vanhoof, W. 2003. One loop at a time. In 6th International Workshop on Termination (WST 2003). Universidad Politécnica de Valencia, Valencia, Spain.
• 12: Michael Colón , Henny Sipma, Synthesis of Linear Ranking Functions, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.67-81, April 02-06, 2001
• 13: Michael Colón , Tomás E. Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures, Proceedings of the 10th International Conference on Computer Aided Verification, p.293-304, June 28-July 02, 1998
• 14: Cook, B., Podelski, A., and Rybalchenko, A. 2005. Abstraction refinement for termination. In SAS'2005: Static Analysis Symposium. Lecture Notes in Computer Science, vol. 3672. Springer, Berlin, Germany, 87--101.
• 15: Byron Cook , Andreas Podelski , Andrey Rybalchenko, Termination proofs for systems code, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 16: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 17: Cousot, P. and Cousot, R. 1994. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In ICCL'1994: Proceedings of the International Conference on Computer Languages. IEEE Computer Society Press, Los Alamitos, CA, 95--112.
• 18: Delzanno, G. and Podelski, A. 2001. Constraint-based deductive model checking. Int. J. Softw. Tools Tech. Trans. 3, 3, 250--270.
• 19: Dershowitz, N., Lindenstrauss, N., Sagiv, Y., and Serebrenik, A. 2001. A general framework for automatic termination analysis of logic programs. Applic. Alg. Eng. Commun. Comput 12, 117--156.
• 20: Cormac Flanagan , Shaz Qadeer, Predicate abstraction for software verification, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.191-202, January 16-18, 2002, Portland, Oregon
• 21: Nissim Francez, Fairness, Springer-Verlag New York, Inc., New York, NY, 1986
• 22: Susanne Graf , Hassen Saïdi, Construction of Abstract State Graphs with PVS, Proceedings of the 9th International Conference on Computer Aided Verification, p.72-83, June 22-25, 1997
• 23: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 24: Verification by augmented finitary abstraction, Information and Computation, v.163 n.1, p.203-243, Nov. 25, 2000 [doi>10.1006/inco.2000.3000]
• 25: Yonit Kesten , Amir Pnueli , Moshe Y. Vardi, Verification by Augmented abstraction: the automata---theoretic view, Journal of Computer and System Sciences, v.62 n.4, p.668-690, June 2001 [doi>10.1006/jcss.2000.1744]
• 26: Nils Klarlund, Progress measures and stack assertions for fair termination, Proceedings of the eleventh annual ACM symposium on Principles of distributed computing, p.229-240, August 10-12, 1992, Vancouver, British Columbia, Canada [doi>10.1145/135419.135462]
• 27: Lahiri, S. K., Bryant, R. E., and Cook, B. 2003. A symbolic approach to predicate abstraction. In CAV'2003: Computer Aided Verification. Lecture Notes in Computer Science, vol. 2725. Springer, Berlin, Germany, 141--153.
• 28: Chin Soon Lee , Neil D. Jones , Amir M. Ben-Amram, The size-change principle for program termination, ACM SIGPLAN Notices, v.36 n.3, p.81-92, March 2001
• 29: Daniel J. Lehmann , Amir Pnueli , Jonathan Stavi, Impartiality, Justice and Fairness: The Ethics of Concurrent Termination, Proceedings of the 8th Colloquium on Automata, Languages and Programming, p.264-277, July 13-17, 1981
• 30: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 31: Manna, Z. and Pnueli, A. 1996. Temporal verification of reactive systems: Progress. unpublished article.
• 32: Stephan Merz, Rules for Abstraction, Proceedings of the Third Asian Computing Science Conference on Advances in Computing Science, p.32-45, December 09-11, 1997
• 33: Amir Pnueli , Jessie Xu , Lenore D. Zuck, Liveness with (0, 1, infty)-Counter Abstraction, Proceedings of the 14th International Conference on Computer Aided Verification, p.107-122, July 27-31, 2002
• 34: Podelski, A. and Rybalchenko, A. 2004a. A complete method for the synthesis of linear ranking functions. In VMCAI'2004: Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937. Springer, Berlin, Germany, 239--251.
• 35: Andreas Podelski , Andrey Rybalchenko, Transition Invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), p.32-41, July 13-17, 2004 [doi>10.1109/LICS.2004.50]
• 36: Ramsey, F. P. 1930. On a problem of formal logic. In Proc. London Math. Soc. 30, 264--285.
• 37: Sagiv, Y. 1991. A termination test for logic programs. In ISLP'1991: Proceedings of the International Logic Programming Symposium, 518--532.
• 38: Henny Sipma , Tomás E. Uribe , Zohar Manna, Deductive Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.208-219, August 03, 1996
• 39: Tiwari, A. 2004. Termination of linear programs. In CAV'2004: Computer Aided Verification. Lecture Notes in Computer Science, vol. 3114. Springer, Berlin, Germany, 70--82.
• 40: Tomas E. Uribe Restrepo , Zohar Manna, Abstraction-based deductive-algorithmic verification of reactive systems, Stanford University, Stanford, CA, 1999
• 41: Vardi, M. Y. 1991. Verification of concurrent programs---the automata-theoretic framework. Ann. Pure Appl. Log. 51, 79--98.
• 42: Eran Yahav, Verifying safety properties of concurrent Java programs using 3-valued logic, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.27-40, January 2001, London, United Kingdom
• 43: Yahav, E., Reps, T., Sagiv, M., and Wilhelm, R. 2003. Verifying temporal heap properties specified via evolution logic. In ESOP'2003: European Symposium on Programming. Lecture Notes in Computer Science, vol. 2618. Springer, Berlin, Germany, 204--222.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Theory, Verification

Keywords:
Software model checking, fair termination, liveness, transition predicate abstraction