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

Probablistische Beweis-Analyse mit KeY

Typ: MA
Datum: 2017-12-11
Betreuer: Mattias Ulbrich
Mihai Herda
Aushang:

Problem

Until now, formal program verification has only two possible results: Either the proof attempt succeeds or it remains unfinished. In the former case the examined property is proved to hold. In the latter case the property can be potentially violated. Without further investigation no more specific statement about partial validity can be made. In this aspect the formal verification is inferior to non-exhaustive testing because there exist reliability metrics like code coverage for testing.

Goal

This thesis will contribute to mitigating this problem by answering the following research question: How can we estimate the practical execution coverage of an unfinished proof attempt of a Java program from KeY given a representation of the distribution of its inputs?

Kontakt: