Introduction
to Boolean SAT/SMT solvers and their applications. Internals of modern SAT solvers. Internals
of modern SMT solvers. Symbolic executionbased testing. Model
checking. Application of solvers to program analysis/synthesis. SAT/SMT
solvers in programming language design. SAT/SMT solvers in
AI.
Date  Time  Place: Wednesdays  23:15 PM  E54106/4128
Date 
Lectures 
Relevant Papers and Books 
Relevant Websites  Wellengineered SAT, SMT solvers and their applications 
Jan 9,2013 
Lecture 1: Introduction
to SAT solvers. Motivation for using SAT solvers in formal
methods, testing, program analysis, synthesis. Internals of
conflictdriven clauselearning (CDCL) SAT solvers. Techniques for
Boolean propagation,
conflict analysis, VSIDS branching heuristic, backjumping, twowatched
literal scheme. 

 
Jan 16, 2013 
Lecture 2: Introduction to SMT solvers.
Core ideas: DPLL(T), combination of decision procedures, lazy vs. eager
encoding. Important SMT theories: Bitvectors, arrays, functions,
strings, integer linear arithmetic, Peano arithmetic. Quantifiers. 



Jan 23, 2013 
Lecture 3: Introduction to Bounded Model Checking by Dr. Shoham BenDavid 

Jan 30, 2013 
Lecture 4: Introduction to IC3 model checking algorithm by Dr. Shoham BenDavid 

Feb 6, 2013 
No Class 

Feb 13, 2013 
Lecture 5: Requirement analysis and software modelling by Rafael Olaechea 

Feb 20, 2013 
Lecture 6: Solvers for computer security and cryptography by Alireza Sharifi 

Feb 27, 2013 
Lecture 7: Internals of MiniSAT by Frank Imeson 

March 6, 2013 
Lecture 8: Constraint programming by Professor Peter Van Beek 

March 13, 2013 
Lecture 9: Solvers and higherorder theorem proving by Leopoldo Motta Teixeira  
March 20, 2013 
Lecture 10: Concolic testing (aka dynamic symbolic testing) by Sandy Beidu 

March 27, 2013 
Lecture 11: Complexity theory talk by Professor Raman 

April 3, 2013 
Lecture 12: Debugging tools based on symbolic execution and solvers by Lei Zhang 

April 10, 2013 
Lecture 13: Solverbased program analysis for security testing and repair by Professor Frank Tip 

April 17, 2013 
Lecture 14: Solvers in program analysis 

April 24, 2013 
Lecture 15: Modelchecking revisited 

May 1, 2013 
Lecture 16: Prooftheoretic treatment of CDCL SAT solvers by Vijay Ganesh 