


default search action
ABZ 2016: Linz, Austria
- Michael J. Butler

, Klaus-Dieter Schewe, Atif Mashkoor
, Miklós Biró
:
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings. Lecture Notes in Computer Science 9675, Springer 2016, ISBN 978-3-319-33599-5
Keynote Article
- Egon Börger:

Modeling Distributed Algorithms by Abstract State Machines Compared to Petri Nets. 3-34
Regular Research Articles
- Michael Stegmaier, Marcel Dausend, Alexander Raschke, Matthias Tichy:

A Universal Control Construct for Abstract State Machines. 37-53 - Stephan Merz, Hernán Vanzetto:

Encoding TLA ^+ + into Many-Sorted First-Order Logic. 54-69 - Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal

, Stephan Merz:
Proving Determinacy of the PharOS Real-Time Operating System. 70-85 - Noran Azmy, Stephan Merz, Christoph Weidenbach:

A Rigorous Correctness Proof for Pastry. 86-101 - Ivaylo Dobrikov, Michael Leuschel:

Enabling Analysis for Event-B. 102-118 - Michael Leuschel, Egon Börger:

A Compact Encoding of Sequential ASMs in Event-B. 119-134 - Sebastian Krings

, Michael Leuschel:
Proof Assisted Symbolic Model Checking for B and Event-B. 135-150 - Andrew Edmunds, Colin F. Snook

, Marina Waldén:
On Component-Based Reuse for Event-B. 151-166 - Dominik Hansen, David Schneider, Michael Leuschel:

Using B and ProB for Data Validation Projects. 167-182 - Joy Clark, Jens Bendisposto, Stefan Hallerstede, Dominik Hansen, Michael Leuschel:

Generating Event-B Specifications from Algorithm Descriptions. 183-197 - Maha Boussabbeh, Mohamed Tounsi

, Mohamed Mosbah
, Ahmed Hadj Kacem:
Formal Proofs of Termination Detection for Local Computations by Refinement-Based Compositions. 198-212 - Felix Kossak

, Atif Mashkoor
:
How to Select the Suitable Formal Method for an Industrial Application: A Survey. 213-228
Short Articles (Work in Progress)
- Paolo Arcaini

, Silvia Bonfanti
, Marcel Dausend, Angelo Gargantini, Atif Mashkoor
, Alexander Raschke, Elvinia Riccobene, Patrizia Scandurra
, Michael Stegmaier:
Unified Syntax for Abstract State Machines. 231-236 - Gerhard Schellhorn, Gidon Ernst

, Jörg Pfähler, Wolfgang Reif
:
A Relational Encoding for a Clash-Free Subset of ASMs. 237-243 - Flavio Ferrarotti

, Loredana Tec, José Maria Turull Torres:
Towards an ASM Thesis for Reflective Sequential Algorithms. 244-249 - Philipp Paulweber

, Uwe Zdun:
A Model-Based Transformation Approach to Reuse and Retarget CASM Specifications. 250-255 - John W. Baugh Jr.

, Alper Altuntas
:
Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy. 256-261 - Yibo Liang, Yuhui Lin, Gudmund Grov:

'The Tinker' for Rodin. 262-268 - Dana Dghaym, Matheus Garay Trindade, Michael J. Butler

, Asieh Salehi Fathabadi
:
A Graphical Tool for Event Refinement Structures in Event-B. 269-274 - Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, Alexander B. Romanovsky

:
Rodin Platform Why3 Plug-In. 275-281 - Gudmund Grov, Andrew Ireland, Maria Teresa Llano, Peter Kovacs, Simon Colton, Jeremy Gow:

Semi-Automated Design Space Exploration for Formal Modelling. 282-289 - Guillaume Babin

, Yamine Aït Ameur, Neeraj Kumar Singh, Marc Pantel:
Handling Continuous Functions in Hybrid Systems Reconfigurations: A Formal Event-B Development. 290-296 - Rajiv Murali, Andrew Ireland, Gudmund Grov:

UC-B: Use Case Modelling with Event-B. 297-302 - Joshua Schmidt, Sebastian Krings

, Michael Leuschel:
Interactive Model Repair by Synthesis. 303-307 - David Mentré:

SysML2B: Automatic Tool for B Project Graphical Architecture Design Using SysML. 308-311 - Florent Chevrou, Aurélie Hurault, Philippe Mauran, Philippe Quéinnec:

Mechanized Refinement of Communication Models with TLA ^+ +. 312-318 - Yuhui Lin, Gudmund Grov, Colin O'Halloran, Priiya G.:

A Super Industrial Application of PSGraph. 319-325
Articles Contributing to the Hemodialysis Machine Case Study
- Atif Mashkoor

:
The Hemodialysis Machine Case Study. 329-343 - Paolo Arcaini

, Silvia Bonfanti
, Angelo Gargantini, Elvinia Riccobene:
How to Assure Correctness and Safety of Medical Software: The Hemodialysis Machine Case Study. 344-359 - Thai Son Hoang

, Colin F. Snook
, Lukas Ladenberger, Michael J. Butler
:
Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation. 360-375 - Richard Banach:

Hemodialysis Machine in Hybrid Event-B. 376-393 - Thomas Fayolle, Marc Frappier, Frédéric Gervais, Régine Laleau:

Modelling a Hemodialysis Machine Using Algebraic State-Transition Diagrams and B-like Methods. 394-408 - Artur Oliveira Gomes, Andrew Butterfield

:
Modelling the Haemodialysis Machine with Circus. 409-424

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














