Stud.IP Uni Oldenburg
University of Oldenburg
06.12.2021 18:31:26
inf450 - Correctness of Graph Programs (Complete module description)
 Module label Correctness of Graph Programs Module code inf450 Credit points 6.0 KP Workload 180 h Institute directory Department of Computing Science Applicability of the module Master's Programme Computing Science (Master) > Theoretische Informatik Master's Programme Embedded Systems and Microrobotics (Master) > Akzentsetzungsmodule Responsible persons Habel, Annegret (Module responsibility) Hein, Andreas (Authorized examiners) Lehrenden, Die im Modul (Authorized examiners) Prerequisites 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 competenceThe students:Describe the basics of graph programs and graph properties Describe verification procedures of system correctnessMethodological competenceThe students:Model systems, system changes and system properties Apply the formalism of graph programsSocial competence The students:Solve problems in a teamPresent and discuss their proposed solutionsSelf-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. 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. Links 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 / module level AC (Aufbaucurriculum / Composition) Modulart / typ of module je nach Studiengang Pflicht oder Wahlpflicht Lehr-/Lernform / Teaching/Learning method Vorkenntnisse / Previous knowledge - inf400 Theoretische Informatik I - inf401 Theoretische Informatik II
Course type Comment SWS Frequency Workload of compulsory attendance
Lecture
3 WiSe 42
Exercises
1 WiSe 14
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