Philipp Paulweber, Emmanuel Pescosta and Uwe Zdun. CASM-IR: Uniform ASM-Based Intermediate Representation for Model Specification, Execution, and Transformation
Flavio Ferrarotti, Senén González, Klaus-Dieter Schewe and Jose Maria Turull Torres. Systematic Refinement of Abstract State Machines with Higher-Order Logic
Tueno Fotso Steve Jeffrey, Amel Mammar, Regine Laleau and Marc Frappier. Event-B Expression and Validation of Translation Rules Between SysML/KAOS Domain Models and B System Specifications
Richard Banach. Issues in Automated Urban Train Control: 'Tackling' the Rugby Club Problem
Farah Al-Shareefi, Alexei Lisitsa and Clare Dixon. Formal Resolution of Ambiguity for the Simple Authentication and Security Layer
Sebastian Krings, Joshua Schmidt, Carola Brings, Marc Frappier and Michael Leuschel. A Translation from Alloy to B
Jure Kukovec, Thanh Hai Tran and Igor Konnov. Extracting Symbolic Transitions from TLA+ Specifications
Kaiyuan Wang, Allison Sullivan, Manos Koukoutos, Darko Marinov and Sarfraz Khurshid. Systematic Generation of Non-Equivalent Expressions for Relational Algebra
Kaiyuan Wang, Allison Sullivan, Darko Marinov and Sarfraz Khurshid. Solver-based Sketching of Alloy Models using Test Valuations
Christoph Beierle and Klaus-Dieter Schewe. Abstract State Machines with Exact Real Arithmetic
Chenyang Zhu, Michael Butler and Corina Cirstea. Refinement of Timing Constraints for Concurrent Tasks with Queue Based Scheduling
Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel and Neeraj Kumar Singh. Proof-based approach to hybrid systems development: Dynamic Logic and Event-B
Mohammadsadegh Dalvandi, Michael Butler, Abdolbaghi Rezazadeh and Asieh Salehi Fathabadi. Verifiable Code Generation from Scheduled Event-B Models
Case Study Papers
Tueno Fotso Steve Jeffrey, Marc Frappier, Regine Laleau and Amel Mammar. Modeling the Hybrid ERTMS/ETCS Level 3 Standard Using a Formal Requirements Engineering Approach
Paolo Arcaini, Pavel Ježek and Jan Kofron. Modelling the Hybrid ERTMS/ETCS Level 3 Case Study in Spin
Dana Dghaym, Mike Poppleton and Colin Snook. Diagram-led formal modelling using iUMLB for Hybrid ERTMS Level 3
Dominik Hansen, Michael Leuschel, Sebastian Krings, Philipp Koerner, David Schneider, Thomas Naulin, Frank Skowron and Nader Nayeri. Using a B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains
Alcino Cunha and Nuno Macedo. Validating the Hybrid ERTMS/ETCS Level 3 Concept with Electrum
Amel Mammar, Marc Frappier, Regine Laleau and Steve Jeffrey Tueno Fotso. An Event-B Model of the ERTMS/ETCS Level 3 Standard
Jean-Raymond Abrial. The ABZ-2018 Case Study with Event-B
Short Papers
Lilian Burdy and David Deharbe. Teaching an Old Dog New Tricks : The Drudges of the Interactive Prover in Atelier B
Markus Leitz and Alexander Raschke. Formal Specification of the Semantics of Control State Diagrams
Jinxin Chen, Wen Su and Shehroz Khan. A Case Study of Modular Modeling of Hybrid System Using Event-B
John Baugh and Tristan Dyer. State-Based Formal Methods in Scientific Computation
Silvia Bonfanti, Angelo Gargantini and Atif Mashkoor. AsmetaA: Animator for Abstract State Machines
Julien Brunel, David Chemouil, Alcino Cunha, Thomas Hujsa, Nuno Macedo and Jeanne Tawa. An Action Layer for Lightweight Behavioral and Structural Modeling
Guillaume Bury, Simon Cruanes, David Delahaye and Pierre-Louis Euvrard. An Automation-Friendly Set Theory for the B Method
Inna Vistbakka, Mikhail Barash and Elena Troubitsyna. Towards Creating a DSL Facilitating Modelling of Dynamic Access Control in Event-B
Frédéric Badeau, Vincent Lacroix, Vincent Monfort, Laurent Voisin and Christophe Métayer. Modelling Dynamic Data Structures with the B Method
Yamine Ait Ameur, Dominique Mery, Idir Ait Sadoune, Neeraj Singh, Laurent Voisin and Gibson Paul. On the importance of explicit domain modelling in refinement-based modelling design. Experiments with Event-B
Klaus-Dieter Schewe, Loredana Tec and Qing Wang. Capturing Membrane Computing by ASMs