[pl-seminar] Talk by Leo Haller, today @ 4 PM in 4310 CS

[Thomas Reps <reps@xxxxxxxxxxx>]

This is a reminder about the PL Seminar talk today:

Abstract Conflict Driven Clause Learning
Date: Mon, 07/02/2012 - 4:00pm - 5:00pm Room: 4310 CS

Speaker Name: Leo Haller
Speaker Institution: Univ. of Oxford

  High performance propositional satisfiability
   solvers based on the Conflict Driven Clause Learning framework 
(CDCL) have
   been a major driver of research in areas such as verification and 
decision
   procedures. Modern satisfiability procedures are routinely applied to
   problems that were deemed intractable based on theoretical 
considerations
   15 years ago. Lifting the algorithmic lessons of CDCL to richer problem
   domains is a focus of ongoing research. In this talk, I show how one 
can
   generalise CDCL using lattice-theoretic abstractions to yield natural
   domain SMT procedures for logics and program verification problems. I
   leverage the simple insight that existing CDCL solvers can be
   characterised as logical abstract interpreters. The resulting Abstract
   CDCL (ACDCL) framework is a mathematical and algorithmic recipe for
   lifting CDCL by combining over- and underapproximate abstractions. I
   discuss the lattice-theoretic prerequisites of clause learning, give
   conditions for completeness and present two instantiations of ACDCL for
   program verification and SMT problems which significantly outperform
   existing techniques. This talk is based on joint work with Vijay 
D'Silva,
   Daniel Kroening, and Alberto Griggio.


[1] http://www.cs.wisc.edu/event/abstract-conflict-driven-clause-learning