AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
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

Transition invariants

LICS, pp.32-41, (2004)

Cited by: 326|Views110
EI WOS
Full Text
Bibtex
Weibo

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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Y. Fang, N. Piterman, A. Pnueli, and L. D. Zuck. Liveness with invisible ranking. In Steffen and Levi [20], pages 223– 238.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica, (3):243–263, 1974.
    Google ScholarLocate open access versionFindings
  • Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83(1):91–130, 1991.
    Google ScholarLocate open access versionFindings
  • Z. Manna and A. Pnueli. Temporal verification of reactive systems: Safety. Springer, 1995.
    Google ScholarFindings
  • Z. Manna and A. Pnueli. Temporal verification of reactive systems: Progress. Draft, 1996.
    Google ScholarLocate open access versionFindings
  • A. Podelski and A. Rybalchenko. Transition predicate abstraction. Draft. Available from the authors.
    Google ScholarFindings
  • A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In Steffen and Levi [20], pages 239–251.
    Google ScholarLocate open access versionFindings
  • F. P. Ramsey. On a problem of formal logic. In Proc. London Math. Soc., volume 30, pages 264–285, 1930.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • B. Steffen and G. Levi, editors. Proc. of VMCAI’2004: Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS. Springer, 2004.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • A. Tiwari. Termination of linear programs. In Proc. of CAV’2004: Computer Aided Verification, 2004. To appear.
    Google ScholarLocate open access versionFindings
  • M. Y. Vardi. Verification of concurrent programs — the automata-theoretic framework. Annals of Pure and Applied Logic, 51:79–98, 1991.
    Google ScholarLocate open access versionFindings
  • M. Y. Vardi. Rank predicates vs. progress measures in concurrent-program verification. Chicago Journal of Theoretical Computer Science, 1996.
    Google ScholarLocate open access versionFindings
Your rating :
0

 

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