Stud.IP Uni Oldenburg
University of Oldenburg
06.07.2022 07:07:07
inf407 - Program Verification (Complete module description)
 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 Olderog, Ernst-Rüdiger (Module responsibility) Lehrenden, Die im Modul (Authorized examiners) Prerequisites Skills to be acquired in this module Introduction to methods for proving the correctness of sequential, parallel, and distributed programs.Professional competenceThe students:Describe operational semantics of sequential, parallel, and distributed programsKnow the concepts of partial and total correctness of programsEstablish soundness and completeness of proof systemsConstruct input-output specifications of programsConduct correctness proofs for programs of different classes with the help of proof rulesCheck interference and deadlock freedom of parallel programsTransform parallel and distributed programs into nondeterministic programsMethodological competenceThe students:Recognize correctness as an important aspect of programs and informatics systemsSocial competenceThe students:Work together in small groups to solve problemsPresent their solutions to groups of other studentsSelf-competenceThe students:Learn persistence in pursuing difficult tasksLearn 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 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 ConcurrentPrograms, Third Edition, Springer-Verlag, 2008'' Links Language of instruction German Duration (semesters) 1 Semester Module frequency unregelmäßig Module capacity unlimited Modullevel / module level AS (Akzentsetzung / Accentuation) Modulart / typ of module je nach Studiengang Pflicht oder Wahlpflicht Lehr-/Lernform / Teaching/Learning method V+Ü Vorkenntnisse / Previous knowledge Theoretische Informatik I und II
Course type Comment SWS Frequency Workload of compulsory attendance
Lecture
3 42
Exercises
1 14
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