Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic
From MaRDI portal
Publication:5892495
DOI10.1007/978-3-642-19835-9_13zbMath1315.68179arXiv1010.4422MaRDI QIDQ5892495
Roberto Sebastiani, Alberto Griggio, Thi Thieu Hoa le
Publication date: 19 May 2011
Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1010.4422
68Q60: Specification and verification (program logics, model checking, etc.)
03B25: Decidability of theories and sets of sentences
03C40: Interpolation, preservation, definability
Related Items
Complete instantiation-based interpolation, An interpolating sequent calculus for quantifier-free Presburger arithmetic, Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic, Interpolation and Model Checking
Uses Software
Cites Work
- Unnamed Item
- Constraint solving for interpolation
- An interpolating theorem prover
- Efficient generation of craig interpolants in satisfiability modulo theories
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
- Interpolants for Linear Arithmetic in SMT
- Ground Interpolation for the Theory of Equality
- Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers
- Lower bounds for resolution and cutting plane proofs and monotone computations
- Interpolating Quantifier-Free Presburger Arithmetic
- Ground Interpolation for Combined Theories
- Splitting on Demand in SAT Modulo Theories
- Automated Deduction – CADE-20
- An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic
