Abstraction-Driven Verification of Array Programs

摘要

We describe a refutation-based theorem proving algorithm capable of checking the satisfiability of non-ground formulae modulo (a combination of) theories. The key idea is the use of abstraction to drive the application of (ⅰ) ground satisfiability checking modulo theories ax-iomatized by equational clauses, (ⅱ) Presburger arithmetic, and (ⅲ) quantifier instantiation. A prototype implementation is used to discharge the proof obligations necessary to show the correctness of some typical programs manipulating arrays. On these benchmarks, the prototype automatically discharge more proof obligations than Simplify - the prover of reference for program checking - thereby confirming the viability of our approach.