Princeton University
Computer Science Department

COS 516 / ELE 516
Automated Reasoning about Software

Aarti Gupta

Fall 2019
General Information | Schedule | Policies

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

Week/Dates Lectures Readings Homework
Week 0: Sept 11 Introduction, Course overview
Week 1: Sept 16, 18 Propositional logic, SAT solvers [BM Ch 1], [R1] HW1 posted
Week 2: Sept 23, 25 First order logic, Satisfiability Modulo Theories (SMT) [BM Ch 2-4], [R2] HW2 posted
Week 3: Sept 30, Oct 2 SMT solvers, Binary Decision Diagrams [R3], [R4]
Week 4: Oct 7, 9 Model checking, Transition systems, Program verification [R5], [R6], [R7] HW3 posted
Week 5: Oct 14, 16 Program verification, Software model checking [BM Ch 5, 6], [R8]
Week 6: Oct 21
Midterm Exam: Oct 23		 Software model checking, Midterm review Project Outline due on Oct 25
Fall Break
Week 7: Nov 4, 6 Automatic invariant generation, CHC solvers [BM Ch 12] HW4 posted
Week 8: Nov 11, 13 Program synthesis [R9] HW5 posted
Week 9: Nov 18, 20 Network verification [R10], [R11]
Week 10: Nov 25
Nov 27: Thanksgiving break		 Applications: test generation, security
Week 11: Dec 2, 4 Student Project Presentations Project Interim Report due on Dec 6
Week 12: Dec 9, 11 Student Project Presentations
NO Final Exam Project Report due on Dean's Date: January 14, 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] Shuyuan Zhang, Sharad Malik. SAT Based Verification of Network Data Planes. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA) 2013: 496-505.
[R11] Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker. A General Approach to Network Configuration Verification. In Proceedings of SIGCOMM 2017: 155-168.