University of Iowa/h3>
The first part of this talk introduces Abstract DPLL, a
general rule-based formulation of the Davis-Putnam-Logemann-Loveland
(DPLL) procedure, one of the most successful decision procedures for
propositional satisfiability. Abstract DPLL allows one to model and
formally reason about several DPLL variants and enhancements in a
simple way. Its main properties, such as soundness, completeness or
termination, immediately carry over to modern DPLL implementations
with such advanced features as non-chronological backtracking, lemma
learning, and restarts. The second part of the talk extends the
framework to Satisfiability Modulo Theories (SMT), the problem of
determining the satisfiability of quantifier-free formulas in the
context of logical theories of interest. Abstract DPLL Modulo
Theories allows one to formalize a family of SMT techniques that
couple a DPLL engine, a generic DPLL-style SAT solver, with a theory
solver, a procedure for deciding the satisfiability of sets of
literals in a background theory T.
This is joint work with Robert Nieuwenhuis and Albert Oliveras of the
Technical University of Catalonia, and with Clark Barrett of New York
University.
Bio: Dr. Tinelli is an associate professor of Computer Science at
the University of Iowa. He received a PhD in Computer Science from
UIUC in 1999. His work mainly concentrates on constraint-based
approaches and combination methods in automated reasoning, and their
applications to formal verification. His research interests include
automated reasoning, formal methods, foundations of programming
languages, and applications of logic in computer science. In 2003,
Dr. Tinelli received an NSF CAREER award for a project on improving
extended static checking of software by means of advanced automated
reasoning techniques. He co-leads an international initiative, called
SMT-LIB, supported by several research groups in academia and
industry, aimed at producing various common standards for SMT
applications as well as a large library of benchmarks. Dr. Tinelli
has served in the program committee of several conferences and
workshops, inclunding CADE, LPAR, FroCoS, PDPAR, and ECAI. He is
currently a steering committee member of IJCAR, FTP, and FroCoS, and a
trustee of CADE Inc.
Deepak Ramachandran
Last modified: Mon Apr 3 15:42:04 CDT 2006