Dr. Steffen Schlager

"Deduktive Verifikation von Java-Programmen"

Zusammenfassung: Die Geschichte der deduktiven Programmverifikation reicht zurück bis in die 1960er Jahre. Trotz erfolgreicher akademischer Fallstudien ist es bis heute nicht gelungen, die Programmverifikation als Methode in die industrielle Software-Entwicklung zu integrieren. Gründe dafür sind unter anderem, dass die Verifikationswerkzeuge zumeist nur für Experten bedienbar sind und dass die in der Praxis verwendeten Programmiersprachen nicht unterstützt werden.

In diesem Vortrag gehe ich auf die Herausforderungen ein, die sich bei der deduktiven Verifikation von Programmen in einer echten Programmiersprache, nämlich Java, ergeben. Anhand der Beweisregel für die while-Schleife gebe ich einen Überblick über die Konzepte, die dem Java-Programmverifikationssystem KeY zugrunde liegen. Ferner stelle ich eine alternative Version dieser Beweisregel vor, die die Verifikation von Schleifen in der Praxis deutlich vereinfacht.