ProB Virtual Machine

ProB ist ein am Lehrstuhl entwickeltes Werkzeug zur Analyse von Modellen der B Methode. Im Prinzip arbeitet ProB als eine Art Interpreter, der einen Kern aufruft, der Lösungen zu logischen Gleichungen sucht. Dabei entsteht ein evtl. unnötiger Aufwand durch das Heraussuchen von Variablenwerten aus einem Zustand, das Zusammenstellen eines neuen Zustands, und einiger anderer Dinge, die eigentlich nicht zum Lösen des Kernproblems benötigt sind. Thema der Arbeit ist die Entwickelung einer Art "virtueller Maschine", also eine Übersetzung von B in eine Art Bytecode und dazu ein Interpreter, der auf diesem Bytecode arbeitet.

Das Thema ist als Projekt und/oder Masterarbeit gedacht. Voraussetzungen sind (gute) Kenntnisse in Prolog und Grundkenntnisse in B. Auch sollte man wissen, was z.B. ein abstrakter Syntaxbaum (AST) ist (Thema des Compilerbaus).