Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
From MaRDI portal
Publication:3512498
DOI10.1007/978-3-540-70545-1_24zbMath1155.68439MaRDI QIDQ3512498
Orna Grumberg, Himanshu Jain, Edmund M. Clarke
Publication date: 15 July 2008
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_24
11U05: Decidability (number-theoretic aspects)
68Q60: Specification and verification (program logics, model checking, etc.)
03C40: Interpolation, preservation, definability
Related Items
Interpolant Generation for UTVPI, An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic, Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic, An interpolating sequent calculus for quantifier-free Presburger arithmetic, Cuts from proofs: a complete and practical technique for solving linear inequalities over integers, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, A layered algorithm for quantifier elimination from linear modular constraints, Interpolation and Model Checking, Interpolants for Linear Arithmetic in SMT