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. |
|
|
|
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 |