The schedule may change during the semester. Please check it frequently.
| Week/Dates |
Lectures |
Readings |
Homework |
| Week 1: Sept 4 |
Introduction, Propositional logic |
[BM Ch 1] |
|
| Week 2: Sept 9, 11 |
SAT solvers: DPLL, CDCL |
[R1] |
HW1 posted |
| Week 3: Sept 16, 18 |
First order logic, Satisfiability Modulo Theory (SMT) |
[BM Ch 2-4], [R2] |
HW2 posted |
| Week 4: Sept 23, 25 |
SMT solvers, Transition systems |
[R3] |
HW3 posted |
| Week 5: Sept 30, Oct 2 |
Model checking, SAT-based model checking |
[R4], [R5] |
|
| Week 6: Oct 7, 9 |
Program verification, Hoare logic |
[R6], [BM Ch 5, 6] |
HW4 posted |
| Week 6: Oct 10 |
|
|
Project Outline due |
| Fall Break: Oct 14, 16 |
|
|
|
Week 7: Oct 21
Week 7: Oct 23 |
Midterm Exam review, Program termination
Midterm Exam (in class) |
|
|
| Week 8: Oct 28, 30 |
Software model checking, Invariant generation |
[R7] |
|
| Week 9: Nov 4, 6 |
Program synthesis, Invariant synthesis |
[R8] |
|
| Week 10: Nov 11, 13 |
Security verification, Distributed systems verification |
[R9] |
|
| Week 11: Nov 18, 20 |
Network verification, DNN verification |
[R10] |
|
| Week 12: Nov 25 |
Student project presentations (in class) |
|
|
| Week 12: Nov 27 |
no class, Thanksgiving Break |
|
|
Week 13: Dec 2, 4
| Student project presentations (in class) |
|
|
| Week 14: Dec 13 |
Dean's date |
|
Project Report due |
| NO Final Exam |
|
|
|
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]
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]
[R5]
Armin Biere, Daniel Kröning.
SAT-Based Model Checking.
Handbook of Model Checking 2018: 277-303.
[
link]
[R6]
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12, 10, 576-580, 1969.
[
link]
[R7]
Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Computing Surveys 41, 4, Article 21, 2009.
[
link]
[R8]
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]
[R9]
Kenneth L. McMillan, Oded Padon.
Ivy: A Multi-modal Verification Tool for Distributed Algorithms.
In Proceedings of CAV (2) 2020: 190-202.
[
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]
