ABZ 2014 conference was held from June 2d to 6th in Toulouse. It was attended by about 120 people and allowed B, Z, ASM, Alloy and VDM communities to meet and exchange ideas. The diversity and relevance of the work presented, as well as the presence of significant industrial, reflect a growing force in the community of formal methods.
Thursday allowed comparing various methods of formalization through a common case studies provided by ONERA (landing gear control system).
CLEARSY had a Method B booth all through the conference in which were exposed Atelier B 4.2 and the results of several ANR research projects. The numerous demonstrations made possible to present the new programmable proof obligations (PO) generator , PO traceability / model and the ability to translate PO to Why3 (for connection to other solvers).