Cesare Tinelli's Publications
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. DPLL(T): Fast Decision Procedures. Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04), Boston, USA, 2004.
Abstract. The logic of equality with uninterpreted functions 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 for a given theory T, thus producing a system DPLL(T). We decribe this DPLL(T) scheme, the interface between DPLL(X) and the theory solver, 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.