a Lean4 framework for the modeling and refinement of stateful systems

Event-B to txt converter

Collection of various Event-B models

Open tool platform for the cost effective rigorous development of dependable complex software systems services. This platform is based on the Event-B formal method and provides natural support for refinement and mathematical proof.

First level of the Event-B specification of the HIMACF model (with role-based access control)

Rodin Platform Bundles that include features developed by our group

CamilleX extension for Rodin platform

A formal specification written in Event-B notation that formally specifies the behaviour of a multi-lift elevator system.

Uses lisb to transform an Event-B machine to a B machine. Very experimental.

Code generation project of C code from Event-B formal models. Including C metamodel files, C XText files, and Event-B to C translation rules

Adaptation of the EMF translator for Event-B and Rodin

(READ ONLY MIRROR) The Camille Editor for Rodin

Formal model and verification of a multi-cabin elevator system in Event-B/Rodin, with additional static verification in Ada/SPARK (not in repo), following a requirement specification.

Program synthesis for cyber-resilience. Generation of certified code for architectural tactics, for which we use Event-B and EventB2Java. We show how testing can be used to animate and check the generated code.

Event-B model for University Programme Management System

Source code for building Docker images for running/developing Rodin

A function to sum your sets of integers in a flash !