Abstraction-Driven Verification of Array Programs - Artificial Intelligence and Symbolic Computation - page 275

ground after the invocation of top ex . Both our system and Simplify are quite
successful in finding suitable instances to the quantified variables but our system
automatically discharges more proof obligations than Simplify .
We believe that the main reason for the success (measured in number of
proof obligations automatically discharged) of our algorithm over Simplify is that
we use superposition as the instantiation mechanism rather than the heuristic
matching algorithm described in [3]. In fact, superposition performs inferences
also on the quantified formulae: this may generate ground instances of facts
which are otherwise impossible to derive by requiring that at most one formula
participating to an inference is non-ground as it is the case for Simplify .
References
1. A. Armando, S. Ranise, and M. Rusinowitch. A Rewriting Approach to Satisfia-
bility Procedures. Info. and Comp. , 183(2):140-164, June 2003.
2. D. Deharbe and S. Ranise. Light-Weight Theorem Proving for Debugging and
Verifying Units of Code. In Proc. of the 1st Int. Conf. on Software Engineering
and Formal Methods (SEFM'03) . IEEE Computer Society Press, 2003.
3. D. Detlefs, G. Nelson, and J. B. Saxe. Simplify: A Theorem Prover for Program
Checking. Technical Report HPL-2003-148, HP Lab., 2003.
4. H. B. Enderton. A Mathematical Introduction to Logic . Academic Pr., 1972.
5. J.-C. Filliatre and N. Magaud. Certification of Sorting Algorithms in the System
Coq. In Theorem Proving in Higher Order Logics: Emerging Trends . 1999.
6. H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T):
Fast Decision Procedures. In Proc. of the 16th Int. Conf. on Computer Aided Ver-
ification (CAV'04) , LNCS. Springer, 2004.
7. G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures.
ACM TOPLAS , 1(2):245-257, 1979.
8. R. Nieuwenhuis and A. Rubio. Paramodulation-based theorem proving. In
A. Robinson and A. Voronkov, editors, Hand. of Automated Reasoning . 2001.
9. A. Nonnengart and C. Weidenbach. Handbook of Automated Reasoning , chapter
Computing Small Clause Normal Forms. Elsevier Science, 2001.
10. N. Suzuki and D. R. Jefferson. Verification Decidability of Presburger Array Pro-
grams. J. of the ACM , 27(1):191-205, 1980.
11. C. Tinelli and M. T. Harandi. A new correctness proof of the Nelson-Oppen combi-
nation procedure. In Front. of Combining Systems: Proc. of the 1st Int. Workshop ,
pages 103-120. Kluwer Academic Publishers, 1996.
12. P. van Hentenryck and T. Graf. Standard Forms for Rational Linear Arithmetics
in Constraint Logic Programming. Ann. of Math. and Art. Intell. , 5:303-319, 1992.