By Yamine Ait Ameur (July 2014)
The 4th edition of the international conference ABZ took place in Toulouse from June 2nd to June 6th., 2014. The conference records the latest development in refinement and proof state based formal methods. It follows the success of the London (2008), Orford (2010) and Pisa (2012) editions.
This edition of ABZ was marked by two major events. In addition to ASM, B, Z, Alloy and VDM, ABZ 2014 has seen the introduction of TLA (Temporal Logic of Actions) as the sixth formal method covered by the scope of the conference. In order to emphasise the integration of TLA, Leslie LAMPORT gave an invited address entitled TLA+ for Non-Dummies, right in the year he was distinguished by the Turing Award.
After the Steam Boiler case study raised 20 years ago, the second event highlighting the 4th ABZ conference is the introduction of a case study track. The aeronautic context offered by the Toulouse area pushed us to look for a case study issued from this domain. Fr&eacte;d&eactute;eric Boniol and Virginie Wiels proposed a Landing Gear System to be modelled within proof and refinement state based methods in the scope of ABZ. A separate proceedings volume, also published by Springer Verlag, is dedicated to this case study.
ABZ 2014 received 81 submissions covering the whole formal methods in the scope of the conference: Alloy, ASM, B, TLA, VDM and Z. These papers range on a wide spectrum covering fundamental contributions, applications in industrial contexts and tool developments and improvements. Each paper was reviewed by at least three reviewers and the programme committee accepted 13 long papers and 19 short papers. Furthermore, 8 long and 3 short papers were accepted for the case study track published in another proceedings volume. Three workshops and one tutorial took place between June 2 and 4. More than 120 participants issued from all the continents registered to the conference.
In addition to the invited talk of Leslie Lamport, ABZ 2014 invited two other speakers. Gerhard Schellhorn from the University of Augsburg, Germany gave a talk entitled Development of a Verified Flash File System centred around the ASM formal method and Laurent Voisin from the Systerel company, France present a talk entitled The Rodin Platform has turned ten reporting the progress achieved within the Rodin platform supporting Event-B. We would like to thank the three invited speakers for their contributions to the success of ABZ 2014.
ABZ 2014 would not have succeeded without the efforts and involvement of the Programme Committee members and the external reviewers who contributed to review (more than 250 reviews) and select the best contributions. This event would not exist if authors and contributors did not submit their proposals. We address our thanks to every person, reviewer, author, programme committee members and organisation committee members involved in the success of ABZ’2014.
Finally, ABZ 2014 has received the support of several sponsors, among them Airbus, CNES, CNRS, CRITT Informatique, CS, ENSEEIHT Toulouse, Formal Methods Europe, INP Toulouse, IRIT, Midi Pyrénées Region, ONERA, SCCH, University Paul Sabatier Toulouse. Many thanks for their support.