2005 International Conference on Computer Design (2005)
San Jose, California
Oct. 2, 2005 to Oct. 5, 2005
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICCD.2005.91
Anubhav Gupta , Carnegie Mellon University, Pittsburgh
Edmund Clarke , Carnegie Mellon University, Pittsburgh
<p>Abstraction techniques have been very successful in model checking large systems by enabling the model checker to ignore irrelevant details. Most abstraction techniques in literature are based on refinement. We introduce the notion of broken traces which capture the necessary and sufficient conditions for the existence of an error path in the abstract model. We formulate abstraction as learning the abstract model from samples of broken traces. Our iterative algorithm for abstraction-based model checking is not based on refinement and can generate the smallest abstract model that proves the property. We present an implementation of this algorithm for the verification of safety properties on gate-level net-lists with localization abstraction. Experimental results prove the viability of our techniques.</p>
E. Clarke and A. Gupta, "Reconsidering CEGAR: Learning Good Abstractions without Refinement," 2005 International Conference on Computer Design(ICCD), San Jose, California, 2005, pp. 591-598.