There is a signup schedule for this event (UT EID required).

Type of Talk: UTCS Colloquium

Speaker/Affiliation: Clark W. Barre

tt/Dept. of Computer Science/New York University

Date/Time: Friday
April 18 2008 11:00 a.m.

Location: ACES 2.402

Host: J. St

rother Moore

Talk Title: Satisfiability Modulo Theories

Talk
Abstract:
The Satisfiability Modulo Theories (SMT) problem is that

of checking the satisfiability of first-order formulas with
respect to

some logical theory T of interest. This talk will
start with some moti

vation and applications of SMT. I will
briefly review the theoretical f

ramework for SMT and then
discuss some of the main issues involved in c

reating a
practical implementation in particular the need for and
implementation of fast Boolean reasoning. The talk will
also cover so

me of our recent work such as the
implementation of non-convex theories
and strategies
for quantifier instantiation in the context of SMT.

Speaker Bio:
Clark Barrett received his bachelor''s degree in Mathem

atics
Computer Science and Electrical Engineering from Brigham
Yo

ung University in 1995. He received his PhD from Stanford
University a

nd joined the faculty of New York University in the
Fall of 2002.
Professor Barrett is the co-author of a number of SMT systems
includ

ware and software verification.