Umfang

Dieses Thema kann als Bachelorarbeit oder Teil einer Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • gute Prolog Kenntnisse (z.B. durch Besuch der Veranstaltung “Einführung in die logische Programmierung”)
  • Kenntnisse der B Sprache sind erwünscht (zB. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)

Problem

ProB ist ein am Lehrstuhl entwickeltes Werkzeug zur Analyse von Modellen der B Methode. Der Constraint-Solver von ProB wird dabei in SICStus Prolog entwickelt und setzt auf die CLP(FD)-Bibliothek auf. Andere Solver, wie die SMT Solver CVC4 und Z3 setzen hingegen auf den DPLL(T) Algorithmus und passende Entscheidungsprozeduren für Teilprobleme zur Lösung von Constraints.

Im Zuge der Arbeit soll versucht werden einen Solver für Ausdrücke in B zu schreiben, der auf dem DPLL(T)-Ansatz beruht. Dabei kann teilweise auf bestehende Arbeiten aufgesetzt werden.

Das Thema ist im Umfang relativ flexibel und ist daher als Projekt- und/oder Masterarbeit geeignet. Voraussetzungen sind (gute) Kenntnisse in Prolog und Interesse an anderen Algorithmen zum Lösen von Constraints.

Minimalanforderungen

  • funktionsfähiger DPLL(T)-Solver für eine Untermenge von B
  • Analyse der Performance auf ein paar Beispielen, Vergleich mit ProB

Erweiterungen (für Masterarbeit erforderlich)

  • Erweiterung der abgedeckten Sprache
  • Ausführliche empirische Evaluierung

Kontakt

Professor Michael Leuschel
Raum 25.12.02.60 · michael.leuschel@hhu.de