Faculty of Computer Science

Research Group Theoretical Computer Science

Oberseminar: Heterogene formale Methoden

Abstract:

Das Heterogene Toolset (Hets) ist ein umfängliches System für das Zusammenführen formaler Methoden und die Verwaltung von Beweisen, kann aber keine Beweisgraphen aus den Beweisen gewinnen, die es verwaltet. Dieser Vortrag soll darlegen, wie diese Fähigkeit zu Hets hinzugefügt werden kann. Es werden die relevanten theoretischen Konzepte vorgestellt und mögliche Anwendungsgebiete für Beweisgraphen gezeigt. Schließlich werden die Möglichkeiten der Implementierung ergründet und die Details der finalen Implementierung vorgestellt.

The Heterogeneous Tool Set (Hets) as a general framework for formal methods integration and proof management lacks the ability to extract proof graphs from the proofs it manages. This talk lays out the process of adding that ability to Hets. It compiles the relevant theoretical concepts and presents some applications for proof graphs. It then discusses possible implementations and details the one that was ultimately implemented.