Search

• < Previous
• 1
• Next >

---

Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

Alberto Griggio ; Thi Thieu Hoa Le ; Roberto Sebastiani.

The problem of computing Craig interpolants in SAT and SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for interpolant generation have been presented for some theories of interest ---including that of equality and uninterpreted&nbsp;[&hellip;]

---

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays

Makai Mann ; Ahmed Irfan ; Alberto Griggio ; Oded Padon ; Clark Barrett.

We develop a framework for model checking infinite-state systems by automatically augmenting them with auxiliary variables, enabling quantifier-free induction proofs for systems that would otherwise require quantified invariants. We combine this mechanism with a counterexample-guided abstraction&nbsp;[&hellip;]

---