Skip to Main content Skip to Navigation
Reports

BDD-Driven First-Order Satisfiability Procedures (Extended Version)

David Déharbe Silvio Ranise 1
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Providing a high degree of automation to discharge proof obligations in (fragments of) first-order logic is a crucial activity in many verification efforts. Unfortunately, this is quite a difficult task. On the one hand, reasoning modulo ubiquitous theories (such as lists, arrays, and Presburger arithmetic) is essential. On the other hand, to effectively incorporate this theory specific reasoning in boolean manipulations requires a substantial work. In this paper, we propose a simple technique to cope with such difficult- ies whose aim is to check the validity of universally quantified formulae with arbitrary boolean structure modulo an equational theory. Our approach combines BDDs with refutation theorem proving. The former allows us to compactly represent the boolean structure of formulae, the latter to effectively mechanize the reasoning in equational theories. We report some experimental results on formulae extracted from software verification efforts which confirm both the flexibility and the viability of our approach.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00071955
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 7:21:19 PM
Last modification on : Friday, January 15, 2021 - 3:24:35 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:46:07 PM

Identifiers

  • HAL Id : inria-00071955, version 1

Citation

David Déharbe, Silvio Ranise. BDD-Driven First-Order Satisfiability Procedures (Extended Version). [Research Report] RR-4630, INRIA. 2002, pp.24. ⟨inria-00071955⟩

Share

Metrics

Record views

253

Files downloads

354