Lecture Notes

Lecture notes will be made available here as the course progresses. 

1. Introduction. Historical Perspective. Overview. Operational Semantics. (PDF)
2. Axiomatic Semantics. Hoare Rules. (PDF)
3. Weakest preconditions. Verification Condition Generation. (PDF)
4. Extensions and Pitfalls of VC Generation. (PDF)
5. Forward VC Generation. VC as "semantic checksum" (PDF)
6. Logical theories. Definitions. (PDF)
7. Combining Satisfiability Procedures by Equality Sharing. (PDF)
8. Proof-Generating Extension of Nelson-Oppen prover. Proof Representation. (PDF courtesy of Wes Weimer)
9. Satisfiability Procedure for Equality using Congruence Closure (PDF)
10. A method for Finding satisfiability Procedures based on Congruence Closure. Lists. (PDF)
11. A method for Finding satisfiability Procedures based on Congruence Closure. Arrays. (PDF)
12. Satisfiability Procedures for Arithmetic. Pratt's difference constraints algorithm. (PDF)
13. Satisfiability Procedures for Arithmetic. Shostak's algorithm. Fourier-Motzkin. SUP-INF. (PDF)
14. Overview of the class project 
15. Satisfiability Procedures for Arithmetic. The Simplex algorithm. (PDF)
16. Overview and demo of the PVS theorem proving system. Lecture by Dawn Song. (.PS.GZ)
17. Detecting equalities of variables using simplex. Proof generation in Simplex. (PDF)
18. Tactic-Based Theorem Proving. (PDF). Isabelle demo.
19. Incorporating Tactics in the Nelson-Oppen Prover. (PDF)
20. Generalized tactics and matching. (PDF)
21. A theory of semantic type checking. (PDF)
22. Shostak's Method for Combining Theories (used in PVS). "On Shostak's Decision Procedure for Combination of Theories", David Cyrluk, Patrick Lincoln, Natarajan Shankar, CADE'96.
23. Synthesizing loop invariants (PDF)

Last modified: 04/28/00 09:38 PM by necula@cs