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.
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
April 18 2008 11:00 a.m.
Location: ACES 2.402
Host: J. St
Talk Title: Satisfiability Modulo Theories
The Satisfiability Modulo Theories (SMT) problem is that
of checking the satisfiability of first-order formulas with
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
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
for quantifier instantiation in the context of SMT.
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
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
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.
- Awards & Honors
- About Us
- Student Engagement and Support
- Masters Program
- Ph.D. Program
- Financial Information
- Prospective Students
- Incoming Students
- Current Students
- Curricular Practical Training
- Grad Student Talks
- UTCS Direct