MPI-INF Logo
MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2

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.

  • MPI-I-2003-2-004.ps
  • Attachement: MPI-I-2003-2-004.ps (386 KBytes)

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/2003-2-004

Hide details for BibTeXBibTeX
@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},
}