Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations

DOI10.1007/s10703-009-0069-xzbMath1186.68013OpenAlexW2065748220MaRDI QIDQ1039847

Orna Grumberg, Edmund M. Clarke, Himanshu Jain

Publication date: 23 November 2009

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-009-0069-x

zbMATH Keywords

linear Diophantine equationsCraig interpolationabstraction refinementlinear Diophantine disequationslinear modular equations (linear congruences)proofs of unsatisfiability

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07) Linear Diophantine equations (11D04)

Related Items (1)

Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic

Uses Software

• PARI/GP
• Yices
• FOCI

Cites Work

• Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Abstractions from proofs
• Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
• Simplification by Cooperating Decision Procedures
• Lower bounds for resolution and cutting plane proofs and monotone computations
• Automated Deduction – CADE-20
• Constraint Solving for Interpolation
• Efficient Interpolant Generation in Satisfiability Modulo Theories
• Lazy Abstraction with Interpolants
• Tools and Algorithms for the Construction and Analysis of Systems
• Computer Aided Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations