Software
Hier finden Sie eine Übersicht über die am Lehrstuhl entwickelte Software.
ProB
ProB ist ein Animator und Model Checker für Modelle der B-Method. ProB unterstützt die automatische Animation vieler B Spezifikationen und kann verwendet werden um diese systematisch nach Fehlern abzusuchen. ProB Homepage
BMotion Studio
BMotion Studio ist ein visueller Editor, der es dem Entwickler eines formalen Modells ermöglicht, eine domänenspezifische Visualisierung zu erzeugen und mit einem Domänenexperten zu diskutieren. BMotion Studio Homepage
Mittlerweile wurde BMotion Studion durch VisB ersetzt. VisB arbeitet auf Basis von SVG-Grafiken und ermöglicht es, noch schneller domänenspezifische Visualisierungen zu erstellen.
PyPy
PyPy ist eine schnelle, standardkompatible Alternativimplementation der Programmiersprache Python (2.7, 3.9, 3.8). PyPy Homepage
Ecce
Ecce ist ein automatischer online Programmspezialisierer für rein logische Prolog Programme (inklusive built-ins). Ecce bekommt ein rein logisches Prolog Programm und eine Anfrage und liefert ein auf die Anfrage spezialisiertes Programm zurück. Ecce Homepage
Logen
Logen ist ein offline partieller Auswerter, der den sogenannten "cogen approach" verwendet. Im Grunde genommen ist ein "cogen" ein System, das eine anmontierte Version des zu spezialisierenden Programms verwendet um einen spezialisierter partiellen Auswerter zugeschnitten auf das Eingabeprogramm zu generieren. Dieser Auswerter wird als "generating extension" bezeichnet und kann verwendet werden um das Eingabeprogramm effizient zu spezialisieren.
Logen vs Ecce
Die Entscheidung zwischen Logen und Ecce basiert auf der Anwendung. Ecce funktioniert autonom und kann so einfacher von unerfahrenen Anwendern eingesetzt werden. Dafür ist es komplizierter einzugreifen, falls die Spezialisierung nicht wie erwartet funktioniert. Im Gegensatz zu Logen beherrscht Ecce conjunctive partial deduction und Slicing.
Aufgrund der benötigten Annotationen ist Logen für unerfahrene Anwender schwieriger einzusetzen. Dafür ist es einfacher, die Spezialisierung anzupassen und Ergebnisse vorherzusagen. In der Spezialisierungsphase arbeitet Logen sehr effizient, es kommt kaum zu Overhead gegenüber gewöhnlicher Auswertung.
Logen kann mit nahezu allen Prolog Programmen umgehen, während Ecce nur deklarative Prolog Programme spezialisieren kann. Diese Einschränkung reduziert zwar die Programme auf die Ecce angewendet werden kann, ermöglicht aber den Einsatz effizienter Optimierungen.