PROGRAM VERIFICATION



Instructor:
Nachum Dershowitz

Textbook:

Exam (Questions & Answers) Due (by email) 28 Feb 00:01h

Lecture Notes

Topics and Readings:

  1. Background
    1. Text, Chapter 1 and 2
  2. Invariants
    1. Chapter 3
  3. Nondeterminism and Concurrency
    1. Chapters 4, 5
  4. Termination
    1. Term Rewriting and All That, Chap. 5 (on reserve in library)
    2. Rewriting, Sect. 4
  5. Temporal Logic and Automata
    1. Automated Verification Notes, Vardi
    2. Automata and Temporal Logic, Vardi (PDF download)
    3. Temporal and Model Logic, Emerson (PDF download)
  6. Fairness, Chap. 9 [not covered]

Handouts:

    This page
  1. Binary Search Exercise
  2. Tree Program
  3. Termination Problem
  4. Concurrent Search Program
  5. Mystery Program
  6. Inference Rules
  7. "Column 4: Writing Correct Programs", J. Bentley, Programming Pearls, Addison-Wesley, 1986.
  8. "An Early Program Proof by Alan Turing", F. L. Morris and C. B. Jones, Annals of the History of Computing, vol. 6, no. 2 (Apr. 1984), pp. 139-143.
  9. Disjoint Find Program
  10. Proof of a program: FIND. C. A. R. Hoare
  11. On-the-fly garbage collection proof, D. Gries
  12. Ackermann's function
  13. Path Orderings
  14. ["The Schorr-Waite Graph Marking Algorithm", D. Gries, Acta Informatica, vol. 11, pp. 223-232 (1979).]

Homeworks:

  1. Find invariants for Find
  2. Concurrent Search
  3. Ackermann's function
  4. Prove protocol properties using STeP

Links: