Computer systems play a very important role in modern society. Ensuring the reliability and dependability of such systems is economically important and intellectually challenging. This course will introduce students to fundamental techniques that have made significant contributions towards meeting this challenge. The material covered in the course is divided into three parts. The first part will cover model checking, with topics such as reachability analysis of finite-state and pushdown systems, symbolic representation with binary decision diagrams, and verification of temporal logic specifications. The second part of the course will dwell on classic program verification techniques developed by the early work of Floyd, Hoare, and Dijkstra. We will cover topics such as derivation of verification conditions and decision procedures for checking the validity of these verification conditions. We will cover satisfiability procedures for propositional logic, arithmetic, uninterpreted functions, and the Nelson-Oppen method for combining decision procedures. The last part of the course will bring together the material covered in the first two parts and focus on abstraction, perhaps the most important weapon for creating scalable verification tools. In this part, we will cover techniques such as abstract interpretation, predicate abstraction, and automated refinement of abstractions.

The course should be accessible to graduate students as well as senior undergraduate students. Exposure to formal language theory, algorithms, and elementary mathematical logic would be useful.

Office hours: by appointment

Mailing list: cse599f at cs dot washington dot edu

**Assignment 1**. Program verification: Attack and defense (Review due April 7)

**Assignment 2**. Explicit-state model checking of concurrent software

**Assignment 3**. Compositional verification

1. March 29. Introduction.

2. March 31. State transition graph, safety vs. liveness, CTL Slides.

3. April 5. LTL, specification via automata Slides

4. April 7. Continutation of last lecture

5. April 12. Algorithms for model checking Slides

6. April 14. Continutation of last lecture

7. April 19. Symbolic model checking Slides

8. April 21. Continutation of last lecture

9. April 26. Pushdown model checking Slides

10. April 28. Continuation of last lecture

11. May 3. Verification conditions Slides

12. May 5. Continuation of last lecture

13. May 10. Guest lecture: Building a program verifier by Rustan Leino

14. May 12. Guest lecture: Applying model checking to large programs by Madan Musuvathi

15. May 17. Propositional satisfiability Slides

16. May 19. Arithmetic Slides

17. May 24. Combining theories using the Nelson-Oppen procedure Slides

18. May 26. Abstract interpretation and predicate abstraction Slides

19. May 31. Continuation of last lecture

20. June 2. Wrapping up; Student presentations