| 2016 | 'The Tinker' for Rodin. Yibo Liang, Yuhui Lin, Gudmund Grov |
| 2016 | A Compact Encoding of Sequential ASMs in Event-B. Michael Leuschel, Egon Börger |
| 2016 | A Graphical Tool for Event Refinement Structures in Event-B. Dana Dghaym, Matheus Garay Trindade, Michael J. Butler, Asieh Salehi Fathabadi |
| 2016 | A Model-Based Transformation Approach to Reuse and Retarget CASM Specifications. Philipp Paulweber, Uwe Zdun |
| 2016 | A Relational Encoding for a Clash-Free Subset of ASMs. Gerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif |
| 2016 | A Rigorous Correctness Proof for Pastry. Noran Azmy, Stephan Merz, Christoph Weidenbach |
| 2016 | A Super Industrial Application of PSGraph. Yuhui Lin, Gudmund Grov, Colin O'Halloran, Priiya G. |
| 2016 | A Universal Control Construct for Abstract State Machines. Michael Stegmaier, Marcel Dausend, Alexander Raschke, Matthias Tichy |
| 2016 | Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings Michael J. Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklós Biró |
| 2016 | Enabling Analysis for Event-B. Ivaylo Dobrikov, Michael Leuschel |
| 2016 | Encoding TLA ^+ + into Many-Sorted First-Order Logic. Stephan Merz, Hernán Vanzetto |
| 2016 | Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions. Maha Boussabbeh, Mohamed Tounsi, Mohamed Mosbah, Ahmed Hadj Kacem |
| 2016 | Generating Event-B Specifications from Algorithm Descriptions. Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel |
| 2016 | Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development. Guillaume Babin, Yamine Aït Ameur, Neeraj Kumar Singh, Marc Pantel |
| 2016 | Hemodialysis Machine in Hybrid Event-B. Richard Banach |
| 2016 | How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study. Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene |
| 2016 | How to Select the Suitable Formal Method for an Industrial Application: A Survey. Felix Kossak, Atif Mashkoor |
| 2016 | Interactive Model Repair by Synthesis. Joshua Schmidt, Sebastian Krings, Michael Leuschel |
| 2016 | Mechanized Refinement of Communication Models with TLA ^+ +. Florent Chevrou, Aurélie Hurault, Philippe Mauran, Philippe Quéinnec |
| 2016 | Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets. Egon Börger |
| 2016 | Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy. John W. Baugh Jr., Alper Altuntas |
| 2016 | Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods. Thomas Fayolle, Marc Frappier, Frédéric Gervais, Régine Laleau |
| 2016 | Modelling the Haemodialysis Machine with Circus. Artur Oliveira Gomes, Andrew Butterfield |
| 2016 | On Component-Based Reuse for Event-B. Andrew Edmunds, Colin F. Snook, Marina Waldén |
| 2016 | Proof Assisted Symbolic Model Checking for B and Event-B. Sebastian Krings, Michael Leuschel |
| 2016 | Proving Determinacy of the PharOS Real-Time Operating System. Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz |
| 2016 | Rodin Platform Why3 Plug-In. Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, Alexander B. Romanovsky |
| 2016 | Semi-Automated Design Space Exploration for Formal Modelling. Gudmund Grov, Andrew Ireland, Maria Teresa Llano, Peter Kovacs, Simon Colton, Jeremy Gow |
| 2016 | SysML2B: Automatic Tool for B Project Graphical Architecture Design Using SysML. David Mentré |
| 2016 | The Hemodialysis Machine Case Study. Atif Mashkoor |
| 2016 | Towards an ASM Thesis for Reflective Sequential Algorithms. Flavio Ferrarotti, Loredana Tec, José Maria Turull Torres |
| 2016 | UC-B: Use Case Modelling with Event-B. Rajiv Murali, Andrew Ireland, Gudmund Grov |
| 2016 | Unified Syntax for Abstract State Machines. Paolo Arcaini, Silvia Bonfanti, Marcel Dausend, Angelo Gargantini, Atif Mashkoor, Alexander Raschke, Elvinia Riccobene, Patrizia Scandurra, Michael Stegmaier |
| 2016 | Using B and ProB for Data Validation Projects. Dominik Hansen, David Schneider, Michael Leuschel |
| 2016 | Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation. Thai Son Hoang, Colin F. Snook, Lukas Ladenberger, Michael J. Butler |