Deductive Program Verification

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.

Prerequisites

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

Temporal verification of reactive systems: slides exercise #3 solutions to exercise #3

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#