Better generalization in IC3
- 1 October 2013
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
An improved clause generalization procedure for IC3 is presented. Whereas standard generalization extracts a relatively inductive clause from a single state, called a counterexample to induction (CTI), the new procedure also extracts such clauses from other states, called counterexamples to generalization (CTG), that interfere with the primary generalization attempt. The motivation is to enable IC3 to explore states farther from the error states than are CTIs while remaining property-focused. CTGs are strong candidates for being farther but still backward reachable. Significant reductions in the maximum depth reached by IC3's priority queue-directed explicit backward search indicate that this intention is achieved in practice. The effectiveness of the new procedure is established in two independent implementations of IC3, which demonstrate an increase of 17 and 27, respectively, in the number of solved HWMCC benchmarks.Keywords
This publication has 4 references indexed in Scilit:
- Exploiting step semantics for efficient bounded model checking of asynchronous systemsScience of Computer Programming, 2012
- SAT-Based Model Checking without UnrollingPublished by Springer Nature ,2011
- Checking Safety by Inductive Generalization of Counterexamples to InductionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2007
- Temporal Verification of Reactive SystemsPublished by Springer Nature ,1995