Below you find an overview of our software projects.
ProB is an animator and model checker for the B-Method. It allows fully automatic animation of many B specifications, and can be used to systematically check a specification for errors. ProB Homepage
BMotion Studio is a visual editor which enables the developer of a formal model to set-up easily a domain specific visualization for discussing it with the domain expert. BMotion Studio Homepage
We have since replaced BMotionStudio with VisB. VisB is based on SVG graphics and allows faster development of domain-specific visualisations.
Ecce is an automatic online program specialiser for pure Prolog programs (with built-ins). It takes a pure Prolog program and a query of interest and then specialises the program for that particular query. Ecce Homepage
LOGEN is an offline partial evaluation system for Prolog written using the so called "cogen approach". Basically, the cogen is a system which: based upon an annotated version of the program to be specialised produces a specialised partial evaluator for that program. This partial evaluator is called a generating extension the generating extension can be used to specialise the program in a very efficient manner.
Logen vs Ecce
The choice on which tool to use depends on the particular application. Ecce is a fully automatic online specialiser. It is hence easier to use by inexperienced users, but more difficult to tweak in case specialisation does not proceed as desired. Ecce uses more refined control techniques and can perform conjunctive partial deduction and slicing, which Logen cannot. Because of the additional annotation phase, Logen is more difficult to master by inexperienced users, but the outcome of the specialisation is easier to tweak and predict. The specialisation phase of Logen is very efficient, with very little overhead compared to ordinary evaluation. Logen can deal with almost full Prolog, whereas Ecce only deals with declarative Prolog programs. The latter restricts the range of programs to which Ecce can be applied, but it also allows Ecce to perform more powerful optimisations.