Table of Contents

Lecturer: Yih-Kuen Tsay 蔡益坤

This module introduces the students to the basics of how correctness of a program can be expressed and how it can be proven with a logic system.

The student must have taken a Computer Programming course and a Discrete Mathematics course, or their equivalences.

- Hoare logic (I): axiomatic semantics and program correctness — assertions, pre and post-conditions, proof rules, invariants, program annotation, rank functions, termination, nondeterminism
- Hoare logic (II): procedures and concurrency — non-recursive procedures, recursive procedures, concurrent programs, Owicki-Gries method, proof outlines, intereference freedom, auxiliary variables
- Temporal verification of reactive systems — fair transition systems, linear temporal logic, safety, liveness
- Program verification with the Spec# tool

Hoare Logic

- K.R. Apt and E.-R. Olderog. Verification of Sequential and Concurrent Programs (2nd Edition), Springer, 2006.
- D. Gries. The Science of Programming, Springer-Verlag, 1981.
- C.A.R. Hoare. An axiomatic basis for computer program. CACM, 12(10):576–583, 1969.
- T. Kleymann. Hoare logic and auxiliary variables. Formal Aspects of Computing, 11:541–566, 1999.
- S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319–340, 1976.
- R. Sethi. Programming Languages: Concepts and Constructs, 2nd Ed., Addison-Wesley, 1996.
- K. Slonneger and B.L. Kurtz. Formal Syntax and Semantics of Programming Languages, Addison-Wesley, 1995.

Temporal Verification

- Z. Manna and A. Pnueli. Completing the temporal picture. Theoretical Computer Science, 83(1):97–130, 1991.
- Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, 1995.
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: Progress. Unpublished manuscript, available at this site, 1996.

Spec#