Abstract
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 (i) ground satisfiability checking modulo theories axiomatized by equational clauses, (ii) Presburger arithmetic, and (iii) 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armando, A., Ranise, S., Rusinowitch, M.: A Rewriting Approach to Satisfiability Procedures. Info. and Comp. 183(2), 140–164 (2003)
Déharbe, D., Ranise, S.: 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 2003), IEEE Computer Society Press, Los Alamitos (2003)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Technical Report HPL-2003-148, HP Lab (2003)
Enderton, H.B.: A Mathematical Introduction to Logic. Academic Pr., London (1972)
Filliâtre, J.-C., Magaud, N.: Certification of Sorting Algorithms in the System Coq. In: Theorem Proving in Higher Order Logics: Emerging Trends (1999)
Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast Decision Procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 175–188. Springer, Heidelberg (2004)
Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM TOPLAS 1(2), 245–257 (1979)
Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Hand. of Automated Reasoning (2001)
Nonnengart, A., Weidenbach, C.: Handbook of Automated Reasoning, chapter Computing Small Clause Normal Forms. Elsevier Science, Amsterdam (2001)
Suzuki, N., Jefferson, D.R.: Verification Decidability of Presburger Array Programs. J. of the ACM 27(1), 191–205 (1980)
Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson–Oppen combination procedure. In: Front. of Combining Systems: Proc. of the 1st Int. Workshop, pp. 103–120. Kluwer Academic Publishers, Dordrecht (1996)
van Hentenryck, P., Graf, T.: Standard Forms for Rational Linear Arithmetics in Constraint Logic Programming. Ann. of Math. and Art. Intell. 5, 303–319 (1992)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Déharbe, D., Imine, A., Ranise, S. (2004). Abstraction-Driven Verification of Array Programs. In: Buchberger, B., Campbell, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2004. Lecture Notes in Computer Science(), vol 3249. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30210-0_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-30210-0_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23212-4
Online ISBN: 978-3-540-30210-0
eBook Packages: Springer Book Archive