CINECA IRIS Institutional Research Information System
IRIS è l’archivio della produzione scientifica della Fondazione Bruno Kessler.
EnglishDeclarative 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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte di FBK.
| Titolo: | Satisfiability solving for software verification |
| Autori: | |
| Data di pubblicazione: | 2009 |
| Rivista: | |
| 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. |
| Handle: | http://hdl.handle.net/11582/22073 |
| Appare nelle tipologie: | 1.1 Articolo in rivista |
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Utilizza questo identificativo per citare o creare un link a questo documento:
http://hdl.handle.net/11582/22073
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
Copyright © 2018