Princeton University
Computer Science Department

COS 516 / ELE 516
Automated Reasoning about Software

Aarti Gupta

Fall 2017
General Information | Schedule | Policies

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

Week/Dates Lectures Readings Homework (posted)
Week 0: Sept 13 Introduction, Course overview
Week 1: Sept 18, 20 Review of logic, Program verification intro [BM Ch 1, 2], [R1], [BM Ch 4-6] HW1
Week 2: Sept 25, 27 SAT solvers, SMT solvers [R2], [BM Ch 3], [R3], [R4] HW2
Week 3: Oct 2, 4 Temporal logic, Model checking [R5]
Week 4: Oct 9, 11 Symbolic model checking: BDD-based, SAT-based [R6], [R7] HW3
Week 5: Oct 16, 18 Software model checking: CEGAR, Interpolant-based [R8] HW4
Week 6: Oct 23
Midterm Exam: Oct 25		 Software model checking, Review for Midterm Project Outline due
Fall Break
Week 7: Nov 6, 8 Automatic invariant generation [BM Ch 12]
Week 8: Nov 13, 15 Program synthesis [R9]
Week 9: Nov 20
Nov 22: Thanksgiving break		 Symbolic execution and test generation [R10] HW5
Week 10: Nov 27, 29 Network verification [R11], [R12] Project Interim Report due
Week 11: Dec 4, 6 Concurrent program verification, Security verification
Week 12: Dec 11, 13 Student Project Presentations
NO Final Exam Project Report due on Dean's Date: January 16, 2018.

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] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12, 10, 576-580, 1969.
[R2] Joao Marques-Silva, Ines Lynce, and Sharad Malik. Conflict-Driven Clause Learning SAT Solvers. Handbook of Satisfiability, Chapter 4, 2008.
[R3] Leonardo de Moura and Nikolaj Bjorner. Satisfiability Modulo Theories: Introduction and Applications. Communications of the ACM, vol. 54, no. 9, 2011.
[R4] Clark Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability Modulo Theories. Handbook of Satisfiability, Chapter 12, 2008.
[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] Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 100 (8), 677-691, 1986.
[R7] 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.
[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] Patrice Godefroid, Michael Y. Levin, David A. Molnar. Automated Whitebox Fuzz Testing. In Proceedings of Network and Distributed System Security Symposium (NDSS) 2008.
[R11] 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.
[R12] Ryan Beckett, Aarti Gupta, Ratul Mahajan, David Walker. A General Approach to Network Configuration Verification. In Proceedings of SIGCOMM 2017: 155-168.