BDD-Driven First-Order Satisfiability Procedures (Extended Version)
Résumé
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.