Stud.IP Uni Oldenburg
University of Oldenburg
01.10.2020 15:29:16
inf450 - Correctness of Graph Programs (Complete module description)
Original version English Download as PDF
Module label Correctness of Graph Programs
Module code inf450
Credit points 6.0 KP
Workload 180 h
Faculty/Institute Department of Computing Science
Used in course of study
  • Master's Programme Computing Science (Master) > Theoretische Informatik
  • Master's Programme Embedded Systems and Microrobotics (Master) > Akzentsetzungsmodule
Contact person
Module responsibility
Authorized examiners
Entry requirements
Skills to be acquired in this module
The objectives of this module are modelling of systems, system changes and system properties. Introduction to graph programs. Introduction into system correctness. Methods for proving system correctness.

Professional competence
The students:
  • Describe the basics of graph programs and graph properties
  • Describe verification procedures of system correctness

Methodological competence
The students:
  • Model systems, system changes and system properties
  • Apply the formalism of graph programs

Social competence
The students:
  • Solve problems in a team
  • Present and discuss their proposed solutions

The students:
  • Reflect upon their actions with regard to term rewriting systems and the methods of those
Module contents
The module is an introduction to the modelling of systems, system changes and system properties by means of graphs, graph programs and graph conditions and presents a method for proving correctness of systems with respect to a pre- and a postcondition.

The basic structures used in this lecture are graphs; they are used in practically all domains of computing science for the representation of complex structures. Graph programs are constructed from the core constructs of nondeterministic rule application, sequential composition and iteration and they can effect programmatic changes of a graph structure. One well-known method for determining the correctness of programs with respect to a pre- and a postcondition is based on the construction of a weakest precondition of the postcondition with respect to the program and the attempt to decide whether the given precondition implies the computed weakest precondition.
Reader's advisory
  • A. Habel, K.-H. Pennemann. Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science, 19:245-296, 2009.
  • A. Habel, K.-H. Pennemann, A. Rensink. Weakest preconditions for high-level programs. In Graph Transformations (ICGT 2006), LNCS 4178, 445-460, 2006.
  • K. Azab, A. Habel, K.-H. Pennemann, C. Zuckschwerdt. ENFORCe: A system for ensuring formal correctness of high-level programs. In Electronic Communications of the EASST, Vol. 1. 82-93, 2007.
Language of instruction German
Duration (semesters) 1 Semester
Module frequency im 2-Jahres-Zyklus
Module capacity unlimited
Reference text
Wird oft als Blockveranstaltung angeboten
Modullevel AC (Aufbaucurriculum / Composition)
Modulart je nach Studiengang Pflicht oder Wahlpflicht
Lern-/Lehrform / Type of program
Vorkenntnisse / Previous knowledge - inf400 Theoretische Informatik I
- inf401 Theoretische Informatik II
Course type Comment SWS Frequency Workload attendance
Lecture 3.00 WiSe 42 h
Exercises 1.00 WiSe 14 h
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
Will be announced during the course
presentation or oral exam