Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


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

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-2003-2-004.ps386 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:
Hide details for BibTeXBibTeX
  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},