The Community for Technology Leaders
Logic in Computer Science, Symposium on (2004)
Turku, Finland
July 13, 2004 to July 17, 2004
ISSN: 1043-6871
ISBN: 0-7695-2192-4
pp: 32-41
Andreas Podelski , Max-Planck-Institut f?r Informatik, Saarbr?cken, Germany
Andrey Rybalchenko , Max-Planck-Institut f?r Informatik, Saarbr?cken, Germany
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.
INDEX TERMS
null
CITATION
Andreas Podelski, Andrey Rybalchenko, "Transition Invariants", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 32-41, 2004, doi:10.1109/LICS.2004.1319598
92 ms
(Ver 3.3 (11022016))