Reconsidering Cegar: learning good abstractions without refinement

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.