*banner
 

Automated Extraction of Inductive Invariants to Aid Model Checking
Mike Case

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

©2002-2018 Chess