EB2ALL - The Event-B to C, C++, Java and C# Code Generator

EB2ALL is a set of translator tools that automatically generates efficient target programming language code (C, C++, Java and C#) from Event-B formal specification related to the analysis of the complex problems. The EB2ALL contains four plugin namely EB2C, EB2C++, EB2J and EBC#. The goal of EB2ALL is to be able to generate a verified source code that satisfies behavioral properties of the develop formal system (abstractly). The EB2ALL tool is developed as a set of plugins for RODIN development tool under the Eclipse framework. RODIN is an integrated development environment (IDE) for developing Event-B models. The RODIN tool is written entirely in Java and build on top of the Eclipse platform.

The EB2ALL tool is still in development stage, we are releasing all the EB2C, EB2C++, EB2J and EB2C# tools as beta version before final release of the EB2ALL for collecting the bugs. For downloading any tool, please visit the downloading page.