CMU-CS-08-102
Computer Science Department
School of Computer Science, Carnegie Mellon University



CMU-CS-08-102

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

Himanshu Jain, Edmund M. Clarke, Orna Grumberg*
February 2008

CMU-CS-08-102.pdf


Keywords: Craig interpolation, proofs of unsatisfiability, linear diophantine equations, linear modular equations (linear congruences), linear diophantic disequations, abstraction refinement

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 proofs of unsatisfiability and interpolants for conjunctions of linear diophantine equations, linear modular equations (linear congruences), 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.

39 pages

*Department of Computer Science, Technion-Israel Institute of Technology


Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu