MPI-I-2003-2-004

Software model checking of liveness properties via transition invariants

Podelski, Andreas and Rybalchenko, Andrey

MPI-I-2003-2-004. December 2003, 29 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:

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.
Acknowledgement:
References to related material:

To download this research report, please select the type of document that fits best your needs.	Attachement Size(s):
	386 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView

URL to this document: http://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},}