Automatischer Korrektheitsnachweis von Programmtransformationen

• Applicant: Professor Dr. Manfred Schmidt-Schauß
• Subject Area: Theoretical Computer Science
• Term: from 2010 to 2014
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 164088002

Untersucht werden Semantiken verschiedener – insbesondere nebenläufiger und nichtdeterministischer – Programmiersprachen (repräsentiert durch Programmkalküle) auf der Basis der kontextuellen Gleichheit, die wiederum auf einer operationalen Semantik aufsetzt. Informell: zwei Programme sind gleich, wenn man keinen Unterschied bzgl. Terminierung / Nichtterminierung „beobachten“ kann, bei allen möglichen Verwendungen. Diese Gleichheitsdefinition ist von Interesse, da sie maximal ist und fast immer anwendbar ist, auch dann noch, wenn andere Semantik-Formalismen versagen oder zu restriktiv sind. Ziel ist die Automatisierung des Korrektheitsnachweises von Programmtransformationen. Der algorithmische Kern ist die Berechnung der Überlappungen von Auswertungsregeln und Transformationsregeln in Analogie zum Berechnen der kritischen Paare nach Knuth-Bendix. Diese Methode soll so allgemein umgesetzt werden, dass diese für viele Programmkalküle verwendbar ist, und somit auch für andere Forschergruppen von Interesse ist.

• DFG Programme: Research Grants