CIS 673: Computer-Aided Verification, Spring 2020
Class: Mon Wed 3--4.30 , Towne 315
How can a programmer verify that the software they have 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.
These tools have now reached a level of maturity where they are being integrated in system design
in companies such as Amazon, Facebook, Google, and Microsoft.
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 course assumes basic knowledge of algorithms, data structures,
programming languages, computational complexity, and
The course requires mathematical maturity, and is appropriate
for PhD students who wish to pursue research in
formal methods, programming languages, or cyber-physical systems, and
undergraduate/Masters students who want to understand the techqniues used in formal verification tools.
If you need more information to decide, contact the instructor.
Every week, students are expected to read course handouts and participate actively during class.
There will be no homeworks or exams, but each student is required to do a class project.
The project can be (1) a case study of applying formal verification to design/debug/understand a system component,
(2) an implementation, and its evalution, to enhance features/scalability of a verification tool, or
(3) a project of your choice relevant to the themes of the course.
At the end of the semester, you are required to submit a written report and give a presentation about the project.
The exact set of topics will be determined dynamically based on the students' interests. Below is
a tentative organization of the course:
- Constraint solving: Program verification as satisfiability checking of logical formulas,
Boolean satisfiability and efficient SAT solvers, decidable logical theories, combination of decision procedures,
- Software model checking: Predicate abstraction, temporal logic specifications, symbolic state-space exploration,
reasoning about procedures, counterexample-guided abstraction refinement
- Program synthesis: Syntax-guided synthesis, counterexample-guided inductive synthesis, machine learning and synthesis
- Analysis of hybrid systems: Basics of dynamical systems and control, symbolic reachability analysis, robustness,
- 1/15: Introduction
- 1/20: Assertion checking as constraint solving
- 1/27, 1/29: Tutorial on SAT solvers by Sharad Malik
- 2/3, 2/5: Symbolic reachability analysis
- SMT Tutorial by Leonardo de Moura: 2/10: Part 1, 2/12: Part 2
- 2/17: Verifying neural networks using ReluPlex by Guy Katz
- 2/19: Concolic testing by Koushik Sen
- Project instructions
- 2/24, 26: Temporal logic model checking
- 3/2, 4: Software model checking by Henzinger, Jhala, and Majumdar
- 3/ 23, 25, 30: Program synthesis: see Piazza site under Lecture Notes for lecture slides
- 4/ 1, 6, 8: Analysis of concurrent programs: see Piazza site under Lecture Notes for lecture slides
- 4/ 13, 15: Probabilistic model checking: see Piazza site under Lecture Notes for lecture slides
Maintained by Rajeev Alur