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].

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