# zbMATH — the first resource for mathematics

DPLL($$T$$): Fast decision procedures. (English) Zbl 1103.68616
Alur, Rajeev (ed.) et al., Computer aided verification. 16th international conference, CAV 2004, Boston, MA, USA, July 13–17, 2004. Proceedings. Berlin: Springer (ISBN 3-540-22342-8/pbk). Lecture Notes in Computer Science 3114, 175-188 (2004).
Summary: The logic of equality with uninterpreted functions (EUF) and its extensions have been widely applied to processor verification, by means of a large variety of progressively more sophisticated (lazy or eager) translations into propositional SAT. Here we propose a new approach, namely a general DPLL($$X)$$ engine, whose parameter $$X$$ can be instantiated with a specialized solver Solver$$_{T}$$ for a given theory $$T$$, thus producing a system DPLL($$T)$$. We describe this DPLL($$T)$$ scheme, the interface between DPLL($$X)$$ and Solver$$_{T}$$, the architecture of DPLL($$X)$$, and our solver for EUF, which includes incremental and backtrackable congruence closure algorithms for dealing with the built-in equality and the integer successor and predecessor symbols. Experiments with a first implementation indicate that our technique already outperforms the previous methods on most benchmarks, and scales up very well.
For the entire collection see [Zbl 1056.68003].

##### MSC:
 68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: