The schedule may change during the semester. Please check it frequently.
| Week/Dates |
Lectures |
Readings |
Homework |
| Week 1: Sept 6 |
Introduction, Propositional logic |
[BM Ch 1] |
|
| Week 2: Sept 11, 13 |
SAT solvers: DPLL, CDCL |
[R1] |
HW1 posted |
| Week 3: Sept 18, 20 |
First order logic, Satisfiability Modulo Theory (SMT) solvers |
[BM Ch 2-4], [R2], [R3] |
HW2 posted |
| Week 4: Sept 25, 27 |
SMT solvers, Binary Decision Diagrams |
[R4] |
HW3 posted |
| Week 5: Oct 2, 4 |
Model checking, Bounded model checking |
[R5], [R6] |
|
| Week 6: Oct 9, 11 |
Program verification, Automating proofs |
[R7], [BM Ch 5, 6] |
HW4 posted |
|
|
|
Project Outline due on Oct 12 |
| Fall Break: Oct 16, 18 |
|
|
|
Week 7: Oct 23
Week 7: Oct 25 |
Midterm Exam review, Program termination
Midterm Exam (in class) |
|
|
| Week 8: Oct 30, Nov 1 |
Software model checking |
[R8] |
|
| Week 9: Nov 6, 8 |
Invariant inference, CHC solvers |
[BM Ch 12] |
HW5 posted |
| Week 10: Nov 13, 15 |
Program synthesis, Security verification |
[R9] |
|
| Week 11: Nov 20 |
Network verification |
[R10] |
|
| Week 11: Nov 22 (no class) |
Thanksgiving Break |
|
|
| Week 12: Nov 27, 29 |
DNN verification, Student project presentations |
|
|
Week 13: Dec 4, 6
| Student project presentations |
|
|
| NO Final Exam |
|
|
Project Report due on Dean's Date: December 15, 2023 |
Textbook
[BM Chapters 1-6, 12]
The Calculus of Computation: Decision Procedures with Applications to Verification
by Aaron R. Bradley and Zohar Manna
Electronic version
Readings
[R1]
João Marques-Silva, Sharad Malik.
Propositional SAT Solving. Handbook of Model Checking 2018: 247-275.
[
link]
[R2]
Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9, 2011.
[
link]
[R3]
Clark W. Barrett, Cesare Tinelli.
Satisfiability Modulo Theories.
Handbook of Model Checking 2018: 305-343.
[
link]
[R4]
Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 100 (8), 677-691, 1986.
[
link]
[R5]
E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8, 2 (April 1986), 244-263.
[
link]
[R6]
Armin Biere, Daniel Kröning.
SAT-Based Model Checking.
Handbook of Model Checking 2018: 277-303.
[
link]
[R7]
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12, 10, 576-580, 1969.
[
link]
[R8]
Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Computing Surveys 41, 4, Article 21, 2009.
[
link]
[R9]
Rajeev Alur, Rastislav Bodík, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa.
Syntax-guided synthesis. In Proceedings of FMCAD 2013: 1-8.
[
link]
[R10]
Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker.
A General Approach to Network Configuration Verification.
In Proceedings of SIGCOMM 2017: 155-168.
[
link]
