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. ©Sorineer-Verlae 2004.
Abstraction-Driven Verification of Array Programs / Deharbe, D.; Imine, A.; Ranise, S.. - 3249:(2004), pp. 271-275. (Intervento presentato al convegno AISC tenutosi a Austria nel 22-24/09/2004) [10.1007/978-3-540-30210-0_23].
Abstraction-Driven Verification of Array Programs
Ranise S.
2004-01-01
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. ©Sorineer-Verlae 2004.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
