UTCS Colloquium: Clark W. Barrett/Dept. of Computer Science New York University Satisfiability Modulo Theories ACES 2.402 Friday April 18 2008 11:00 a.m.

Contact Name: 
Jenna Whitney
Apr 18, 2008 11:00am - 12:00pm

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

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

Computer Science and Electrical Engineering from Brigham

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

ing the Stanford Validity Checker (SVC) and its successor
the Coopera

ting Validity Checker (CVC). His current research
includes work on a n

ew version of CVC called CVC3 as well as
applications of CVC3 to hard

ware and software verification.