Archives de l’auteur : ClearSy
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
Jean Louis Dufour (Sagem Défense & Sécurité, ), will come to the AdaCore Paris offices to give a 101 introduction to the B-Method (June 26, 2012 – Paris, France) Source: adacore internal seminar
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
Rodin 2.5 is available on Sourceforge
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
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.