IC3-Guided Abstraction

Abstract-Localization is a powerful automated abstraction-refinement technique to reduce the complexity of property checking. This process is often guided by SATbased bounded model checking, using counterexamples obtained on the abstract model, proofs obtained on the original model, or a combination of both to select irrelevant logic. In this paper, we propose the use of bounded invariants obtained during an incomplete IC3 run to derive higher-quality abstractions for complex problems. Experiments confirm that this approach yields significantly smaller abstractions in many cases, and that the resulting abstract models are often easier to verify