Verification of imperative programs

• Applicant: Professor Dr. Jürgen Giesl
• Subject Area: Theoretical Computer Science
• Term: from 1999 to 2001
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 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 Programme: Research Fellowships
• International Connection: USA
• Cooperation Partner: Professor Dr. Deepak Kapur