Stud.IP Uni Oldenburg
University of Oldenburg
06.07.2020 01:38:41
inf407 - Program Verification (Complete module description)
Original version English Download as PDF
Module label Program Verification
Module code inf407
Credit points 6.0 KP
Workload 180 h
Faculty/Institute Department of Computing Science
Used in course of study
  • Bachelor's Programme Computing Science (Bachelor) >
  • Dual-Subject Bachelor's Programme Computing Science (Bachelor) >
  • Master of Education Programme (Gymnasium) Computing Science (Master of Education) >
Contact person
Module responsibility
Authorized examiners
Entry requirements
Skills to be acquired in this module
Introduction to methods for proving the correctness of sequential, parallel, and distributed programs.

Professional competence
The students:
  • Describe operational semantics of sequential, parallel, and distributed programs
  • Know the concepts of partial and total correctness of programs
  • Establish soundness and completeness of proof systems
  • Construct input-output specifications of programs
  • Conduct correctness proofs for programs of different classes with the help of proof rules
  • Check interference and deadlock freedom of parallel programs
  • Transform parallel and distributed programs into nondeterministic programs

Methodological competence
The students:
  • Recognize correctness as an important aspect of programs and informatics systems

Social competence
The students:
  • Work together in small groups to solve problems
  • Present their solutions to groups of other students

The students:
  • Learn persistence in pursuing difficult tasks
  • Learn precision in specifying problems         
Module contents
Program verification is a systematic approach to show the absence of errors in programs. For this purpose desirable behavioural properties of a given program are proven. For instance, a sorting program should only deliver sorted arrays.

Partial correctness, termination, and the absence of runtime errors are essential for sequential programs. Additional behavioural properties are of interest for parallel programs: absence of interference, absence of deadlocks, and fair behaviour.

The module focuses on the verification of parallel programs. For this purpose classic methods of Hoare's logic are combined with more recent techniques of program transformation. Sequential programs are covered in preparation for this.
Reader's advisory
"K.R. Apt, E.-R. Olderog, Programmverifikation, Springer-Verlag, 1994''

Or the extended English version:
"K.R. Apt, F.S. de Boer, E.-R. Olderog, Verfication of Sequential and Concurrent
Programs, Third Edition, Springer-Verlag, 2008''
Language of instruction German
Duration (semesters) 1 Semester
Module frequency unregelmäßig
Module capacity unlimited
Modullevel AS (Akzentsetzung / Accentuation)
Modulart je nach Studiengang Pflicht oder Wahlpflicht
Lern-/Lehrform / Type of program V+Ü
Vorkenntnisse / Previous knowledge Theoretische Informatik I und II
Course type Comment SWS Frequency Workload attendance
Lecture 3.00 42 h
Exercises 1.00 14 h
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
At the end of the lecture period
Written exam or oral exam