Integrating Bounded Model Checking with KeY

Typ: MA
Datum: 2017-07-14
Betreuer: Mattias Ulbrich
Michael Kirsten
Bearbeiter:
Aushang:

Ziel

In Kooperation mit der Technischen Universität Darmstadt sowie der Technischen Hochschule Chalmers entwickelt unser Lehrstuhl das Software-Verifikations-Werkzeug KeY, mit dem die formale Korrektheit von Java-Programmen bezüglich gültiger JML-Verträge bewiesen werden kann. Der Regelsatz von KeY unterstützt hierzu einige Datentypen, die für einen formalen Beweis in logische Formeln überführt werden.

Allerdings gibt es auch Datentypen wie beispielsweise Bit-Vektoren, bei denen andere explorierende Techniken geeigneter scheinen. Innerhalb dieser Abschlussarbeit soll nun ein Konzept untersucht und implementiert werden, um Beweisverpflichtungen für Bit-Vektor-Variablen aus KeY zu extrahieren und hierfür einen bounded model checker (z. B. Java Pathfinder oder CBMC) zu beauftragen, der gut damit umgehen kann. Anschließend soll das Ergebnis wieder von KeY verarbeitet werden können.

Kontakt: