CSE599f, Spring 2006 (original) (raw)

CSE 599F: Formal Verification of Computer Systems

Course Description

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.

Staff

Instructor: Shaz Qadeer, qadeer at cs dot washington dot edu, Allen Center 454
Office hours: by appointment
Mailing list: cse599f at cs dot washington dot edu

Reading Assignments

During the course, I will give out several reading assignments comprising research papers that have either influenced the fundamental ideas presented in the lectures or attempted to apply them in practice. We will discuss the papers in each reading assignment in the class a week after it is given out. In addition to participating in the classroom discussion, each student is expected to write a review of the papers. Please use the web-based toolfor entering your reviews.

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

• A mechanized program verifier. J.S. Moore. Verification Grand Challenge Workshop, October, 2005.
• Social processes and proofs of theorems and programs. R.A. de Millo, R.J. Lipton, and A.J. Perlis. Communications of the ACM, Vol. 22, Number 5, pages 271-280, 1979.
• Section 2 ("Defense of Program Verification") of Techniques for Program Verification. G. Nelson. Ph.D. thesis. Stanford University, 1981.

Assignment 2. Explicit-state model checking of concurrent software

• The Model Checker Spin. G. Holzmann. IEEE Transactions on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295.
• Software model checking: the VeriSoft approach. P. Godefroid. Formal Methods in System Design, Kluwer Academic Publishers, volume 26, number 2, pages 77-101, March 2005.
• CMC: A pragmatic approach to model checking real code. M. Musuvathi, D.Y.W. Park, A. Chou, D.R. Engler, D.L. Dill. ACM Symposium on Operating Systems Design and Implementation (OSDI), December 2002.

Assignment 3. Compositional verification

• Proofs of networks of processes . J. Misra and K.M. Chandy. IEEE Transactions on Software Engineering, Vol. SE-7, No. 4, pages 417-426, July 1981.
• Reactive modules. R. Alur and T.A. Henzinger. Formal Methods in System Design 15:7-48, 1999.
• A compositional rule for hardware design refinement. K.L. McMillan. Conference on Computer Aided Verification, pages 24-35, 1997.

Homeworks

There will be two kinds of homeworks. The first kind will require you to work out examples or theoretical problems related to the material taught in class. The second kind will be case studies involving modeling and verification with tools such as SMV, Alloy, and ESC/Java2.

• Homework 1 (Due April 14)
• Homework 2. Using a model checker (Due May 12)
• Homework 3 (Due May 19)

Project

Each student is expected, either individually or with a partner, to do a project. Several kinds of projects are possible:

• Independent research
• Survey of a research area
• Case-study using a verification tool

Lectures

Thanks to Tom Ball, Randy Bryant, Tom Henzinger, and George Necula for providing many slides in the following lectures.

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

References

• A mechanized program verifier. J.S. Moore. Verification Grand Challenge Workshop, October, 2005.
• Social processes and proofs of theorems and programs. R.A. de Millo, R.J. Lipton, and A.J. Perlis. Communications of the ACM, Vol. 22, Number 5, pages 271-280, 1979.
• Model Checking. E.M. Clarke, O. Grumberg, and D.A. Peled. MIT Press, 1999.
• Automatic verification of finite-state concurrent systems using temporal logic specifications. E.M. Clarke, E.A. Emerson, and A.P. Sistla. ACM Transactions On Programming Languages and Systems, Vol. 8, No. 2, pages 244-263, 1986.
• Graph-based algorithms for Boolean function manipulation. R. Bryant. IEEE Transactions on Computers, Vol. C-35, No. 8, pages 677-691, August 1986.
• Symbolic model checking: 10^20 states and beyond. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pages 1-33, 1990.
• An automata-theoretic approach to linear temporal logic. M.Y. Vardi. Banff Higher Order Workshop, 1996.
• Model Checking Pushdown Systems. S. Schwoon. Ph.D. thesis, Technische Universitat, Munchen, 2002.
• Guarded commands, nondeterminacy and formal derivation of programs. E.W. Dijkstra. Communications of the ACM, Vol. 18, No. 8, August 1975.
• Techniques for Program Verification. G. Nelson. Ph.D. thesis. Stanford University, 1981.
• Simplify: a theorem prover for program checking. D. Detlefs, G. Nelson, and J.B. Saxe. Technical Report HPL-2003-148, HP Labs, 2003.
• Assertions: a personal perspective. C.A.R. Hoare. June 2001.
• Weakest-precondition of unstructured programs. M. Barnett and K.R.M. Leino. ACM Workshop on Program Analysis for Software Tools and Engineering, pages 82-87, 2005.
• Abstract interpretation: a unified lattice model for static analysis by construction or approximation of fixpoints. P. Cousot and R. Cousot. ACM Symposium on Principles of Programming Languages, ACM Press, pages 238-252, 1977.
• Automatic discovery of linear restraints among variables of a program. P. Cousot and N. Halbwachs. ACM Symposium on Principles of Programming Languages, ACM Press, pages 84-97, 1978.
• Construction of abstract state graphs with PVS. S. Graf and H. Saidi. Conference on Computer-Aided Verification, LNCS 1254, Springer-Verlag, pages 72--83, 1997.
• Proofs of networks of processes . J. Misra and K.M. Chandy. IEEE Transactions on Software Engineering, Vol. SE-7, No. 4, pages 417-426, July 1981.
• Reactive modules. R. Alur and T.A. Henzinger. Formal Methods in System Design 15:7-48, 1999.
• A compositional rule for hardware design refinement. K.L. McMillan. Conference on Computer Aided Verification, pages 24-35, 1997.
• Verification of an implementation of Tomasulo's algorithm by compositional model checking. K.L. McMillan. Conference on Computer Aided Verification, 1998.
• GRASP: A search algorithm for propositional satisfiability. J.P. Marques-Silva and K.A. Sakallah. IEEE Transactions on Computers, vol. 48, no. 5, pages 506-521, 1999.