Umfang

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

Empfohlene Vorkenntnisse

  • gute Clojure Kenntnisse (z.B. durch Besuch der Veranstaltung “Funktionale Programmierung”)
  • optional: Kenntnisse in Compilerbau

Problem

Mit Hilfe von lisb ist es möglich, die recht unflexible Sprachen B und Event-B aufzuweichen. Mittels einer DSL wird es ermöglicht Prädikate zu schreiben, die in die klare Semantik nach B übersetzt werden und dann von ProB gelöst werden.

Dazu ist lisb in drei Ebenen getrennt:

  • ein Frontend, was derzeit sehr an B angelehnt ist,
  • eine Zwischenrepräsentation (IR), die ebenso an B angelehnt ist,
  • ein Backend, was ein B-AST erstellt und von ProB lösen lässt.

Minimalanforderungen

  • Implementierungen von weiteren Frontends und Backends. Dies kann auch für Teilmengen der Sprachen geschehen (z.B. Alloy, SMT / Z3, SAT / Kodkod, …)

Variationen

  • verschiedene Front- und Backends
  • Evaluation der IR

Kontakt

Philipp Körner
Raum 25.12.02.56
p.koerner@hhu.de