hide
Free keywords:
-
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.
