You are here: HomeABZ 2016Accepted Papers

Accepted Papers

Full Papers

  • Selma Azaiez, Damien Doligez, Jael Kriener, Matthieu Lemerre and Stephan Merz. Proving Determinacy of PharOS in TLA+
  • Noran Azmy, Stephan Merz and Christoph Weidenbach. A Rigorous Correctness Proof for Pastry
  • Maha Boussabbeh, Mohamed Tounsi, Mohamed Mosbah and Ahmed Hadj Kacem. Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions
  • Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen and Michael Leuschel.Generating Event-B Specifications from Algorithm Descriptions
  • Ivaylo Dobrikov and Michael Leuschel. Enabling Analysis for B and Event-B
  • Andrew Edmunds, Colin Snook and Marina Waldén. On Component-based Reuse for Event-B
  • Dominik Hansen, David Schneider and Michael Leuschel. Using B and ProB for Data Validation Projects
  • Felix Kossak and Atif Mashkoor. How to Select the Suitable Formal Method for an Industrial Application: A Survey
  • Sebastian Krings and Michael Leuschel. Proof Assisted Symbolic Model Checking for B and Event-B
  • Michael Leuschel and Egon Börger. A compact encoding of sequential ASMs in Event-B
  • Stephan Merz and Hernán Vanzetto. Encoding TLA+ into Many-Sorted First-Order Logic
  • Michael Stegmaier, Marcel Dausend, Alexander Raschke and Matthias Tichy. A Universal Control Construct for Abstract State Machines

Short Papers

  • Paolo Arcaini, Silvia Bonfanti, Marcel Dausend, Angelo Gargantini, Atif Mashkoor, Alexander Raschke, Elvinia Riccobene, Patrizia Scandurra and Michael Stegmaier. Unified Syntax for Abstract State Machines
  • Guillaume Babin, Yamine Ait Ameur, Neeraj Singh and Marc Pantel. Handling continuous functions in hybrid systems reconfigurations : a formal Event-B development
  • John Baugh and Alper Altuntas. Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy
  • Florent Chevrou, Aurélie Hurault and Philippe Queinnec. Mechanized Refinement of Communication Models with TLA+
  • Dana Dghaym, Matheus Garay Trindade, Michael Butler and Asieh Salehi Fathabadi. A Graphical Tool for Event Refinement Structures in Event-B
  • Gidon Ernst, Gerhard Schellhorn, Jörg Pfähler and Wolfgang Reif. A Relational Encoding for a Clash-Free Subset of ASMs
  • Flavio Ferrarotti, Loredana Tec and José María Turull Torres. Towards an ASM Thesis for Reflective Sequential Algorithms
  • Gudmund Grov, Andrew Ireland, Maria Teresa Llano Rodriguez, Peter Kovacs, Simon Colton and Jeremy Gow. Semi-Automated Design Space Exploration for Formal Modelling
  • Alexei Iliasov, Paulius Stankaitis and Alexander Romanovsky. Rodin Platform Why3 plug-in
  • Yibo Liang, Yuhui Lin and Gudmund Grov. 'The Tinker' for Rodin
  • Yuhui Lin, Gudmund Grov, Colin O'Halloran and Priiya G. A super industrial application of PSGraph
  • David Mentré. SysML2B: automatic tool for B project graphical architecture design using SysML
  • Rajiv Murali, Andrew Ireland and Gudmund Grov. UC-B: Use Case Modelling with Event-B
  • Philipp Paulweber and Uwe Zdun. A Model-based Transformation Approach to Reuse and Retarget CASM Specifications
  • Joshua Schmidt, Sebastian Krings and Michael Leuschel. Interactive Model Repair by Synthesis

Case Study Papers

  • Paolo Arcaini, Silvia Bonfanti, Angelo Gargantini and Elvinia Riccobene. How to assure correctness and safety of medical software: the Hemodialysis Machine Case Study
  • Richard Banach. Hemodialysis Machine in Hybrid Event-B
  • Andrew Butterfield and Artur Oliveira Gomes. Modelling the Haemodialysis Machine with Circus
  • Thomas Fayolle, Marc Frappier, Frederic Gervais and Regine Laleau. Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods
  • Thai Son Hoang, Colin Snook, Lukas Ladenberger and Michael Butler. Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation