## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Transition invariants

LICS, pp.32-41, (2004)

EI WOS

Keywords

Abstract

Proof rules for program verification rely on auxiliary assertions. We propose a (sound and relatively complete) proof rule whose auxiliary assertions are transition invariants. A transition invariant of a program is a binary relation over program states that contains the transitive closure of the transition relation of the program. A rela...More

Code:

Data:

Introduction

- Temporal verification of concurrent programs is an active research topic; for entry points to the literature see e.g. [6, 9, 11, 13, 14, 15, 23].
- [11]
- The application of these proof rules requires the construction of auxiliary assertions.
- This construction is generally considered hard to automate, especially when ranking functions and well-founded orderings are involved.
- The authors propose a proof rule whose auxiliary assertions are transition invariants.
- The authors introduce the notion of a transition invariant as a binary relation over program states that contains the transitive closure of the transition relation of the program.
- The authors formulate an inductiveness principle for transition invariants.

Highlights

- Temporal verification of concurrent programs is an active research topic; for entry points to the literature see e.g. [6, 9, 11, 13, 14, 15, 23]
- In the unifying automatatheoretic framework of [23], a temporal proof is reduced to the proof of fair termination, which again can be done using deductive proof rules, e.g. [11]
- We propose a proof rule whose auxiliary assertions are transition invariants
- We introduce the notion of a transition invariant as a binary relation over program states that contains the transitive closure of the transition relation of the program
- We have presented a proof rule for the temporal verification of concurrent programs
- Our conceptual contribution is the notion of a transition invariant, and its usefulness in temporal proofs

Conclusion

- In a well-chosen instantiation, this proof rule allows one to decompose the verification problem into a number of independent smaller verification problems: one for establishing a transition invariant, and the others for establishing the disjunctive well-foundedness.
- The former is done in a way that is reminiscent of establishing state invariants, using a familiar inductive reasoning.
- It allows one to account for Buchi accepting conditions in a direct way, namely by intersecting relations

Related work

- There is a large body of work on proof rules for liveness properties of concurrent programs, see [6, 11, 13, 15]. They all rely on auxiliary well-founded (lexicographic) orderings for the transition relation, and not on independent orderings for sub-relations, as in our approach.

The automata-theoretic approach for verification of concurrent programs [23] reduces the verification problem to proving termination. It leaves open how to prove termination. We indicate one possible way.

A rank predicate [24] (a notion directly related to progress measures [9]) proves fair termination of a program if the rank does not increase in every computation step and decreases in the accepting states. In a disjunctively wellfounded transition invariant a rank need not decrease in all sub-relations if an accepting state is visited, i.e., the rank of one sub-relation must decrease and all other ranks may increase.

Funding

- This work was partly supported by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS) and by the German Federal Ministry of Education and Research (BMBF) in the framework of the Verisoft project under grant 01 IS C38

Reference

- T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proc. of PLDI’2001: Programming Language Design and Implementation, volume 36 of ACM SIGPLAN Notices, pages 203–213. ACM Press, 2001.
- B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proc. of PLDI’2003: Programming Language Design and Implementation, pages 196–207. ACM Press, June 7–14 2003.
- S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In Proc. of ICSE’2003: Int. Conf. on Software Engineering, pages 385– 395, 2003.
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of POPL’1977: Principles of Programming Languages, pages 238–252. ACM Press, 1977.
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. of POPL’1979: Principles of Programming Languages, pages 269–282. ACM Press, 1979.
- Y. Fang, N. Piterman, A. Pnueli, and L. D. Zuck. Liveness with invisible ranking. In Steffen and Levi [20], pages 223– 238.
- S. Graf and H. Saıdi. Construction of abstract state graphs with PVS. In Proc. of CAV’1997: Computer Aided Verification, volume 1254 of LNCS, pages 72–83.
- T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. In Proc. of POPL’2002: Principles of Programming Languages, pages 58–70. ACM Press, 2002.
- N. Klarlund. Progress measures and stack assertions for fair termination. In Proc. of PODC’1992: Principles of Distributed Computing, pages 229–240. ACM Press, 1992.
- C. S. Lee, N. D. Jones, and A. M. Ben-Amram. The size-change principle for program termination. In Proc. of POPL’2001: Principles of Programming Languages, volume 36, 3 of ACM SIGPLAN Notices, pages 81–92. ACM Press, 2001.
- D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. In Proc. of ICALP’1981: Int. Colloq. on Automata, Languages and Programming, volume 115 of LNCS, pages 264–277.
- Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica, (3):243–263, 1974.
- Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83(1):91–130, 1991.
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: Safety. Springer, 1995.
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: Progress. Draft, 1996.
- A. Podelski and A. Rybalchenko. Transition predicate abstraction. Draft. Available from the authors.
- A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In Steffen and Levi [20], pages 239–251.
- F. P. Ramsey. On a problem of formal logic. In Proc. London Math. Soc., volume 30, pages 264–285, 1930.
- P. A. Sistla, M. Y. Vardi, and P. Wolper. The complementation problem for Buchi automata with applications to temporal logic. Theoretical Computer Science, 49(2–3):217–237, 1987.
- B. Steffen and G. Levi, editors. Proc. of VMCAI’2004: Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS. Springer, 2004.
- W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics, pages 133– 192. Elsevier and MIT Press, 1990.
- A. Tiwari. Termination of linear programs. In Proc. of CAV’2004: Computer Aided Verification, 2004. To appear.
- M. Y. Vardi. Verification of concurrent programs — the automata-theoretic framework. Annals of Pure and Applied Logic, 51:79–98, 1991.
- M. Y. Vardi. Rank predicates vs. progress measures in concurrent-program verification. Chicago Journal of Theoretical Computer Science, 1996.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn