English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Report

Software model checking of liveness properties via transition invariants

MPS-Authors
/persons/resource/persons45201

Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons45328

Rybalchenko,  Andrey
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-2003-2-004.pdf
(Any fulltext), 388KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Podelski, A., & Rybalchenko, A.(2003). Software model checking of liveness properties via transition invariants (MPI-I-2003-2-004). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-6AF8-9
Abstract
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.