Proving correctness of graph programs relative to recursively nested conditions

21. Oktober 2016, 14:15

Organisator:  Herr Dipl.-Inform. Nils Erik Flick

Ort:  Gebäude A14, Raum 0-031

M i t t e i l u n g 

Im Rahmen der Disputation seines Promotionsverfahrens hält Herr Dipl.-Inform. Nils Erik Flick, seinen öffentlichen Vortrag zum Thema

„Proving correctness of graph programs relative to recursively nested conditions“

am Freitag, den 21. Oktober 2016, um 14.15 Uhr im Gebäude A14, Raum 0-031.

Abstract: 

This thesis deals with formally proving the correctness of graph programs. A wide variety of discrete systems can be modelled with Petri nets. Graph transformation systems are a suitable extension of Petri nets when the system structure is not fixed. They allow the explicit representation of structured states with dynamic connectivity. Graph programs are an extension of graph transformation systems by control constructs (sequence, nondeterministic choice and iteration). Graph transformation systems are already Turing-complete and results on automatic checking of correctness of graph programs with respect to a specification must accept incompleteness. We start by investigating language-theoretic notions of correctness for restricted classes of structure-changing Petri nets, where we establish some decidability results. Acknowledging the limitations of this approach, we then transcend it by striving for methods based on theorem proving. The main part, accordingly, is about developing methods for reasoning about graph conditions and graph programs, especially under the assumption of adverse conditions manifested as intermittent faults. We provide examples and case studies to demonstrate how our methods can be applied.

Mit der Teilnahme von Zuhörerinnen und Zuhörern an der anschließenden Prüfung bis 15.45 Uhr ist Herr Flick einverstanden.

gez. Prof. Dr.-Ing. A. Hahn