Princeton University
Computer Science Department

COS 516 / ELE 516
Automated Reasoning about Software

Aarti Gupta

Fall 2016
General Information | Schedule | Policies

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

Week/Dates Lectures Readings Homework
Week 0: Sept 14 Introduction, Course overview
Week 1: Sept 19, 21 Review of logic, Program verification [BM Ch 1, 2], [R1], [BM Ch 4-6] HW1 posted
Week 2: Sept 26, 28 SAT solvers, SMT solvers [R2], [BM Ch 3], [R3], [R4] HW2 posted
Week 3: Oct 3, 5 SMT solvers, Temporal logic, Model checking [R5]
Week 4: Oct 10, 12 Model checking: BDD-based, SAT-based [R6], [R7] HW3 posted
Week 5: Oct 17, 19 Software model checking: CEGAR, Interpolant-based [R8]
Week 6: Oct 24
Midterm Exam: Oct 26		 Software model checking, Review for Midterm HW4 posted, Project Outline due
Fall Break
Week 7: Nov 7, 9 Incremental inductive verification (IC3) [R9]
Week 8: Nov 14, 16 Automatic invariant generation [BM Ch 12]
Week 9: Nov 21
Nov 24: Thanksgiving		 Symbolic execution and test generation [R10] Project Interim Report due
Week 10: Nov 28, 30 Program synthesis [R11] HW5 posted
Week 11: Dec 5, 7 Concurrent program verification, Network verification
Week 12: Dec 12, 14 Student Project Presentations
NO Final Exam Project Report due on Dean's Date: January 17, 2017.

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] Aaron R. Bradley, SAT-Based Model Checking without Unrolling, In Proceedings of VMCAI 2011.
[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] Rajeev Alur, Rastislav Bodík, and others. Syntax-guided synthesis. In Proceedings of FMCAD 2013: 1-8.

Other Papers

Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, Michael Deardeuff: How Amazon web services uses formal methods. Communications of the ACM 58(4): 66-73 (2015)