« zurück

Kolloquium | Olga Tveretina | 21.04.2004

MZH 5210 | 17.00 Uhr c.t.

DPLL-based Procedure for Equality Logic with Uninterpreted Functions

Olga Tveretina | Department of Computer Science, Technical University of Eindhoven, The Netherlands

The logic of equality with uninterpreted functions (EUF) has been proposed for verifying abstract hardware designs. Fast satisfiability checking over this logic is important for such verification to be successful. In the past several years various procedures for checking satisfiability of such formulas have been suggested. Mainly they are based on transforming a formula in this logic to a propositional one, which is checked by a SAT solver for satisfiability. We are working on a general procedure for EUF, and some optimizations of it, without translating into SAT. Our algorithm is based on the Davis-Putman-Logemann-Loveland (DPLL) procedure, one of the most effective methods to check propositional satisfiability. Being based on the DPLL procedure, our algorithm can adopt heuristics developed for this method. Therefore it can be used as the formal basis for an efficient implementations for satisfiability checkers for EUF.