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 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 counter-example guided abstraction refinement (CEGAR) framework. This has enabled verification of simple programs that cannot be checked using existing CEGAR based model checkers.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 2008
Accession Number
ADA476796

Entities

People

  • Edmund M. Clarke
  • Himanshu Jain
  • Orna Grumberg

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Air Platforms
  • C4I

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Coefficients
  • Computations
  • Computer Science
  • Computers
  • Equations
  • Inequalities
  • Integrals
  • Interpolation
  • Military Research
  • Notation
  • Numbers
  • Polynomials
  • Rational Numbers
  • Standards
  • Verification

Readers

  • Computer Programming and Software Development.
  • Mathematical Modeling and Probability Theory.
  • Research Science/Academic Research