Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations

DOI10.1007/978-3-540-70545-1_24zbMath1155.68439OpenAlexW1882377980MaRDI 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

Mathematics Subject Classification ID

Decidability (number-theoretic aspects) (11U05) Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Related Items (9)

A layered algorithm for quantifier elimination from linear modular constraints ⋮ Interpolation and Model Checking ⋮ An interpolating sequent calculus for quantifier-free Presburger arithmetic ⋮ Cuts from proofs: a complete and practical technique for solving linear inequalities over integers ⋮ Interpolants for Linear Arithmetic in SMT ⋮ An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic ⋮ Interpolant Generation for UTVPI ⋮ Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic ⋮ Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations

This page was built for publication: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations