Conference paper
Using cross-entropy for satisfiability
Hana Chockler, Alexander Ivrii, et al.
SAC 2013
Conference paper
K-induction without unrolling
Abstract
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.
Related
Nobuyuki Yoshioka, Mirko Amico, et al.
Nature Communications
Alexander Ivrii, Sharad Malik, et al.
Constraints
Raviv Gal, Haim Kermany, et al.
DAC 2020