Verifikation imperativer Programme

• Antragsteller: Professor Dr. Jürgen Giesl
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 1999 bis 2001
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 5197474

Um die Korrektheit von Programmen zu garantieren, wird eine formale Verifikation benötigt. Die Durchführung eines mathematischen Korrektheitsbeweises ist jedoch im allgemeinen sehr aufwendig. Deshalb muß die Programmverifikation weitgehend automatisiert werden. Hierfür wurden sogenannte Induktionsbeweissysteme entwickelt, die eine automatische Programmverifikation unterstützen. Diese Systeme werden sehr erfolgreich für funktionale Programmiersprachen verwendet. Eines der Hauptprobleme für ihren praktischen Einsatz ist jedoch, daß sie sich kaum für die in der Praxis benutzten imperativen Programmiersprachen eignen. Der Ansatz des Forschungsvorhabens ist daher die Entwicklung eines automatischen Transformationsverfahrens. Hierbei sollen imperative Programme, die für die Verifikation ungeeignet sind, in funktionale Programme überführt werden, deren Korrektheit leicht mit den bestehenden Systemen gezeigt werden kann. Im Gegensatz zu existierenden Transformationen soll dieses Verfahren auf die Verifikation hin ausgerichtet sein, so daß im Vergleich zu bekannten Übersetzungstechniken deutlich leichter zu verifizierende Zielprogramme erzeugt werden. Der praktische Nutzen des entwickelten Verfahrens soll schließlich mit einer Implementierung unter Verwendung eines geeigneten Indusktionsbeweissystems evaluiert werden.

• DFG-Verfahren: Forschungsstipendien
• Internationaler Bezug: USA
• Kooperationspartner: Professor Dr. Deepak Kapur