Some Talks


Notice:The slides referenced on this page are included by the contributing authors as a means to ensure timely dissemination of technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors. Please acknowledge the authors when using these slides.  

(Talks listed in reverse chronological order. Most of these are powerpoint presentations.)
 

UCLID: Deciding Combinations of Theories via Eager Translation to SAT. Introduction and Part II on Integer Linear Arithmetic. [ppt]
Stanford/SRI Summer School on Combination of Decision Procedures, August 10, 2004.
(Earlier versions of this talk were given at MIT CSAIL, at LICS'04, and at the SVC meeting on July 6, 2004.)

 
First-Order Decision Procedures Based on Eager SAT-Encodings. [ppt]
Seminar at the Tata Institute of Fundamental Research, Mumbai, January 2, 2004.

 
Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. [ppt]
15th Intl. Conference on Computer-Aided Verification, July 10, 2003.

 
A Hybrid SAT-based Decision Procedure for Separation Logic with Uninterpreted Functions. [ppt]
40th Design Automation Conference, June 4, 2003.
(Earlier version given at the SVC meeting on May 27, 2003.)

 
Translating Quantified Separation Logic to Quantified Boolean Logic. [ppt]
Invited talk at Dagstuhl Seminar on Deduction and Infinite-State Model Checking, April 24, 2003.
(Earlier version given at the SVC meeting on April 15, 2003.)

 
A SAT-based Decision Procedure for Infinite-State System Verification. [ppt]
Seminar at Microsoft Research, Redmond, November 8, 2002.

 
Modeling and Verifying Systems using CLU Logic. [ppt]
14th Intl. Conference on Computer-Aided Verification, July 28, 2002.

 
Modular Verification of Multithreaded Software. [ppt]
SCS Student Seminar Series, April 12, 2002.
(This talk is aimed at a general CS audience. For a more technical version, see my co-author Cormac Flanagan's slides from CAV'02.)

 

Posters
 

Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean Methods. [pdf]
ARO funding meeting, May 1, 2003.