Andreas Podelski
Andrey Rybalchenko
Skip Abstract Section
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.
- Arts, T. and Giesl, J. 2000. Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236, 1--2, 133--178. Google Scholar
Digital Library
- Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press, Cambridge, U.K. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. 2001a. Automatic predicate abstraction of C programs. In PLDI'2001: Programming Language Design and Implementation. ACM SIGPLAN Not. 36, 203--213. Google ScholarDigital Library
- Ball, T., Podelski, A., and Rajamani, S. K. 2001b. Boolean and Cartesian abstractions for model checking C programs. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer, Berlin, Germany, 268--283. Google ScholarDigital Library
- Bourdoncle, F. 1993. Abstract debugging of higher-order imperative languages. In PLDI'1993: Proceedigs of the Conference on Programming Language Design and Implementation. ACM Press, New York, NY, 46--55. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Browne, I., Manna, Z., and Sipma, H. 1995. Generalized verification diagrams. In FSTTCS'1995: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 1026. Springer, Berlin, Germany, 484--498. Google ScholarDigital Library
- 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.Google Scholar
- Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H. 2003. Modular verification of software components in C. In ICSE'2003: Proceedings of the International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 385--395. Google ScholarDigital Library
- 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.Google Scholar
- Colón, M. and Sipma, H. 2001. Synthesis of linear ranking functions. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2031. Springer, Berlin, Germany, 67--81. Google ScholarDigital Library
- Colón, M. and Uribe, T. 1998. Generating finite-state abstractions of reactive systems using decision procedures. In CAV'1998: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1427. Springer, Berlin, Germany, 293--304. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- Cook, B., Podelski, A., and Rybalchenko, A. 2006. Termination proofs for systems code. In PLDI'06: Proceedings of the Conference on Programming Language Design and Implementation. ACM Press, New York, NY. Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'1977: Proceedings of the Conference on Principles of Programming Languages. ACM Press, New York, NY, 238--252. Google ScholarDigital Library
- 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.Google Scholar
- Delzanno, G. and Podelski, A. 2001. Constraint-based deductive model checking. Int. J. Softw. Tools Tech. Trans. 3, 3, 250--270.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- Flanagan, C. and Qadeer, S. 2002. Predicate abstraction for software verification. In POPL'2002: Proceedings of the Conference on Principles of Programming Languages. ACM Press, New York, NY, 191--202. Google ScholarDigital Library
- Francez, N. 1986. Fairness. Springer, Berlin, Germany. Google ScholarDigital Library
- Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In CAV'1997: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1254. Springer, Berlin, Germany, 72--83. Google ScholarDigital Library
- Henzinger, T., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In POPL'2002: Proceedings of the Conference on Principles of Programming Languages. ACM Press, New York, NY, 58--70. Google ScholarDigital Library
- Kesten, Y. and Pnueli, A. 2000. Verification by augmented finitary abstraction. Inform. Computat. (Special Issue on Compositionality) 163, 1, 203--243. Google ScholarDigital Library
- Kesten, Y., Pnueli, A., and Vardi, M. Y. 2001. Verification by augmented abstraction: The automata-theoretic view. J. Comput. Syst Sci. 62, 4, 668--690. Google ScholarDigital Library
- Klarlund, N. 1992. Progress measures and stack assertions for fair termination. In PODC'1992: Proceedings of the Conference on Principles of Distributed Computing. ACM Press, New York, NY, 229--240. Google ScholarDigital Library
- 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.Google Scholar
- Lee, C. S., Jones, N. D., and Ben-Amram, A. M. 2001. The size-change principle for program termination. In POPL'2001: Principles of Programming Languages. ACM SIGPLAN Not. 36, 3, 81--92. Google ScholarDigital Library
- Lehmann, D., Pnueli, A., and Stavi, J. 1981. Impartiality, justice and fairness: The ethics of concurrent termination. In ICALP'1981: International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 115. Springer, Berlin, Germany, 264--277. Google ScholarDigital Library
- Manna, Z. and Pnueli, A. 1995. Temporal verification of reactive systems: Safety. Springer, Berlin, Germany. Google ScholarDigital Library
- Manna, Z. and Pnueli, A. 1996. Temporal verification of reactive systems: Progress. unpublished article.Google Scholar
- Merz, S. 1997. Rules for abstraction. In ASIAN'1997: Advances in Computer Science. Lecture Notes in Computer Science, vol. 1345. Springer, Berlin, Germany, 32--45. Google ScholarDigital Library
- Pnueli, A., Xu, J., and Zuck, L. 2002. Liveness with (0, 1, ∞)-counter abstraction. In CAV'2002: Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404. Springer, Berlin, Germany, 107--122. Google ScholarDigital Library
- 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.Google Scholar
- Podelski, A. and Rybalchenko, A. 2004b. Transition invariants. In LICS'2004: Proceedings of the Conference on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 32--41. Google ScholarDigital Library
- Ramsey, F. P. 1930. On a problem of formal logic. In Proc. London Math. Soc. 30, 264--285.Google ScholarCross Ref
- Sagiv, Y. 1991. A termination test for logic programs. In ISLP'1991: Proceedings of the International Logic Programming Symposium, 518--532.Google Scholar
- Sipma, H., Uribe, T., and Manna, Z. 1996. Deductive model checking. In CAV'1996: Computer Aided Verification. Lecture Notes in Computer Science, vol. 1102. Springer, Berlin, Germany, 208--219. Google ScholarDigital Library
- 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.Google Scholar
- Uribe, T. 1999. Abstraction-based deductive-algorithmic verification of reactive systems. Ph.D. dissertation. Stanford University, Stanford, CA. Google ScholarDigital Library
- Vardi, M. Y. 1991. Verification of concurrent programs---the automata-theoretic framework. Ann. Pure Appl. Log. 51, 79--98.Google ScholarCross Ref
- Yahav, E. 2001. Verifying safety properties of concurrent Java programs using 3-valued logic. In POPL'2001: Proceedings of the Conference on Principles of Programming Languages. ACM Press, New York, NY, 27--40. Google ScholarDigital Library
- 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. Google ScholarDigital Library
Index Terms
- Transition predicate abstraction and fair termination
Recommendations
Transition predicate abstraction and fair termination
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate 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 ...
Transition predicate abstraction and fair termination
POPL '05: Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesPredicate 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 ...
Abstraction refinement for termination
SAS'05: Proceedings of the 12th international conference on Static AnalysisAbstraction can often lead to spurious counterexamples. Counterexample-guided abstraction refinement is a method of strengthening abstractions based on the analysis of these spurious counterexamples. For invariance properties, a counterexample is a ...
Comments