Archives de catégorie : Tools

Atelier B Open Source Tools Map

  At the occasion of the forthcoming Atelier B 4.1 release, a map referencing the open-source projects is published. All the open-source tools are hosted on Sourceforge facilities.

Publié dans Tools | 2 commentaires

Bug Status Section Updated

With the forcoming Atelier B 4.1 Community Edition (to be released in September 2012), the Bug Status section has been updated.

Publié dans Tools | Laisser un commentaire

Atelier B 4.x at Reliable Software Workshop (Paris)

The  Journées  sur la Fiabilité du Logiciel organized  on June 14-15, 2012 by the Initiative de Recherche et Innovation sur le Logiciel Libre  and the Groupe Thématique Logiciel Libre du pôle System@tic adress validation, certification, proof and code analysis.  At this occasion, … Continuer la lecture

Publié dans Event, Tools | 2 commentaires

Why3 as another proof toolchain for Atelier B

In 2011,  Why3 proof tool-chain has been plugged into Atelier B, in order to transform Proof Obligations generated by Atelier B into Why3 verification conditions.  Those verification conditions can then be checked with several automatic provers (Alt-Ergo, CVC3 and Z3). Overall, the … Continuer la lecture

Publié dans Research, Tools | Un commentaire

Development of a generic proof obligation generator

Atelier B proof obligation generator was developped in the early 90’s. Developped with the prolog-like “theory language”, this tool is very sensible to modifications and difficult to adapt to language extensions/modifications. The idea is to develop a generic proof obligation … Continuer la lecture

Publié dans Research, Tools | 2 commentaires

Rodin 2.5 released

Rodin 2.5 is available on Sourceforge

Publié dans Tools | Laisser un commentaire

Integration of ProB

ProB model-checker is being integrated in Atelier B 4.0, in order to provide additional proof power and animation capabilities to Atelier B. With the help of Pr. Michael Leuschel, a MacOS prototype has been developped, allowing to animate and model-check a … Continuer la lecture

Publié dans Research, Tools | Laisser un commentaire

Port & development of Brama model animator to Atelier B

Atelier B 4.0 natively supporting event B, animating such models is mandatory.  The Brama  animator has been ported on Atelier B 4.0 environment: the predicateB predicate evaluator has been ported to C++ and connected with B-Compiler.

Publié dans Applications, Tools | Laisser un commentaire