Citation
Mike Case. "Automated Extraction of Inductive Invariants to Aid Model Checking". Talk or presentation, 10, April, 2007.

Abstract
Many applications, specifically formal model checking, can be aided by inductive invariants, small local properties that can be proved by simple induction. In this work 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 compute, and many invariants can be shown to not be helpful to model checking. In this work, we find invariants to show that a specific targeted state is unreachable. In this way, we can provide a calling application with specific invariants that are few in number and immediately help the problem at hand. This method is applied to interpolation, a state of the art model checker, where invariants are used to refute an error trace to help discard spurious counterexamples.

Electronic downloads

• MikeCaseDesSeminar.ppt · application/vnd.ms-powerpoint · 491 kbytes

• HTML

  Mike Case. <a
  href="http://chess.eecs.berkeley.edu/pubs/269.html"
  ><i>Automated Extraction of Inductive Invariants to
  Aid Model Checking</i></a>, Talk or
  presentation,  10, April, 2007.

• Plain text

  Mike Case. "Automated Extraction of Inductive
  Invariants to Aid Model Checking". Talk or
  presentation,  10, April, 2007.

• BibTeX

  @presentation{Case07_AutomatedExtractionOfInductiveInvariantsToAidModelChecking,
      author = {Mike Case},
      title = {Automated Extraction of Inductive Invariants to
                Aid Model Checking},
      day = {10},
      month = {April},
      year = {2007},
      abstract = {Many applications, specifically formal model
                checking, can be aided by inductive invariants,
                small local properties that can be proved by
                simple induction. In this work 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 compute, and
                many invariants can be shown to not be helpful to
                model checking. In this work, we find invariants
                to show that a specific targeted state is
                unreachable. In this way, we can provide a calling
                application with specific invariants that are few
                in number and immediately help the problem at
                hand. This method is applied to interpolation, a
                state of the art model checker, where invariants
                are used to refute an error trace to help discard
                spurious counterexamples.},
      URL = {http://chess.eecs.berkeley.edu/pubs/269.html}
  }
  

Posted by Christopher Brooks on 29 May 2007.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.