MPI-INF/SWS Research Reports 1991-2021
1. Author,Editor - 1. by Individual
MPI-I-2003-2-004
Software model checking of liveness properties via transition invariants
Podelski, Andreas and Rybalchenko, Andrey
December 2003, 29 pages.
.Status: available - back from printing
Model checking is an automated method to prove safety and liveness
properties for finite systems. Software model checking uses
predicate abstraction to compute invariants and thus
prove safety properties for infinite-state programs. We address the
limitation of current software model checking methods to safety
properties. Our results are a characterization of the validity of a
liveness property by the existence of transition invariants, and a
method that uses transition predicate abstraction to compute
transition invariants and thus prove liveness properties for
infinite-state programs.
-
- Attachement: MPI-I-2003-2-004.ps (386 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2003-2-004
BibTeX@TECHREPORT{PodelskiRybalchenko2003,
AUTHOR = {Podelski, Andreas and Rybalchenko, Andrey},
TITLE = {Software model checking of liveness properties via transition invariants},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Stuhlsatzenhausweg 85, 66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-2003-2-004},
MONTH = {December},
YEAR = {2003},
ISSN = {0946-011X},
}