Satisfiability solving for software verification

被引：1

作者：

David Déharbe

Silvio Ranise

机构：

[1] DIMAp/UFRN,Dip. di Informatica

[2] Università di Verona,undefined

来源：

International Journal on Software Tools for Technology Transfer | 2009年 / 11卷 / 3期

关键词：

Software verification; Equational theorem proving; Boolean solving; Theory reasoning;

D O I：

10.1007/s10009-009-0105-6

中图分类号：

学科分类号：

摘要：

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.

引用

页码：255 / 260

页数：5

共 17 条

[1]

Armando A.(2003)A rewriting approach to satisfiability procedures Inf. Comput. 183 140-164

[2]

Ranise S.(1988)Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic Mach. Intell. 11 83-124

[3]

Rusinowitch M.(2003)Scalable automated proving and debugging of set-based specifications J. Braz. Comput. Soc. 9 17-36

[4]

Boyer R.(2005)Simplify: a theorem prover for program checking JACM 52 365-473

[5]

Moore J.S.(2005)Superposition with equivalence reasoning and delayed clause normal form transformation Inf. Comput. 199 3-23

[6]

Couchot J.F.(1980)Fast decision procedures based on congruence closure J. ACM 27 356-364

[7]

Déharbe D.(2007)Lazy satisfiability modulo theories J. Satisf. Boolean Modeling Comput. 3 141-224

[8]

Giorgetti A.(undefined)undefined undefined undefined undefined-undefined

[9]

Ranise S.(undefined)undefined undefined undefined undefined-undefined

[10]

Detlefs D.(undefined)undefined undefined undefined undefined-undefined

← 1 2 →