inf450 - Correctness of Graph Programs (Complete module description)

Module label	Correctness of Graph Programs
Modulkürzel	inf450
Credit points	6.0 KP
Workload	180 h
Institute directory	Department of Computing Science
Verwendbarkeit des Moduls	Master's Programme Computing Science (Master) > Theoretische Informatik
Zuständige Personen	Lehrenden, Die im Modul (module responsibility) Lehrenden, Die im Modul (Prüfungsberechtigt)
Prerequisites	- inf400 Theoretical Computer Science I - inf401 Theoretical Computer Science II
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 Self-competence 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.
Literaturempfehlungen	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.
Links
Language of instruction	German
Duration (semesters)	1 Semester
Module frequency	in 2-year cycle
Module capacity	unlimited
Reference text	Often offered as a block course
Teaching/Learning method	1VL + 1Ü
Previous knowledge	- inf400 Theoretical Computer Science I - inf401 Theoretical Computer Science II

Lehrveranstaltungsform	SWS	Frequency	Workload of compulsory attendance
Lecture	3	WiSe	42
Exercises	1	WiSe	14
Präsenzzeit Modul insgesamt			56 h

Examination	Prüfungszeiten	Type of examination
Final exam of module	Will be announced during the course	presentation or oral exam