Abstract is missing.
- Modeling Distributed Algorithms by Abstract State Machines Compared to Petri NetsEgon Börger. 3-34 [doi]
- A Universal Control Construct for Abstract State MachinesMichael Stegmaier, Marcel Dausend, Alexander Raschke, Matthias Tichy. 37-53 [doi]
- Encoding TLA ^+ + into Many-Sorted First-Order LogicStephan Merz, Hernán Vanzetto. 54-69 [doi]
- Proving Determinacy of the PharOS Real-Time Operating SystemSelma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz. 70-85 [doi]
- A Rigorous Correctness Proof for PastryNoran Azmy, Stephan Merz, Christoph Weidenbach. 86-101 [doi]
- Enabling Analysis for Event-BIvaylo Dobrikov, Michael Leuschel. 102-118 [doi]
- A Compact Encoding of Sequential ASMs in Event-BMichael Leuschel, Egon Börger. 119-134 [doi]
- Proof Assisted Symbolic Model Checking for B and Event-BSebastian Krings, Michael Leuschel. 135-150 [doi]
- On Component-Based Reuse for Event-BAndrew Edmunds, Colin F. Snook, Marina A. Waldén. 151-166 [doi]
- Using B and ProB for Data Validation ProjectsDominik Hansen, David Schneider, Michael Leuschel. 167-182 [doi]
- Generating Event-B Specifications from Algorithm DescriptionsJoy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel. 183-197 [doi]
- Formal Proofs of Termination Detection for Local Computations by Refinement-Based CompositionsMaha Boussabbeh, Mohamed Tounsi, Mohamed Mosbah, Ahmed Hadj Kacem. 198-212 [doi]
- How to Select the Suitable Formal Method for an Industrial Application: A SurveyFelix Kossak, Atif Mashkoor. 213-228 [doi]
- Unified Syntax for Abstract State MachinesPaolo Arcaini, Silvia Bonfanti, Marcel Dausend, Angelo Gargantini, Atif Mashkoor, Alexander Raschke, Elvinia Riccobene, Patrizia Scandurra, Michael Stegmaier. 231-236 [doi]
- A Relational Encoding for a Clash-Free Subset of ASMsGerhard Schellhorn, Gidon Ernst, Jörg Pfähler, Wolfgang Reif. 237-243 [doi]
- Towards an ASM Thesis for Reflective Sequential AlgorithmsFlavio Ferrarotti, Loredana Tec, José Maria Turull Torres. 244-249 [doi]
- A Model-Based Transformation Approach to Reuse and Retarget CASM SpecificationsPhilipp Paulweber, Uwe Zdun. 250-255 [doi]
- Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in AlloyJohn Baugh, Alper Altuntas. 256-261 [doi]
- 'The Tinker' for RodinYibo Liang, Yuhui Lin, Gudmund Grov. 262-268 [doi]
- A Graphical Tool for Event Refinement Structures in Event-BDana Dghaym, Matheus Garay Trindade, Michael J. Butler, Asieh Salehi Fathabadi. 269-274 [doi]
- Rodin Platform Why3 Plug-InAlexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, Alexander Romanovsky. 275-281 [doi]
- Semi-Automated Design Space Exploration for Formal ModellingGudmund Grov, Andrew Ireland, Maria Teresa Llano, Peter Kovacs, Simon Colton, Jeremy Gow. 282-289 [doi]
- Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B DevelopmentGuillaume Babin, Yamine Aït Ameur, Neeraj Kumar Singh, Marc Pantel. 290-296 [doi]
- UC-B: Use Case Modelling with Event-BRajiv Murali, Andrew Ireland, Gudmund Grov. 297-302 [doi]
- Interactive Model Repair by SynthesisJoshua Schmidt, Sebastian Krings, Michael Leuschel. 303-307 [doi]
- SysML2B: Automatic Tool for B Project Graphical Architecture Design Using SysMLDavid Mentré. 308-311 [doi]
- Mechanized Refinement of Communication Models with TLA ^+ +Florent Chevrou, Aurélie Hurault, Philippe Mauran, Philippe Quéinnec. 312-318 [doi]
- A Super Industrial Application of PSGraphYuhui Lin, Gudmund Grov, Colin O'Halloran, Priiya G.. 319-325 [doi]
- The Hemodialysis Machine Case StudyAtif Mashkoor. 329-343 [doi]
- How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case StudyPaolo Arcaini, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene. 344-359 [doi]
- Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-SimulationThai Son Hoang, Colin F. Snook, Lukas Ladenberger, Michael J. Butler. 360-375 [doi]
- Hemodialysis Machine in Hybrid Event-BRichard Banach. 376-393 [doi]
- Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like MethodsThomas Fayolle, Marc Frappier, Frédéric Gervais, Régine Laleau. 394-408 [doi]
- Modelling the Haemodialysis Machine with CircusArtur Oliveira Gomes, Andrew Butterfield. 409-424 [doi]