Princeton University
Computer Science Department

COS 516 / ELE 516
Automated Reasoning about Software

Aarti Gupta

Fall 2020
General Information | Schedule | Policies

The schedule may change during the semester. Please check it frequently.

Week/Dates Lectures Readings Homework
Week 1: Aug 31, Sept 2 Introduction, Propositional logic [BM Ch 1]
Week 2: Sept 7, 9 SAT solvers, First order logic [R1], [BM Ch 2-4] HW1 posted
Week 3: Sept 14, 16 First order logic, Satisfiability Modulo Theories (SMT) [R2], [R3]
Week 4: Sept 21, 23 SMT solvers, Binary Decision Diagrams, Transition systems [R4] HW2 posted
Week 5: Sept 28, 30 Model checking, Program verification [R5], [R6], [R7] HW3 posted
Week 6: Oct 5, 7 Program verification, Software model checking [BM Ch 5, 6], [R8] Project Outline due on Oct 9
Fall Break: Oct 12-13
Week 7: Oct 14
Software model checking tools, Midterm Exam review
Week 8: Oct 19
Oct 21		 Midterm Exam
Invariant generation
[BM Ch 12]
HW4 posted
Week 9: Oct 26, 28 CHC solvers, Program synthesis [R9] HW5 posted
Week 10: Nov 2, 4 Test generation, Network verification [R10]
Week 11: Nov 9
Nov 11		 DNN verification
Student project presentations
Week 12: Nov 16, 18
Student project presentations
Last class: Nov 23
Nov 25: Thanksgiving break		 Student Project Presentations
.
NO Final Exam Project report due on Dean's Date: December 8, 2020

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

References

[R1] Joao Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability, Chapter 4, 2008.
[R2] Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9, 2011.
[R3] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability, Chapter 12, 2008.
[R4] Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 100 (8), 677-691, 1986.
[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.
[R6] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu. Symbolic Model Checking without BDDs. In Proceedings of Tools and Algorithms for Construction and Analysis of Systems (TACAS) Conference 1999: 193-207.
[R7] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12, 10, 576-580, 1969.
[R8] Ranjit Jhala and Rupak Majumdar. Software model checking. ACM Computing Surveys 41, 4, Article 21, 2009.
[R9] Rajeev Alur, Rastislav Bodík, and others. Syntax-guided synthesis. In Proceedings of FMCAD 2013: 1-8.
[R10] Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker. A General Approach to Network Configuration Verification. In Proceedings of SIGCOMM 2017: 155-168.