Home | B News | B Method | R&D Activities | Formal Proof | Publications | Conferences | B, the different languages | Open Source Projects | B Tools | Documents | Links | Contact

B Tools

ClearSy makes available to the general public several tools developped during various R&D projects. All these tools are related to modelling or formal proof.

programmation ClearSy B Tools

Atelier BAtelier B
A tool enabling the operational use of method B. In a coherent environment, it provides many functions for managing projects in B language.

CompoSysBEditor
Eclipse plugin enabling to edit an Atelier B model, with colorization of keywords.

CompoSysClick'n Prove
Atelier B interactive prover interface.

RODINRODIN
Event B development platform.
This is its plugins:

BramaBrama
Eclipse plugin enabling to animate a RODIN event model.

B2RODINB2RODIN
Eclipse plugin enabling to import (event B compliant) Atelier B models into RODIN plateform.

CompoSysCompoSys
Tool for formal design of systems architecture.
programmation Other B Tools freelance

ProBProB:
The ProB Animator and Model Checker for the B Method.

GenesystGenesyst:
Set of classes that use BoB to generate labelled transition systems representing the exact behaviour of an Event B specification or refinement.

La BOBLa BOB:
Set of Java classes to handle B constructions.