Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic

DOI10.1007/978-3-642-19835-9_13zbMath1315.68179arXiv1010.4422OpenAlexW2114754094MaRDI 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

Mathematics Subject Classification ID

Related Items (5)

Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic ⋮ Interpolation and Model Checking ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ Complete instantiation-based interpolation ⋮ Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Uses Software

• Princess
• FOCI

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

This page was built for publication: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic