inf407 - Program Verification (Complete module description)

inf407 - Program Verification (Complete module description)

Original version English PDF download
Module label Program Verification
Module code inf407
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Applicability of the module
  • Bachelor's Programme Computing Science (Bachelor) > Akzentsetzungsbereich - Wahlbereich Informatik
  • Dual-Subject Bachelor's Programme Computing Science (Bachelor) > Wahlpflicht Theoretische Informatik (30 KP)
  • Master of Education Programme (Gymnasium) Computing Science (Master of Education) > Wahlpflichtmodule (Theoretische Informatik)
Responsible persons
  • Wehrheim, Heike (module responsibility)
  • Olderog, Ernst-Rüdiger (module responsibility)
  • Lehrenden, Die im Modul (authorised to take exams)
Prerequisites
Skills to be acquired in this module

Introduction to methods for proving the correctness of sequential and parallel programs. 

Professional competence
The students:

  • describe operational semantics of sequential and parallel  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
  •  construct correctness proof for weak memory models

Methodological competence
The students:

  • recognize correctness as an important aspect of programs and informatics systems
  • recognize formal calculi as means of specification and verification

Social competence
The students:

  • work together in small groups to solve problems
  • present their solutions to groups of other students

Self-competence
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  and their extension to parallel programs, in particular also weak memory models, are studied. Sequential programs are covered in preparation for this.
Recommended reading

essential:

  • "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''
Links
Language of instruction English
Duration (semesters) 1 Semester
Module frequency every second winter term
Module capacity unlimited
Teaching/Learning method V+Ü
Previous knowledge Helpful prerequisites:

set theory, relations, functions, propositional logic, predicate logic, programming in an imperative language
Type of course Comment SWS Frequency Workload of compulsory attendance
Lecture 3 see frequency of module offering 42
Exercises 1 see frequency of module offering 14
Total module attendance time 56 h
Examination Prüfungszeiten Type of examination
Final exam of module

At the end of the lecture period

Written exam or oral exam