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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione
