Archives mensuelles : mai 2012

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

B-Method – AdaCore micro-seminar

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

Publié dans Event | Laisser un commentaire