CMU-CS-08-102Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-08-102
Himanshu Jain, Edmund M. Clarke, Orna Grumberg*
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 39 pages *Department of Computer Science, Technion-Israel Institute of Technology
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |