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.
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.
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
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
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
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
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.