Andreas Podelski
Andrey Rybalchenko
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 (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.
- T. Ball. A theory of predicate-complete test coverage and generation. In FMCO'2004: Symp. on Formal Methods for Components and Objects, LNCS. Springer, 2004. To appear. Google Scholar
Digital Library
- T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In PLDI'2001: Programming Language Design and Implementation, volume 36 of ACM SIGPLAN Notices, pages 203--213. ACM Press, 2001. Google Scholar
- T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstractions for model checking C programs. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of LNCS, pages 268--283. Springer, 2001. Google ScholarDigital Library
- F. Bourdoncle. Abstract debugging of higher-order imperative languages. In PLDI'1993: Programming Language Design and Implementation, pages 46--55. ACM Press, 1993. Google Scholar
- I. Browne, Z. Manna, and H. Sipma. Generalized verification diagrams. In FSTTCS'1995: Foundations of Software Technology and Theoretical Computer Science, volume 1026 of LNCS, pages 484--498. Springer, 1995. Google ScholarDigital Library
- S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In ICSE'2003: Int. Conf. on Software Engineering, pages 385--395, 2003. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV'2000: Computer Aided Verification, volume 1855 of LNCS, pages 154--169. Springer, 2000. Google ScholarDigital Library
- M. Colón and H. Sipma. Synthesis of linear ranking functions. In TACAS'2001: Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of LNCS, pages 67--81. Springer, 2001. Google ScholarDigital Library
- M. Colón and T. Uribe. Generating finite-state abstractions of reactive systems using decision procedures. In CAV'1998: Computer Aided Verification, volume 1427 of LNCS, pages 293--304. Springer, 1998. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'1977: Principles of Programming Languages, pages 238--252. ACM Press, 1977. Google Scholar
- P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In ICCL'1994: Int. Conf. on Computer Languages, pages 95--112. IEEE, 1994.Google ScholarCross Ref
- G. Delzanno and A. Podelski. Constraint-based deductive model checking. Int. Journal on Software Tools for Technology Transfer (STTT), 2000.Google Scholar
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL'2002: Principles of Programming Languages, pages 191--202. ACM Press, 2002. Google Scholar
- S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In CAV'1997: Computer Aided Verification, volume 1254 of LNCS, pages 72--83. Springer, 1997. Google ScholarDigital Library
- T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL'2002: Principles of Programming Languages, pages 58--70. ACM Press, 2002. Google Scholar
- Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, a special issue on Compositionality, 163(1):203--243, 2000. Google ScholarDigital Library
- Y. Kesten, A. Pnueli, and M. Y. Vardi. Verification by augmented abstraction: The automata-theoretic view. Journal of Computer and System Sciences, 62(4):668--690, 2001. Google ScholarDigital Library
- S. K. Lahiri, R. E. Bryant, and B. Cook. A symbolic approach to predicate abstraction. In CAV'2003: Computer Aided Verification, volume 2725 of LNCS, pages 141--153. Springer, 2003.Google ScholarCross Ref
- C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In POPL'2001: Principles of Programming Languages, volume 36, 3 of ACM SIGPLAN Notices, pages 81--92. ACM Press, 2001. Google Scholar
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: Safety. Springer, 1995. Google ScholarDigital Library
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: Progress. Draft, 1996. Google ScholarDigital Library
- A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,∞)-counter abstraction. In CAV'2002: Computer Aided Verification, volume 2404 of LNCS, pages 107--122. Springer, 2002. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI'2004: Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 239--251. Springer, 2004.Google ScholarCross Ref
- A. Podelski and A. Rybalchenko. Transition invariants. In LICS'2004: Logic in Computer Science, pages 32--41. IEEE, 2004. Google ScholarDigital Library
- F. P. Ramsey. On a problem of formal logic. In Proc. London Math. Soc., volume~30, pages 264--285, 1930.Google Scholar
- H. Sipma, T. Uribe, and Z. Manna. Deductive model checking. In CAV'1996: Computer Aided Verification, volume 1102 of LNCS, pages 208--219. Springer, 1996. Google ScholarDigital Library
- A. Tiwari. Termination of linear programs. In CAV'2004: Computer Aided Verification, volume 3114 of LNCS, pages 70--82. Springer, 2004.Google ScholarCross Ref
- T. Uribe. Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems. PhD thesis, Stanford University, 1999. Google ScholarDigital Library
- M. Y. Vardi. Verification of concurrent programs --- the automata-theoretic framework. Annals of Pure and Applied Logic, 51:79--98, 1991.Google ScholarCross Ref
- E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In POPL'2001: Principles of Programming Languages, pages 27--40. ACM Press, 2001. Google Scholar
- E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm. Verifying temporal heap properties specified via evolution logic. In ESOP'2003: European Symp. on Programming, volume 2618 of LNCS, pages 204--222. Springer, 2003. Google ScholarDigital Library
Index Terms
- Transition predicate abstraction and fair termination
Recommendations
Transition predicate abstraction and fair termination
Special issue on POPL 2005Predicate 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 ...
Automatic predicate abstraction of C programs
PLDI '01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementationModel checking has been widely successful in validating and debugging designs in the hardware and protocol domains. However, state-space explosion limits the applicability of model checking tools, so model checkers typically operate on abstractions of ...
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 ...
Comments