Publié le 12/06/2014 |

La conférence ABZ 2014 s’est tenue du 02 au 06 Juin à Toulouse. Elle a regroupé environ 120 personnes et a permis aux communautés B, Z, ASM, Alloy et VDM de se retrouver et d’échanger. La diversité et la pertinence des travaux présentés, ainsi que la présence notable d’industriels, témoignent d’une vigueur grandissante de la communauté des méthodes formelles.

La journée du jeudi a permis de comparer les différentes méthodes de formalisation au travers d’un cas d’études commun fourni par l’ONERA (système de contrôle d’un train d’atterrissage).

CLEARSY a tenu un stand Méthode B tout au long de la conférence où ont été exposés l’Atelier B 4.2 ainsi que les résultats de plusieurs projets de recherche ANR. Les nombreuses démonstrations réalisées ont permis de présenter le nouveau générateur d’obligations de preuve (OP) paramétrable, la traçabilité OP / modèle et la capacité de traduire les OP en Why3 (pour une connexion à d’autres prouveurs).