Model Generation

Typ:	SA / BA / MA / DA
Datum:
Betreuer:	Christoph Gladisch
Aushang:

Kontext

Bei welcher Eingabe Stürzt ein Programm ab? Sind die Axiome, die ich mir definiert habe überhaupt erfüllbar? - Die Antwort zu solchen Fragen zu finden ist das Problem der Modellgenerierung. Ein Modell in dem hier gemeinten Sinne ist eine Interpretation einer prädikatenlogischen Formel, welche die Formel zu „true“ evaluiert. Modellgenerierung ist ein aktuelles Forschungsthema. In den letzten Jahren wurden große Fortschritte auf diesem Gebiet gemacht. Modellgenerierung wird in Softwaretesten und in Softwareverifikation benutzt.

State-of-the-Art Techniken auf diesem Gebiet sind sogenannte SMT-Solver. Diese erreichen jedoch Ihre Grenzen, wenn Modelle für quantifizierte Formeln erzeugt werden sollen. Uns ist es gelungen, ein allgemeineres Verfahren zu entwickeln, mit dem auch Modelle für quantifizierte Formeln erzeugt und verifiziert werden können. Aufgabenstellung

Eine Instanz dieses Verfahren haben wir bereits in einem Prototypen implementiert. In der Studien- oder Bachelorarbeit soll der Prototyp automatisiert werden. Dazu müssen u.a. Heuristiken für die Modellsuche entwickelt werden. In der Diplom-/Masterarbeit soll eine neue allgemeinere Instanz des Verfahrens entwickelt werden. Dazu soll die bisher verwendete Sprache zur Modellrepräsentation sowie das Beweisverfahren zur Verifikation von Modellen verallgemeinert werden. Zur Evaluation sollen Modellklassen für häufig verwendete Axiome entwickelt und verifiziert werden. Die Schwerpunkte liegen auf Theorie und Implementierung.

Voraussetzungen

• Gute Kenntnisse in Logik (z. B. Vorlesung „Formale Systeme“) und in Java-Programmierung
• Interesse an Forschung