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.	The Grasp paper by Joao Marques-Silva et al. The zCHAFF paper by Lintao Zhang et al. Survey paper on SAT solvers by Selman et al. History of Satisfiability by John Franco Handbook of Satisfiability. Edited by Biere, A., Heule, M., Van Maaren, H., Walsh, T.	SAT Live! Boolean SAT Solver competition website (benchmarks and tools) Boolean SAT/SMT Solver Summer school 2011 @ MIT organized by Vijay Ganesh and Daniel Leberre.	MiniSAT Solver Lingeling Solver
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.	Handbook of Satisfiability. Edited by Biere, A., Heule, M., Van Maaren, H., Walsh, T. STP and HAMPI websites CACM paper by Leo DeMoura and Nikolaj Bjorner	SMTLIB SMT competition website	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