Property-directed k-induction

Abstract

IC3 and k-induction are commonly used in automated analysis of infinite-state systems. We present a reformulation of IC3 that separates reachability checking from induction reasoning. This makes the algorithm more modular, and allows us to integrate IC3 and k-induction. We call this new method property-directed k-induction (pd-kind). We show that k-induction is more powerful than regular induction, and that, modulo assumptions on the interpolation method, pd-kind is more powerful than k-induction. Moreover, with k-induction as the invariant generation back-end of IC3, the new method can produce more concise invariants. We have implemented the method in the sally model checker. We present empirical results to support its effectiveness.