Transition invariants
Top Cited Papers
- 1 January 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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 relation is disjunctively well-founded if it is a finite union of well-founded relations. We characterize the validity of termination or another liveness property by the existence of a disjunctively well-founded transition invariant. The main contribution of our proof rule lies in its potential for automation via abstract interpretation.Keywords
This publication has 16 references indexed in Scilit:
- Temporal Verification of Reactive SystemsPublished by Springer Nature ,1995
- Progress measures and stack assertions for fair terminationPublished by Association for Computing Machinery (ACM) ,1992
- Completing the temporal pictureTheoretical Computer Science, 1991
- Verification of concurrent programs: the automata-theoretic framework*Annals of Pure and Applied Logic, 1991
- Automata on Infinite ObjectsPublished by Elsevier ,1990
- The complementation problem for Büchi automata with applications to temporal logicTheoretical Computer Science, 1987
- Systematic design of program analysis frameworksPublished by Association for Computing Machinery (ACM) ,1979
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977
- Axiomatic approach to total correctness of programsActa Informatica, 1974
- On a Problem of Formal LogicProceedings of the London Mathematical Society, 1930