An online proof-producing decision procedure for mixed-integer linear arithmetic

Abstract

Efficient decision procedures for arithmetic play a very important role in formal verification. In practical examples, however, arithmetic constraints are often mixed with constraints from other theories like the theory of arrays, Boolean satisfiability (SAT), bit-vectors, etc. Therefore, decision procedures for arithmetic are especially useful in combination with other decision procedures. The framework for such a combination is implemented at Stanford in the tool called Cooperating Validity Checker (CVC) [SBD02]. This work augments CVC with a decision procedure for the theory of mixed integer linear arithmetic based on the Omega-test [Pug91 ] extended to be online and proof producing. These extensions are the most important and challenging part of the work, and are necessary to make the combination efficient in practice. © Springer-Verlag Berlin Heidelberg 2003.