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.
This course has been renamed to "Deductive Verification of Software"; for more information see this course.
First lecture: 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.