Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

A Divide-and-Conquer Strategy with Block and Loop Contracts for Deductive Program Verification

Forschungsthema:KeY
Typ: BA
Datum: 2017-07-13
Betreuer: Michael Kirsten
Mattias Ulbrich
Aushang:

Ziel

Beweise über komplexe und größere Programme werden schnell sehr unübersichtlich und unhandlich, insbesondere wenn der erfolgreiche Beweis erst durch mehrere Iterationen zwischen Spezifikationsänderungen und Beweisführungen gefunden werden kann.

Um Beweise über komplexere und größere Methoden zu führen, ist es also hilfreich wenn der Beweis in verschiedene (unabhängig bearbeitbare) Teilbeweise aufgetrennt werden kann, die sich jeweils nur auf Teile der zu beweisenden Methode beziehen.

Innerhalb dieser Abschlussarbeit soll ein Weg gefunden und implementiert werden, solche Auftrennungen korrekt vorzunehmen. Hierzu sollen sogenannte Block-Verträge, eine bereits bestehende JML-Erweiterung, genutzt werden, mittels derer sich beliebige Programmteile innerhalb von Methoden spezifizieren lassen.

Voraussetzungen

  • Erfahrung im Programmieren mit Java
  • Kenntnisse, wie sie in der Vorlesung Formale Systeme vermittelt werden, sind hilfreich

Betreuung und Kontakt