Princeton University
Computer Science Department

Computer Science 597B: Advanced Topics in Computer Science
Automated Reasoning about Software

Aarti Gupta

Fall 2015
General Information | Schedule | Policies

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

Week/Dates Lectures Readings Homework
Week 0: Sept 17 Introduction, Course overview
Week 1: Sept 22, 24 Review of logic, Proofs using Hoare logic [BM Ch 1, 2], [R1], [BM Ch 4-6] HW1
Week 2: Sept 29, Oct 1 SAT Solvers, SMT solvers [R2], [BM Ch 3], [R3], [R4] HW2
Week 3: Oct 6, 8 SMT (continued), Model checking, Temporal logic [R5]
Week 4: Oct 13, 15 Symbolic model checking: BDD-based, SAT-based [R6], [R7] HW3
Week 5: Oct 20, 22 Software model checking: CEGAR, Interpolant-based [R8] HW4
Week 6: Oct 27
Midterm Exam: Oct 29		 Software model checking, Review for Midterm
Fall Break
Week 7: Nov 10, 12 Automatic invariant generation [BM Ch 12]
Week 8: Nov 17, 19 Guest lectures: Incremental inductive verification (IC3) [R9]
Week 9: Nov 24
Nov 26: Thanksgiving		 Symbolic execution and test generation [R10]
Week 10: Dec 1, 3 Program synthesis [R11]
Week 11: Dec 8, 10 Concurrent program verification, Network verification HW5
Week 12: Dec 15, 17 (last class) Student Presentations
NO Final Exam Project report due on Dean's Date: January 12, 2016.

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)