Introduction to Boolean SAT/SMT solvers and their applications. Internals of modern SAT solvers. Internals of modern SMT solvers. Symbolic execution-based 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 | 2-3:15 PM | E5-4106/4128

Date
Lectures
Relevant Papers and Books
Relevant Websites
 Well-engineered 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 conflict-driven clause-learning (CDCL) SAT solvers. Techniques for Boolean propagation, conflict analysis, VSIDS branching heuristic, backjumping, two-watched 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: Bit-vectors, arrays, functions, strings, integer linear arithmetic, Peano arithmetic. Quantifiers.
  • Z3 from Microsoft Research
  • OpenSMT by Roberto Bruttomesso
  • STP and HAMPI from Stanford and MIT
  • CVC4 from NYU and U. of Iowa
Jan 23, 2013
Lecture 3: Introduction to Bounded Model Checking by Dr. Shoham Ben-David



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



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 higher-order 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: Solver-based 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: Model-checking revisited



May 1, 2013
Lecture 16: Proof-theoretic treatment of CDCL SAT solvers by Vijay Ganesh