Umfang

Dieses Thema kann als Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • logische Programmierung
  • objektorientierte Programmierung
  • SAT und SMT Solving

Problemstellung

ProB ist ein animator und model checker für B und Event-B. Die Grundlage hierfür ist ein Constraint Solver für die B Sprache welcher Techniken des Constraint Logic Programming verwendet. Neben dem eigenen Constraint Solver hat ProB Schnittstellen zu verschiedenen externen Constraint Solvern wie z.B. Z3. Für die Integration von Z3 werden B Constraints über das C Interface von Z3 in die SMT-LIB Sprache übersetzt. Diese Integration hat einige Vorteile im Vergleich zu ProB’s eigenem Constraint Solver gezeigt, wobei es auch einige Schwachstellen gibt. In dieser Arbeit soll eine ähnliche Integration des Yices SMT Solver implementiert werden. SMT-LIB ist die standard Eingabesprache für die meisten SMT-Solver. Unsere Übersetzung für die Integration von Z3 verwendet jedoch Lambda Ausdrücke die spezifisch für Z3 sind (siehe hier). Diese Übersetzungen mittels Lambda Ausdrücken müssen also für Yices angepasst werden. Insgesamt können aber einige Teile der Integration von Z3 wiederverwendet werden. Die Schnittstelle zu Yices muss jedoch entsprechend dem C Interface neu implementiert werden.

Minimalanforderungen

  • Übersetzung von B nach SMT-LIB
  • Integration in ProB
  • Formalisierung der Übersetzungsregeln

Erweiterungen

  • parallele Einbindung verschiedener Solverkonfigurationen

Kontakt

Joshua Schmidt
Raum 25.12.02.52 · joshua.schmidt@hhu.de