Formale Semantik/Mehrfachvererbung
Ich habe eine formale Semantik einer C++-ähnlichen Sprache,
gennant CoreC++, entwickelt. Diese Sprache ist eine
Weiterentwicklung/Anpassung von Jinja, einer
Java-ähnlichen Sprache, die am
Lehrstuhl von Prof. Nipkow an der Technischen Universität
München entwickelt wurde. Die Formalisierung und der
Korrektheitsbeweis wurden im generischen Theorembeweiser
Isabelle durchgeführt.
Verifikation von Slicing
Slicing mithilfe von Kontrollfluß- und
Programmabhängigkeitsgraphen ist eine Standard-Programmanalyse.
Diese sprachunabhängigen Graphstrukturen enthalten in
Kombination mit gewissen Wohlgeformtheitsbedingungen genug
Information um Slicing durchzuführen und zu verifizieren.
Wir verifizieren, basierend auf diesen Strukturen, verschiedene
Arten des Slicings: dynamisch, statisch intra- und interprozedural.
Außerdem wollen wir zeigen wie verschiedene Semantiken
(z.B. Jinja and CoreC++) in diese Strukturen
eingebettet werden können, womit Slicing für die Kerne
bekannter OO-Sprachen verifiziert wäre.
Meine Erdős Nummer
ist maximal 4 (und ziemlich sicher auch nicht kleiner):
Daniel Wasserrab -> Tobias Nipkow -> Gerhard Weikum ->
Patrick Eugene O'Neil -> Paul Erdős
