Archives de catégorie : Research

BWare: a new project on proving B proof obligations

BWare, a  new research project related to the B method has started in September 2012. It is  funded for a period of 4 years by the programme “Ingénierie Numérique & Sécurité” of the French national agency ANR. This project is aimed at providing … Continuer la lecture

Publié dans Research | Laisser un commentaire

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

DEPLOY project completed

Started in February 2008, the DEPLOY project,  probably the biggest Formal Method project ever funded by the European Community, completed in April 2012. During more than 4 years, 86 researchers and engineers from 14 partners have collaborated to the development, improvement and assessment of … Continuer la lecture

Publié dans Event, Research | 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