Skip to Main content Skip to Navigation

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 :
Complete list of metadata
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 7:21:19 PM
Last modification on : Friday, January 21, 2022 - 3:09:03 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:46:07 PM


  • HAL Id : inria-00071955, version 1


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



Record views


Files downloads