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