Declarative techniques for software verification require the availability of scalable, predictable, and flexible satisfiability solvers. We describe our approach to build such solvers by combining equational theorem proving, Boolean solving, arithmetic reasoning, and some transformations of the proof obligations. The proposed techniques have been implemented in a system called haRVey and the viability of the approach is shown on proof obligations generated in the certification of aerospace code. © Springer-Verlag 2009.

Satisfiability solving for software verification / Deharbe, D.; Ranise, S.. - In: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. - ISSN 1433-2779. - 11:3(2009), pp. 255-260. [10.1007/s10009-009-0105-6]

Satisfiability solving for software verification

Ranise S.
2009-01-01

Abstract

Declarative techniques for software verification require the availability of scalable, predictable, and flexible satisfiability solvers. We describe our approach to build such solvers by combining equational theorem proving, Boolean solving, arithmetic reasoning, and some transformations of the proof obligations. The proposed techniques have been implemented in a system called haRVey and the viability of the approach is shown on proof obligations generated in the certification of aerospace code. © Springer-Verlag 2009.
2009
3
Deharbe, D.; Ranise, S.
Satisfiability solving for software verification / Deharbe, D.; Ranise, S.. - In: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. - ISSN 1433-2779. - 11:3(2009), pp. 255-260. [10.1007/s10009-009-0105-6]
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/333080
 Attenzione

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

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