[Pl-seminar] PL seminar schedule

[Aaron Turon]

NEU Programming Languages Seminar presents

Ian Johnson
Northeastern University

Wednesday, November 18, 2009
11:45-1:30
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

TITLE: SMT (Satisfiability Modulo Theories) Solver Theory and Applications

ABSTRACT:

SAT is a well-known NP-Complete problem, and there have been decades
of research in the area of creating efficient algorithms for deciding
it for practical applications. The best known algorithm for this is
the DPLL (Davis-Putnam-Logemann-Loveland) procedure, and there are
many derivatives that optimize the basic algorithm. The problem with
reducing every problem in hardware or some other NP-hard domain to a
SAT problem is that simple ideas, such as the associativity of
addition of n-wire bit vectors, explode into formulas so complex that
the current state of the art of SAT solvers falls to its knees. In
order to reason about problems in their own domain while leveraging
the power of SAT-solving technology, we have SMT, where instead of
boolean variables, a SAT solver decides satisfiability of
uninterpreted theory terms, and with a theory solver decides
satisfiability of a given complete/partial assignment.

This talk goes into more detail of the DPLL procedure and a general
framework for interacting with a theory solver in order to create an
SMT solver. If time allows, some commonly useful theories will be
discussed, as well as the theory of combining theories.

--

(Ed. note: SMT solvers are quickly becoming relevant to the PL
community as a fast and lightweight way to dispatch verification
conditions.  They are used in tools like Boogie, languages like Sage
(hybrid typing), type systems like Liquid Types, and Andy Gordon's
refinement type systems for e.g. security.  They also show up in
program analysis, e.g. Sorin Lerner's work.)