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.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-540-23212-4
978-3-540-30210-0
Deharbe, D.; Imine, A.; Ranise, S.
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].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333185
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact