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.