Logics of Programs

OUTLINE

This course will survey logics for reasoning about imperative
programs.  Our discussion will be rooted in propositional dynamic
logic for transition systems, and will proceed to first order dynamic
logic, Hoare-style logics for partial and total correctness
assertions, and formally annotated program.

The course will balance theory and applications.
On the side of theory, we shall lay out major foundational results
in the field, including the semantic completeness of propositional dynamic
logic, relative completeness theorems, and the axiomatization
of major programming constructs (including recursive procedures and variable
mechanisms).  We shall also discuss limitations
on notions of completeness, and compare alternative notions.

On the applications side, we shall discuss Dijkstra's program
development methodology, with an emphasis on the interplay between
formal tools and mathematical insight.