Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare 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]. Cited in 1 ReviewCited in 47 Documents MSC: 68Q60 Specification and verification (program logics, model checking, etc.) PDFBibTeX XMLCite \textit{H. Ganzinger} et al., Lect. Notes Comput. Sci. 3114, 175--188 (2004; Zbl 1103.68616) Full Text: DOI