Sciweavers

FMCAD
2007
Springer

Automated Extraction of Inductive Invariants to Aid Model Checking

13 years 9 months ago
Automated Extraction of Inductive Invariants to Aid Model Checking
Abstract— Model checking can be aided by inductive invariants, small local properties that can be proved by simple induction. We present a way to automatically extract inductive invariants from a design and then prove them. The set of candidate invariants is broad, expensive to prove, and many invariants can be shown to not be helpful to model checking. In this work, we develop a new method for systematically exploring the space of candidate inductive invariants, which allows us to find and prove invariants that are few in number and immediately help the problem at hand. This method is applied to interpolation where invariants are used to refute an error trace and help discard spurious counterexamples.
Michael L. Case, Alan Mishchenko, Robert K. Brayto
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FMCAD
Authors Michael L. Case, Alan Mishchenko, Robert K. Brayton
Comments (0)