CIS 673: Computer-Aided Verification, Fall 2016
Class: Mon Wed 10.30-Noon, Towne 305
How can a programmer verify that the software (s)he has designed works correctly as intended?
Computer-aided verification is a sub-discipline of computer science aimed at developing
tools and techniques to assist programmers meet this goal.
This course focuses on logical foundations necessary to formalize the question of software verification
and algorithmic tools necessary to automate the challenging task of software verification to the extent possible.
The list of topics includes verification conditions, program termination, propositional and first-order logic, SAT and SMT solvers,
abstract interpretation and static analysis, software model checking, refinement proofs, modular reasoning, verification of concurrent programs,
and program synthesis.
Note: the previous offering of this course, in Fall 2014, focused on model checking and had a significantly different set of topics
(link to 2014 webpage).
The course assumes basic knowledge of algorithms, data structures,
programming languages, computational complexity, and
The course requires mathematical maturity, and is appropriate
for students who wish to pursue research in
formal methods or programming languages.
If you need more information to decide, contact the instructor.
Every week, students are expected to read course handouts and participate actively during class.
Each student is also expected to do a class project and give a presentation at the end of the semester.
There will be no homeworks or exams.
- Aug 31: Introduction to Computer-Aided Verification
- Sept 7, 12, 14: Foundations of program verification: pre/post-conditions, loop invariants, ranking functions, and
generation of verification conditions
Reading: Chapter 5 of Bradley/Manna
- Sept 19, 21: Propositional logic and modern SAT solvers (Slides by Sharad Malik)
Reading: Conflict-driven clause learning SAT solvers
- Sept 26, 28, Oct 3: Decision procedures and SMT solvers: Lecture slides by Leonardo de Moura
(leo1, leo2, leo3)
Reading:Satisfiability Modulo Theories by Barrett, Sebastiani, Seshia, and Tinelli
- Course project
- Oct 5: No Class
- Oct 10, 12, 17, 19: Static analysis: dataflow analysis (slides by Mayur Naik), abstract interpretation (slides by Isil Dillig), interprocedural analysis (slides by Tom Reps)
Reading: Program analysis by graph reachability, Tom Reps
- Oct 24, 26, 31, Nov 2: Model checking (slides)
Reading: Temporal Logic, by N. Piterman;
Automata theory and model checking, by O. Kupferman
- Nov 7, 9, 14: Concurrency. Lectures by Arjun Radhakrishna: Lecture 1, Lecture 2, Lecture 3
- Nov 16, 21: Software model checking (slides)
Reading: Software model checking, Jhala and Majumdar, ACM Computing Surveys, 2009
A decade of software model checking in SLAM, Ball et al, CACM 2011
- Nov 28: Concolic testing (Slides by Koushik Sen)
Reading: Combining model checking and testing by Godefroid and Sen
Project Springfield at Microsoft
- Nov 30, Dec 5: Analysis of probabilistic systems
See PRISM website for papers and tutorials
- Dec 7: Syntax-guided program synthesis: paper; slides; SyGuS website
- Dec 12: Project presentations by students
We will use a collection of survey articles, research papers, and tutorial slides to cover different topics.
For a coherent and in-depth introduction to a subset of topics, the following textbook is recommended:
For hands-on experience with automated program verification, play with:
Maintained by Rajeev Alur