4th International ABZ 2014 Conference

ASM, Alloy, B, TLA, VDM, Z
June 2 - 6 2014
Toulouse - France

https://www.irit.fr/ABZ2014/




Programme of the week at glance

Monday June 2nd
Tuesday June 3rd
Wednesday June 4th
Thursday June
5th
Friday June
6th
ENSEEIHT Site ENSEEIHT Site IAS Site IAS Site IAS Site
RODIN Workshop RODIN Workshop Main ABZ
conference
Main ABZ conference
Case study day
Main ABZ conference
TLA Workshop City Hall Cocktail Airbus Visit
SETS Workshop Conference Dinner
Tutorial
Formal Data Validation.



The programme of the workshops and of the tutorial are available on the corresponding web sites.


The programme of the main ABZ conference is available HERE.



Invited talks
ABZ'2014 Track: Accepted Papers
ABZ'2014 Case study Track: Accepted Papers


Invited talks

Leslie LAMPORT
"TLA+ for Non-Dummies"

Gerhard SCHELLHORN
"Development of a Verified Flash File System"

Laurent VOISIN
"The Rodin Platform has turned ten"

Back

ABZ'2014 Track
Accepted Papers

Simone Zenzaro, Vincenzo Gervasi and Jacopo Soldani.
"WebASM: an Abstract State Machine execution environment for the Web"

Aleksandar Milicevic, Ido Efrati and Daniel Jackson.
"aRby-An Embedding of Alloy in Ruby"

Marcel Dausend and Alexander Raschke.
"Introducing Aspect-Oriented Specification for Abstract State Machines"

Egon Boerger and Klaus-Dieter Schewe.
"A Transaction Operator for Abstract State Machines"

Dominik Hansen and Michael Leuschel.
"Translating B to TLA+ for Validation with TLC"

Andreas Fürst, Thai Son Hoang, David Basin, Naoto Sato and Kunihiko Miyazaki.
"Formal System Modelling Using Abstract Data Types in Event-B"

Gidon Ernst, Jörg Pfähler, Gerhard Schellhorn and Wolfgang Reif.
"Modular Refinement for Submachines of ASMs"

Eerke Boiten and Jeremy Jacob.
"Modelling Sealed Containers in Z"

Sylvain Conchon and Mohamed Iguernelala.
"Tuning the Alt-Ergo SMT Solver for B Proof Obligations"

Chris Newcombe.
"Why Amazon Chose TLA+"

Graeme Smith and Qin Li.
"MAZE: An extension of Object-Z for multi-agent systems"

Inna Pereverzeva, Michael Butler, Asieh Salehi Fathabadi, Linas Laibinis and Elena Troubitsyna.
"Formal Derivation of Distributed MapReduce"

Pierre Kelsen and Loïc Gammaitoni.
"Domain-Specific Visualization of Alloy Instances"

David Delahaye, Catherine Dubois, Claude Marché and David Mentré.
"The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations"

Narek Nalbandyan, Uwe Glässer, Hamed Yaghoubi Shahir and Hans Wehn.
"Distributed Situation Analysis: A formal semantic framework"

Alcino Cunha.
"Bounded Model Checking of Temporal Formulas with Alloy"

Stefan Hallerstede.
"Quasi-Lexicographic Convergence"

Manamiary Bruno Andriamiarina, Dominique Mery and Neeraj-Kumar Singh.
"Analysis of Self-* and P2P Systems using Refinement"

José Antonio Esparza Isasa, Peter Würtz Vinther Jørgensen and Claus Ballegård Nielsen.
"Modelling Energy Consumption in Embedded Systems with VDM-RT"

Rahma Ben Ayed, Simon Collart-Dutilleul, Philippe Bon, Akram Idani and Yves Ledru.
"B Formal Validation of ERTMS/ETCS Railway Operating Rules"

Nghi Huynh, Marc Frappier, Amel Mammar and Regine Laleau.
"Validating the RBAC ANSI 2012 Standard using B"

Ed Zulkoski, Chris Kleynhans, Ming-Ho Yee, Derek Rayside and Krzysztof Czarnecki.
"Optimizing Alloy for Multi-Objective Software Product Line Configuration"

Andrew Edmunds.
"Templates: Re-use and Configuration for Event-B Code Generation"

Michael Leuschel and David Schneider.
"Solving The Jobs Puzzle Challenge in B: B as a High-Level Constraint Modelling Language"

Ferney Maldonado, Jaime Chavarriaga and Yezid Donoso.
"Detecting Network Policy Conflicts using Alloy"

Vajihollah Montaghami, Amirhosein Vakili and Derek Rayside.
"Staged Evaluation of Partial Instances in a Relational Model Finder"

Petr Devyanin, Victor Kuliamin, Alexander K. Petrenko, Alexey Khoroshilov and Ilya Shchepetkov.
"Formal Verication of OS Security Model with Alloy and Event-B"

Jérôme Guery, Olivier Rolland and Joris Rehm.
"Fixed-Point Arithmetic Modeled in B Software Using Reals"

Richard Banach.
"Invariant Guided System Decomposition"

Elvinia Riccobene and Patrizia Scandurra.
"Towards ASM-based formal specification of self-adaptive systems"

Andreas Prinz and Edel Sherratt.
"Distributed ASM - Pitfalls and Solutions"

Tsutomu Kobayashi, Fuyuki Ishikawa and Shinichi Honiden.
"Understanding and Planning Event-B Refinement through Primitive Rationales"

Back

ABZ'2014 Case study Track
Accepted Papers

Wen Su and Jean-Raymond Abrial.
"Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System"

Dominik Hansen, Lukas Ladenberger, Harald Wiegard, Jens Bendisposto and Michael Leuschel.
"Validation of the ABZ Landing Gear System using ProB"

Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene.
"Offline Model-based Testing and Runtime Monitoring of the Sensor Voting Module"

Paolo Arcaini, Angelo Gargantini and Elvinia Riccobene.
"Modeling and Analyzing using ASMs: the Landing Gear System case study"

Amel Mammar and Régine Laleau.
"Modeling a Landing Gear System in Event-B"

Philippe Dhaussy and Ciprian Teodorov.
"Context-aware Verification of a Landing Gear System"

Bernard Berthomieu, Silvano Dal Zilio and Lukasz Fronc.
"Model-Checking Real-Time Properties of an Airplane Landing Gear System Using Fiacre"

Richard Banach.
"The Landing Gear Case Study in Hybrid Event-B"

Felix Kossak.
"Landing Gear System: An ASM-based Solution for the ABZ Case Study"

Dominique Mery and Neeraj Singh.
"Modelling an Aircraft Landing System in Event-B"

Vitaly Savicks, Michael Butler and John Colley.
"Co-simulation Environment for Rodin: Landing Gear Case Study"

Back

Conference Chairs
- Yamine AIT AMEUR, INPT-ENSEEIHT and IRIT, Toulouse,France
- Klaus-Dieter SCHEWE, University of Linz and SCCH, Linz, Austria

For questions concerning ABZ 2014, contact Yamine AIT AMEUR (yamine@n7.fr) or Klaus-Dieter SCHEWE (Klaus-Dieter.schewe@scch.at).