Abstract State Machines, Alloy, B, TLA, VDM, and Z

Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets.- A Universal Control Construct for Abstract State Machines.- Encoding TLA+ into Many-Sorted First-Order Logic.- Proving Determinacy of PharOS in TLA+.- A Rigorous Correctness Proof for Pastry.- Enabling Analysis for B and Event-B.- A Compact Encoding of Sequential ASMs in Event-B.- Proof Assisted Symbolic Model Checking for B and Event-B.- On Component-based Reuse for Event-B.- Using B and ProB for Data Validation Projects.- Generating Event-B Specifications from Algorithm Descriptions.- Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions.- How to Select the Suitable Formal Method for an Industrial Application: A Survey.- Unified Syntax for Abstract State Machines.- A Relational Encoding for a Clash-Free Subset of ASMs.- Towards an ASM Thesis for Reflective Sequential Algorithms.- A Model-based Transformation Approach to Reuse and Retarget CASM Specifications.- Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy.- `The Tinker' for Rodin.- A Graphical Tool for Event Refinement Structures in Event-B.- Rodin Platform Why3 plug-in.- Semi-Automated Design Space Exploration for Formal Modelling.- Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development.- UC-B: Use Case Modelling with Event-B.- Interactive Model Repair by Synthesis.- SysML2B: Automatic Tool for B Project Graphical Architecture Design using SysML.- Mechanized Refinement of Communication Models with TLA+.- A Super Industrial Application of PSGraph.- The Hemodialysis Machine Case Study.- How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study.- Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotionStudio, and Co-simulation.- Hemodialysis Machine in Hybrid Event-B.- Modeling a Hemodialysis Machine using Algebraic State-Transition Diagrams and B-like Methods.- Modelling the Haemodialysis Machine with Circus.