Sciweavers

CAV
2008
Springer

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

13 years 5 months ago
Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations
Abstract. The use of Craig interpolants has enabled the development of powerful hardware and software model checking techniques. Efficient algorithms are known for computing interpolants in rational and real linear arithmetic. We focus on subsets of integer linear arithmetic. Our main results are polynomial time algorithms for obtaining interpolants for conjunctions of linear diophantine equations, linear modular equations, and linear diophantine disequations. We show the utility of the proposed interpolation algorithms for discovering modular/divisibility predicates in a counterexample guided abstraction refinement (CEGAR) framework. This has enabled verification of simple programs that cannot be checked using existing CEGAR based model checkers.
Himanshu Jain, Edmund M. Clarke, Orna Grumberg
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CAV
Authors Himanshu Jain, Edmund M. Clarke, Orna Grumberg
Comments (0)