Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
Abstract elided by the publisher.
Related papers
- Efficient Interpolant Generation in Satisfiability Modulo Theories TACAS 2008
- Local Search for SMT on Linear Integer Arithmetic CAV 2022
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions TACAS 2015
- Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic TACAS 2020
- Interpolation and Model Checking for Nonlinear Arithmetic CAV 2021
- A Sorted Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic TACAS 2022
- Disjunctive Interpolants for Horn-Clause Verification CAV 2013
- Formalization of a Proof Calculus for Incremental Linearization for Satisfiability Modulo Nonlinear Arithmetic and Transcendental Functions CPP 2026