Logical foundations of formal verification (Hoare logic); development of correct programs using assertions, pre/post-conditions and invariants; verification of sequential, parallel and distributed programs. Exercises with selected verification systems.
First course: Mon, 3 March 2014. Please register for the course via TISS, or if this fails, via email to gernot.salzer@tuwien.ac.at.
Expected time effort per student:
26 h Lectures and examination
24 h Learning for examination
100 h Practice work
in total 150 h
David Gries: The Science of Programming, Springer 1981.
R.C. Backhouse: Program Construction and Verification, Prentice-Hall 1986.
Gerald Futschek: Programmentwicklung und Verifikation, Springer SAI 1989 (in German).
Edsger W. Dijkstra and Carel S. Scholten. Predicate Calculus and Program Semantics. Springer-Verlag 1990.
