Stud.IP Uni Oldenburg
University of Oldenburg
18.10.2021 19:07:33
inf408 - Algorithms for Software Verification (Complete module description)
Original version English Download as PDF
Module label Algorithms for Software Verification
Module code inf408
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) > Mastermodule
Responsible persons
Olderog, Ernst-Rüdiger (Authorized examiners)
Lehrenden, Die im Modul (Authorized examiners)
Prerequisites
Skills to be acquired in this module
Algorithms are presented that enables an automatic analysis and verification of complex structures as used in software systems. In the exercises these algorithms will be implemented and applied to case studies.

Professional competence
The students:
  • conduct CTL model checking using examples
  • construct abstract Kripke structures on the basis of given data abstractions and apply abstraction refinement
to examples
  • characterise the concepts of simulation and bisimulation
  • understand the concept of data and transition abstraction
  • describe model checking methods as instances of fixed-point algorithms

Methodological competence
The students:
  • specify reactive systems by means of Kripke structures and CTL formulas
  • implement model checking methods using Java

Social competence
The students:
  • work in small groups

Self-competence
The students:
  • reflect their actions and use newly learned methods
Module contents
Software systems consist of complex data and control structures and growing state spaces, which makes testing their correctness difficult. The big challenge for computer science is the development of automatic methods to analyse and to verify software systems’ properties. In this course, algorithms for program analysis and model checking are presented and applied. The algorithms process transition systems generated from software and use abstraction techniques for data and transitions to make the state spaces analysable.

Topics:
Kripke structures, transition systems, temporal logic CTL and CTL*, fixed-point algorithms for recursive CTL-operators, model checking algorithms for CTL, simulation and bisimulation of Kripke structures, theorems on
the preservation of properties under (bi-) simulations, existential und universal abstraction of Kripke structures, counterexample-guided abstraction refinement (CEGAR method)
Reader's advisory
  • E.M. Clarke, O. Grumberg, and D. Peled: Model Checking. MIT Press, 2000.
  • F. Nielson, H.R. Nielson, and C. Hankin: Principles of Program Analysis, Springer, 2005
  • E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM 50(5) 752-794 (2003)
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 Grundveranstaltungen in Informatik und Mathematik
Course type Comment SWS Frequency Workload of compulsory attendance
Lecture
2 SoSe oder WiSe 28
Exercises
2 SoSe oder WiSe 28
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
First week of lecture-free period
Written exam or oral exam