Search

• < Previous
• 1
• Next >

---

Reasoning with Finite Sets and Cardinality Constraints in SMT

Kshitij Bansal ; Clark Barrett ; Andrew Reynolds ; Cesare Tinelli.

We consider the problem of deciding the satisfiability of quantifier-free formulas in the theory of finite sets with cardinality constraints. Sets are a common high-level data structure used in programming; thus, such a theory is useful for modeling program constructs directly. More importantly,&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;]

---