Deductive Program Verification

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

Course Materials

  • Predicate transformers (supplementary): slides


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.


verification.txt · Last modified: 2007/07/19 12:24 by tsay
Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki