K-induction without unrolling
Arie Gurfinkel, Alexander Ivrii · 2017
We present a flexible algorithmic framework KIC3 that combines IC3 and k-induction. The key underlying observation is that k-induction can be easily simulated by existing IC3 implementations by following a slightly different counterexample-queue management strategy.