Michael J. Butler

203 papers A 2B 22C 38Misc 8Journal 55Unranked 68
YearRankTypeTitle / Venue / Authors
2025 C conf
Developing Safe Exception Recovery Mechanisms for CHERI Capability Hardware Using UML-B Formal Analysis.
ABZ
Colin F. Snook, Asieh Salehi Fathabadi, Thai Son Hoang, Robert Thorburn, Michael J. Butler, Leonardo Aniello, Vladimiro Sassone
2025 J jnl
Systematic hierarchical analysis of requirements for critical systems.
Innov. Syst. Softw. Eng.
Asieh Salehi Fathabadi, Colin F. Snook, Dana Dghaym, Thai Son Hoang, Fahad Alotaibi, Michael J. Butler
2024 J jnl
An AIC-based approach for articulating unpredictable problems in open complex environments.
CoRR
Haider Al-Shareefy, Michael J. Butler, Thai Son Hoang
2024 C conf
An Event-B Formal Model for Access Control and Resource Management of Serverless Apps.
ABZ
Mehmet Said Nur Yagmahan, Abdolbaghi Rezazadeh, Michael J. Butler
2024 — ch.
Analysing the Safety Implications of Security Risks in Cyber-Physical Systems.
The Practice of Formal Methods (II)
Colin F. Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Michael J. Butler, Martin Kubisch
2024 — conf
CuneiForm Method for Assuring the Safety of ML-Based Computer Vision Development Datasets.
RE Workshops
Haider Al-Shareefy, Michael J. Butler, Thai Son Hoang
2024 C conf
Designing Exception Handling Using Event-B.
ABZ
Asieh Salehi Fathabadi, Colin F. Snook, Thai Son Hoang, Robert Thorburn, Michael J. Butler, Leonardo Aniello, Vladimiro Sassone
2024 C conf
Event-B Development of Modelling Human Intervention Request in Self-driving Vehicle Systems.
ABZ
Fahad Alotaibi, Thai Son Hoang, Asieh Salehi Fathabadi, Michael J. Butler
2024 C conf
Semantics Formalisation - From Event-B Contexts to Theories.
ABZ
Thai Son Hoang, Laurent Voisin, Karla Vanessa Morris Wright, Colin F. Snook, Michael J. Butler
2024 — conf
Semantics Formalisation - Modelling and Proving Strategies Using Event-B Versus Theories.
The Application of Formal Methods
Thai Son Hoang, Colin F. Snook, Karla Vanessa Morris Wright, Laurent Voisin, Michael J. Butler
2023 B conf
A Rigorous Iterative Analysis Approach for Capturing the Safety Requirements of Self-Driving Vehicle Systems.
COMPSAC
Fahad Alotaibi, Thai Son Hoang, Michael J. Butler
2023 J jnl
A fairness-based refinement strategy to transform liveness properties in Event-B models.
Sci. Comput. Program.
Chenyang Zhu, Michael J. Butler, Corina Cîrstea, Thai Son Hoang
2023 — conf
AIC Approach for Intelligent Systems Requirements Elicitation.
ICSRS
Haider Al-Shareefy, Michael J. Butler, Thai Son Hoang
2023 C conf
Designing Critical Systems Using Hierarchical STPA and Event-B.
ABZ
Asieh Salehi Fathabadi, Colin F. Snook, Dana Dghaym, Thai Son Hoang, Fahad Alotaibi, Michael J. Butler
2023 C conf
Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling.
ICTAC
Karla Vanessa Morris Wright, Thai Son Hoang, Colin F. Snook, Michael J. Butler
2023 — conf
Verifiably Safe and Trusted Human-AI Systems: A Socio-technical Perspective.
TAS
Michael Akintunde, Victoria Young, Vahid Yazdanpanah, Asieh Salehi Fathabadi, Pauline Leonard, Michael J. Butler, Luc Moreau
2022 — conf
A lightweight approach to the concurrent use and integration of SysML and formal methods in systems design.
MoDELS (Companion)
Robert Thorburn, Vladimiro Sassone, Asieh Salehi Fathabadi, Leonardo Aniello, Michael J. Butler, Dana Dghaym, Thai Son Hoang
2022 — conf
Building an Extensible Textual Framework for the Rodin Platform.
SEFM Workshops
Thai Son Hoang, Colin F. Snook, Dana Dghaym, Asieh Salehi Fathabadi, Michael J. Butler
2022 — conf
Developing the UML-B Modelling Tools.
SEFM Workshops
Colin F. Snook, Michael J. Butler, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym
2022 J jnl
Formal verification and validation of run-to-completion style state charts using Event-B.
Innov. Syst. Softw. Eng.
Karla Morris, Colin F. Snook, Thai Son Hoang, Geoffrey C. Hulette, Robert C. Armstrong, Michael J. Butler
2022 — conf
Generating SPARK from Event-B, Providing Fundamental Safety and Security.
MEDI Workshops
Asieh Salehi Fathabadi, Dana Dghaym, Thai Son Hoang, Michael J. Butler, Colin F. Snook
2022 B conf
High-Level Rigorous Template for Analysing Safety Properties of Self-driving Vehicle Systems.
COMPSAC
Fahad Alotaibi, Thai Son Hoang, Michael J. Butler
2021 J jnl
Domain-specific scenarios for refinement-based methods.
J. Syst. Archit.
Colin F. Snook, Thai Son Hoang, Dana Dghaym, Asieh Salehi Fathabadi, Michael J. Butler
2021 C conf
Extensible Record Structures in Event-B.
ABZ
Asieh Salehi Fathabadi, Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler
2021 Misc conf
Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions.
TASE
Chenyang Zhu, Michael J. Butler, Corina Cîrstea, Thai Son Hoang
2021 — conf
Refinable Record Structures in Formal Methods.
MEDI Workshops
Asieh Salehi Fathabadi, Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler
2021 C conf
The CamilleX Framework for the Rodin Platform.
ABZ
Thai Son Hoang, Colin F. Snook, Dana Dghaym, Asieh Salehi Fathabadi, Michael J. Butler
2021 C conf
Verifying System-Level Security of a Smart Ballot Box.
ABZ
Dana Dghaym, Thai Son Hoang, Michael J. Butler, Runshan Hu, Leonardo Aniello, Vladimiro Sassone
2020 J jnl
Abstract State Machines, Alloy, B, TLA, VDM and Z (ABZ 2018).
Sci. Comput. Program.
Michael J. Butler, Alexander Raschke
2020 — conf
Formal Verification of Run-to-Completion Style Statecharts Using Event-B.
ECSA Companion
Karla Morris, Colin F. Snook, Thai Son Hoang, Geoffrey C. Hulette, Robert C. Armstrong, Michael J. Butler
2020 J jnl
Formalizing hierarchical scheduling for refinement of real-time systems.
Sci. Comput. Program.
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
2020 J jnl
Introduction to special section on the ABZ 2018 case study: Hybrid ERTMS/ETCS Level 3.
Int. J. Softw. Tools Technol. Transf.
Michael J. Butler, Thai Son Hoang, Alexander Raschke, Klaus Reichl
2020 Misc conf
Real-Time Trigger-Response Properties for Event-B Applied to the Pacemaker.
TASE
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
2020 C conf
Refinement and Verification of Responsive Control Systems.
ABZ
Karla Morris, Colin F. Snook, Thai Son Hoang, Geoffrey C. Hulette, Robert C. Armstrong, Michael J. Butler
2020 C conf
The First Twenty-Five Years of Industrial Use of the B-Method.
FMICS
Michael J. Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, Laurent Voisin
2020 J jnl
Trace semantics and refinement patterns for real-time properties in event-B models.
Sci. Comput. Program.
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
2020 J jnl
Verifying Cross-Layer Interactions Through Formal Model-Based Assertion Generation.
IEEE Embed. Syst. Lett.
Asieh Salehi Fathabadi, Mohammadsadegh Dalvandi, Michael J. Butler, Bashir M. Al-Hashimi
2019 J jnl
A methodology for assuring the safety and security of critical infrastructure based on STPA and Event-B.
Int. J. Crit. Comput. Based Syst.
Giles Howard, Michael J. Butler, John Colley, Vladimiro Sassone
2019 B conf
Behaviour-Driven Formal Model Development of the ETCS Hybrid Level 3.
ICECCS
Michael J. Butler, Dana Dghaym, Thai Son Hoang, Tope Omitola, Colin F. Snook, Andreas Fellner, Rupert Schlick, Thorsten Tarrach, Tomas Fischer, Peter Tummeltshammer
2019 — conf
Domain-Specific Scenarios for Refinement-Based Methods.
MEDI Workshops
Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler
2019 — conf
Making (Implicit) Security Requirements Explicit for Cyber-Physical Systems: A Maritime Use Case Security Analysis.
DEXA Workshops
Tope Omitola, Abdolbaghi Rezazadeh, Michael J. Butler
2019 — conf
SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B.
FM Workshops (1)
Mohammadsadegh Dalvandi, Michael J. Butler, Asieh Salehi Fathabadi
2019 Misc conf
Towards Refinement Semantics of Real-Time Trigger-Response Properties in Event-B.
TASE
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
2018 J jnl
A model-based framework for software portability and verification in embedded power management systems.
J. Syst. Archit.
Asieh Salehi Fathabadi, Michael J. Butler, Sheng Yang, Luis Alfonso Maeda-Nunez, James R. B. Bantock, Bashir M. Al-Hashimi, Geoff V. Merrett
2018 C ed.
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings
ABZ
Michael J. Butler, Alexander Raschke, Thai Son Hoang, Klaus Reichl
2018 C conf
Behaviour-Driven Formal Model Development.
ICFEM
Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler, Tomas Fischer, Rupert Schlick, Keming Wang
2018 J jnl
DeepSaucer: Unified Environment for Verifying Deep Neural Networks.
CoRR
Naoto Sato, Hironobu Kuruma, Masanori Kaneko, Yuichiroh Nakagawa, Hideto Ogawa, Thai Son Hoang, Michael J. Butler
2018 Misc conf
Developing A New Language to Construct Algebraic Hierarchies for Event-B.
SETTA
James Snook, Michael J. Butler, Thai Son Hoang
2018 J jnl
Introduction to the ABZ 2016 Special issue.
Sci. Comput. Program.
Michael J. Butler, Klaus-Dieter Schewe
2018 — conf
Refinement of Statecharts with Run-to-Completion Semantics.
FTSCS
Karla Morris, Colin F. Snook, Thai Son Hoang, Robert C. Armstrong, Michael J. Butler
2018 C conf
Refinement of Timing Constraints for Concurrent Tasks with Scheduling.
ABZ
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
2018 B conf
Reusing Formal Models via Lifting.
ICECCS
Dana Dghaym, Colin F. Snook, Thai Son Hoang, Michael J. Butler
2018 Misc conf
Semantics of Real-Time Trigger-Response Properties in Event-B.
TASE
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
2018 C conf
The Hybrid ERTMS/ETCS Level 3 Case Study.
ABZ
Thai Son Hoang, Michael J. Butler, Klaus Reichl
2018 J jnl
Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset.
Sci. Comput. Program.
Thai Son Hoang, Colin F. Snook, Asieh Salehi Fathabadi, Michael J. Butler, Lukas Ladenberger
2018 C conf
Verifiable Code Generation from Scheduled Event-B Models.
ABZ
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh, Asieh Salehi Fathabadi
2017 B conf
A Composition Mechanism for Refinement-Based Methods.
ICECCS
Thai Son Hoang, Dana Dghaym, Colin F. Snook, Michael J. Butler
2017 — conf
Analysing Security Protocols Using Refinement in iUML-B.
NFM
Colin F. Snook, Thai Son Hoang, Michael J. Butler
2017 C conf
Class-Diagrams for Abstract Data Types.
ICTAC
Thai Son Hoang, Colin F. Snook, Dana Dghaym, Michael J. Butler
2017 J jnl
Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines.
Sci. Comput. Program.
Richard Banach, Michael J. Butler, Shengchao Qin, Huibiao Zhu
2017 J jnl
Derivation of algorithmic control structures in Event-B refinement.
Sci. Comput. Program.
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh
2017 B conf
Extending ERS for Modelling Dynamic Workflows in Event-B.
ICECCS
Dana Dghaym, Michael J. Butler, Asieh Salehi Fathabadi
2017 — conf
Formal Analysis of Safety and Security Requirements of Critical Systems Supported by an Extended STPA Methodology.
EuroS&P Workshops
Giles Howard, Michael J. Butler, John Colley, Vladimiro Sassone
2017 A conf
Formal Development of Policing Functions for Intelligent Systems.
ISSRE
Chris Bogdiukiewicz, Michael J. Butler, Thai Son Hoang, Martin Paxton, James Snook, Xanthippe Waldron, Toby Wilkinson
2017 — conf
Formal Modelling Techniques for Efficient Development of Railway Control Products.
RSSRail
Michael J. Butler, Dana Dghaym, Tomas Fischer, Thai Son Hoang, Klaus Reichl, Colin F. Snook, Peter Tummeltshammer
2017 — conf
Incremental Database Design using UML-B and Event-B.
IMPEX/FM&MDD
Ahmed Al-Brashdi, Michael J. Butler, Abdolbaghi Rezazadeh
2017 J jnl
Theory Plug-in for Rodin 3.x.
CoRR
Thai Son Hoang, Laurent Voisin, A. Salehi, Michael J. Butler, Toby Wilkinson, N. Beauger
2016 C conf
A Graphical Tool for Event Refinement Structures in Event-B.
ABZ
Dana Dghaym, Matheus Garay Trindade, Michael J. Butler, Asieh Salehi Fathabadi
2016 C ed.
Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings
ABZ
Michael J. Butler, Klaus-Dieter Schewe, Atif Mashkoor, Miklós Biró
2016 J jnl
Editorial.
Formal Aspects Comput.
Michael J. Butler
2016 J jnl
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B.
CoRR
Ashish Darbari, Iain Singleton, Michael J. Butler, John Colley
2016 C conf
Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks.
ICFEM
Richard Banach, Michael J. Butler
2016 — ch.
Modelling and Refining Hybrid Systems in Event-B and Rodin.
From Action Systems to Distributed Systems
Michael J. Butler, Jean-Raymond Abrial, Richard Banach
2016 C conf
Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation.
ABZ
Thai Son Hoang, Colin F. Snook, Lukas Ladenberger, Michael J. Butler
2015 J jnl
A method of refinement in UML-B.
Softw. Syst. Model.
Mar Yah Said, Michael J. Butler, Colin F. Snook
2015 J jnl
Building traceable Event-B models from requirements.
Sci. Comput. Program.
Eman H. Alkhammash, Michael J. Butler, Asieh Salehi Fathabadi, Corina Cîrstea
2015 J jnl
Core Hybrid Event-B I: Single Hybrid Event-B machines.
Sci. Comput. Program.
Richard Banach, Michael J. Butler, Shengchao Qin, Nitika Verma, Huibiao Zhu
2015 J jnl
Editorial.
Formal Aspects Comput.
Michael J. Butler, Einar Broch Johnsen, Luigia Petre
2015 J jnl
Editorial.
Formal Aspects Comput.
George Eleftherakis, Michael J. Butler, Mike Hinchey
2015 C ed.
Formal Methods and Software Engineering - 17th International Conference on Formal Engineering Methods, ICFEM 2015, Paris, France, November 3-5, 2015, Proceedings
ICFEM
Michael J. Butler, Sylvain Conchon, Fatiha Zaïdi
2015 — conf
From Event-B Models to Dafny Code Contracts.
FSEN
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh
2015 J jnl
Language and tool support for event refinement structures in Event-B.
Formal Aspects Comput.
Asieh Salehi Fathabadi, Michael J. Butler, Abdolbaghi Rezazadeh
2015 — conf
Towards Automatic Code Generation of Run-Time Power Management for Embedded Systems Using Formal Methods.
MCSoC
Asieh Salehi Fathabadi, Luis Alfonso Maeda-Nunez, Michael J. Butler, Bashir M. Al-Hashimi, Geoff V. Merrett
2015 J jnl
Transforming Event-B Models to Dafny Contracts.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh
2014 — conf
A Systematic Approach to Requirements Driven Test Generation for Safety Critical Systems.
IMBSA
Toby Wilkinson, Michael J. Butler, John Colley
2014 B conf
Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems.
IFM
Asieh Salehi Fathabadi, Colin F. Snook, Michael J. Butler
2014 — conf
Co-simulating event-B and continuous models via FMI.
SummerSim
Vitaly Savicks, Michael J. Butler, John Colley
2014 — conf
Co-simulation Environment for Rodin: Landing Gear Case Study.
ABZ (Case Study)
Vitaly Savicks, Michael J. Butler, John Colley
2014 C conf
Formal Derivation of Distributed MapReduce.
ABZ
Inna Pereverzeva, Michael J. Butler, Asieh Salehi Fathabadi, Linas Laibinis, Elena Troubitsyna
2013 — conf
A Hybrid Event-B Study of Lane Centering.
CSDM
Richard Banach, Michael J. Butler
2013 — conf
A mixed approach to rigorous development of control designs.
CACSD
Manoranjan Satpathy, S. Ramesh, Colin F. Snook, Neeraj Kumar Singh, Michael J. Butler
2013 J jnl
Building Traceable Event-B Models from Requirements.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Eman H. Alkhammash, Asieh Salehi Fathabadi, Michael J. Butler, Corina Cîrstea
2013 C conf
Cruise Control in Hybrid Event-B.
ICTAC
Richard Banach, Michael J. Butler
2013 J jnl
Editorial.
Formal Aspects Comput.
Jonathan P. Bowen, Michael J. Butler, Steve Reeves, Mike Hinchey
2013 J jnl
Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Dana Dghaym, Michael J. Butler, Asieh Salehi Fathabadi
2013 — ch.
Mastering System Analysis and Design through Abstraction and Refinement.
Engineering Dependable Software Systems
Michael J. Butler
2013 — conf
Modelling and Refinement in CODA
Refine@IFM
Michael J. Butler, John Colley, Andrew Edmunds, Colin F. Snook, Neil Evans, Neil Grant, Helen Marshall
2013 — conf
Practical Theory Extension in Event-B.
Theories of Programming and Formal Methods
Michael J. Butler, Issam Maamria
2013 Misc conf
Problem decomposition and sub-model reconciliation of control systems in Event-B.
IRI
Sanaz Yeganefard, Michael J. Butler
2013 J jnl
Reasoned modelling critics: Turning failed proofs into modelling guidance.
Sci. Comput. Program.
Andrew Ireland, Gudmund Grov, Maria Teresa Llano, Michael J. Butler
2013 C conf
Systematic Development of Control Designs via Formal Refinement.
MODELSWARD
Manoranjan Satpathy, Colin F. Snook, Silky Arora, S. Ramesh, Michael J. Butler
2013 — ch.
Tooling.
Industrial Deployment of System Engineering Methods
Michael J. Butler, Laurent Voisin, Thomas Muller
2012 B conf
A Practical Approach for Closed Systems Formal Verification Using Event-B.
SEFM
Brett Bicknell, Jose Reis, Michael J. Butler, John Colley, Colin F. Snook
2012 B conf
A Systematic Approach to Atomicity Decomposition in Event-B.
SEFM
Asieh Salehi Fathabadi, Michael J. Butler, Abdolbaghi Rezazadeh
2012 J jnl
Building on the DEPLOY Legacy: Code Generation and Simulation
CoRR
Andrew Edmunds, Michael J. Butler, John Colley
2012 B conf
Control Systems: Phenomena and Structuring Functional Requirement Documents.
ICECCS
Sanaz Yeganefard, Michael J. Butler
2012 C conf
Event-B Code Generation: Type Extension with Theories.
ABZ
Andrew Edmunds, Michael J. Butler, Issam Maamria, Renato Silva, Chris Lovell
2012 J jnl
External and internal choice with event groups in Event-B.
Formal Aspects Comput.
Michael J. Butler
2012 Misc conf
Formal Modelling for Ada Implementations: Tasking Event-B.
Ada-Europe
Andrew Edmunds, Abdolbaghi Rezazadeh, Michael J. Butler
2011 — conf
Applying Atomicity and Model Decomposition to a Space Craft System in Event-B.
NASA Formal Methods
Asieh Salehi Fathabadi, Abdolbaghi Rezazadeh, Michael J. Butler
2011 A conf
Composing Event-B Specifications - Case-Study Experience.
SC
Ali Gondal, Michael Poppleton, Michael J. Butler
2011 J jnl
Decomposition tool for event-B.
Softw. Pract. Exp.
Renato Silva, Carine Pascal, Thai Son Hoang, Michael J. Butler
2011 B ed.
FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings
FM
Michael J. Butler, Wolfram Schulte
2011 J jnl
Specification and refinement of discrete timing properties in Event-B.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Mohammad Reza Sarshogh, Michael J. Butler
2011 J jnl
Structuring Functional Requirements of Control Systems to Facilitate Refinement-based Formalisation.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Sanaz Yeganefard, Michael J. Butler
2010 — conf
A Basis for Feature-Oriented Modelling in Event-B.
ASM
Jennifer Sorge, Michael Poppleton, Michael J. Butler
2010 — conf
A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.
ASM
Edd Turner, Michael J. Butler, Michael Leuschel
2010 J jnl
Deriving Relationship Between Semantic Models - An Approach for cCSP
CoRR
Shamim Ripon, Michael J. Butler
2010 J jnl
Editorial.
Formal Aspects Comput.
Eerke A. Boiten, Michael J. Butler, John Derrick, Graeme Smith
2010 — conf
Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B.
NASA Formal Methods
Sanaz Yeganefard, Michael J. Butler, Abdolbaghi Rezazadeh
2010 J jnl
Formalizing cCSP Synchronous Semantics in PVS
CoRR
Shamim Ripon, Michael J. Butler
2010 — conf
On an Extensible Rule-Based Prover for Event-B.
ASM
Issam Maamria, Michael J. Butler, Andrew Edmunds, Abdolbaghi Rezazadeh
2010 — conf
Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance.
ASM
Andrew Ireland, Gudmund Grov, Michael J. Butler
2010 — conf
Rewriting and Well-Definedness within a Proof System
PAR
Issam Maamria, Michael J. Butler
2010 — conf
Rewriting and Well-Definedness within a Proof System.
PAR@ITP
Issam Maamria, Michael J. Butler
2010 J jnl
Rodin: an open toolset for modelling and reasoning in Event-B.
Int. J. Softw. Tools Technol. Transf.
Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, Laurent Voisin
2010 — conf
Shared Event Composition/Decomposition in Event-B.
FMCO
Renato Silva, Michael J. Butler
2010 — conf
Verification of UML Models by Translation to UML-B.
FMCO
Colin F. Snook, Vitaly Savicks, Michael J. Butler
2009 — conf
09381 Extended Abstracts Collection - Refinement Based Methods for the Construction of Dependable Systems.
Refinement Based Methods for the Construction of Dependable Systems
Jean-Raymond Abrial, Michael J. Butler, Rajev Joshi, Elena Troubitsyna, J. C. P. Woodcock
2009 — conf
Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B.
SBMF
Kriangsak Damchoom, Michael J. Butler
2009 — conf
Applying Event-B Atomicity Decomposition to a Multi Media Protocol.
FMCO
Asieh Salehi Fathabadi, Michael J. Butler
2009 B conf
Decomposition Structures for Event-B.
IFM
Michael J. Butler
2009 — ch.
Event-B Patterns for Specifying Fault-Tolerance in Multi-agent Interaction.
Methods, Models and Tools for Fault Tolerance
Elisabeth Ball, Michael J. Butler
2009 — ch.
Formal Development of a Total Order Broadcast for Distributed Transactions Using Event-B.
Methods, Models and Tools for Fault Tolerance
Divakar Yadav, Michael J. Butler
2009 B conf
Language and Tool Support for Class and State Machine Refinement in UML-B.
FM
Mar Yah Said, Michael J. Butler, Colin F. Snook
2009 — book
Methods, Models and Tools for Fault Tolerance
Methods, Models and Tools for Fault Tolerance
Michael J. Butler, Cliff B. Jones, Alexander B. Romanovsky, Elena Troubitsyna
2009 — ed.
Refinement Based Methods for the Construction of Dependable Systems, 13.09. - 18.09.2009
Refinement Based Methods for the Construction of Dependable Systems
Jean-Raymond Abrial, Michael J. Butler, Rajev Joshi, Elena Troubitsyna, J. C. P. Woodcock
2009 C conf
Supporting Reuse of Event-B Developments through Generic Instantiation.
ICFEM
Renato Silva, Michael J. Butler
2009 — conf
Validating and Animating Higher-Order Recursive Functions in B.
Rigorous Methods for Software Construction and Analysis
Michael Leuschel, Dominique Cansell, Michael J. Butler
2009 — conf
Verification of Liveness Properties in Distributed Systems.
IC3
Divakar Yadav, Michael J. Butler
2008 C conf
A Roadmap for the Rodin Toolset.
ABZ
Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Laurent Voisin
2008 C ed.
Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings
ABZ
Egon Börger, Michael J. Butler, Jonathan P. Bowen, Paul Boca
2008 J jnl
An incremental development of the Mondex system in Event-B.
Formal Aspects Comput.
Michael J. Butler, Divakar Yadav
2008 — conf
Linking Event-B and Concurrent Object-Oriented Programs.
Refine@FM
Andrew Edmunds, Michael J. Butler
2008 C conf
Modelling and Proof of a Tree-Structured File System in Event-B and Rodin.
ICFEM
Kriangsak Damchoom, Michael J. Butler, Jean-Raymond Abrial
2008 — conf
PVS Embedding of cCSP Semantic Models and Their Relationship.
AVoCS
Shamim Ripon, Michael J. Butler
2008 J jnl
ProB: an automated analysis toolset for the B method.
Int. J. Softw. Tools Technol. Transf.
Michael Leuschel, Michael J. Butler
2008 C conf
UML-B: A Plug-in for the Event-B Tool Set.
ABZ
Colin F. Snook, Michael J. Butler
2007 C conf
Automatic Testing from Formal Specifications.
TAP
Manoranjan Satpathy, Michael J. Butler, Michael Leuschel, S. Ramesh
2007 C ed.
Formal Methods and Software Engineering, 9th International Conference on Formal Engineering Methods, ICFEM 2007, Boca Raton, FL, USA, November 14-15, 2007, Proceedings
ICFEM
Michael J. Butler, Michael G. Hinchey, María M. Larrondo-Petrie
2007 Misc conf
Symmetry Reduced Model Checking for B.
TASE
Edd Turner, Michael Leuschel, Corinna Spermann, Michael J. Butler
2007 — conf
Symmetry Reduction for B by Permutation Flooding.
B
Michael Leuschel, Michael J. Butler, Corinna Spermann, Edd Turner
2006 B conf
A Proposal for Records in Event-B.
FM
Neil Evans, Michael J. Butler
2006 C conf
An Open Extensible Tool Environment for Event-B.
ICFEM
Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Laurent Voisin
2006 J jnl
Guest Editorial Editorial for the FAC Special Issue based on derivative papers from "Refine '05".
Formal Aspects Comput.
Eerke A. Boiten, Michael J. Butler
2006 — conf
Rigorous Design of Fault-Tolerant Transactions for Replicated Database Systems Using Event B.
RODIN Book
Divakar Yadav, Michael J. Butler
2006 — ed.
Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project]
RODIN Book
Michael J. Butler, Cliff B. Jones, Alexander B. Romanovsky, Elena Troubitsyna
2006 B conf
Roadmap for enhanced languages and methods to aid verification.
GPCE
Gary T. Leavens, Jean-Raymond Abrial, Don S. Batory, Michael J. Butler, Alessandro Coglio, Kathi Fisler, Eric C. R. Hehner, Cliff B. Jones, Dale Miller, Simon L. Peyton Jones, Murali Sitaraman, Douglas R. Smith, Aaron Stump
2006 J jnl
UML-B: Formal modeling and design aided by UML.
ACM Trans. Softw. Eng. Methodol.
Colin F. Snook, Michael J. Butler
2005 C conf
Automatic Refinement Checking for B.
ICFEM
Michael Leuschel, Michael J. Butler
2005 B conf
Combining CSP and B for Specification and Property Verification.
FM
Michael J. Butler, Michael Leuschel
2005 B conf
Comparing Two Approaches to Compensable Flow Composition.
CONCUR
Roberto Bruni, Michael J. Butler, Carla Ferreira, C. A. R. Hoare, Hernán C. Melgratti, Ugo Montanari
2005 — conf
Executable Semantics for Compensating CSP.
EPEW/WS-FM
Michael J. Butler, Shamim Ripon
2005 J jnl
Precise Modelling of Compensating Business Transactions and its Application to BPEL.
J. Univers. Comput. Sci.
Michael J. Butler, Carla Ferreira, Muan Yong Ng
2005 — conf
Some Guidelines for Formal Development of Web-Based Applications in B-Method.
ZB
Abdolbaghi Rezazadeh, Michael J. Butler
2005 — conf
Tools for System Validation with B Abstract Machines.
Abstract State Machines
Michael J. Butler, Michael Leuschel, Colin F. Snook
2004 — conf
A Trace Semantics for Long-Running Transactions.
25 Years Communicating Sequential Processes
Michael J. Butler, C. A. R. Hoare, Carla Ferreira
2004 — conf
A Trust Analysis Methodology for Pervasive Computing Systems.
Trusting Agents for Trusting Electronic Societies
Stéphane Lo Presti, Michael J. Butler, Michael Leuschel, Chris Booth
2004 C conf
An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions.
COORDINATION
Michael J. Butler, Carla Ferreira
2004 J jnl
Performance analysis of probabilistic action systems.
Formal Aspects Comput.
Stefan Hallerstede, Michael J. Butler
2004 — conf
ProTest: An Automatic Test Environment for B Specifications.
MBT
Manoranjan Satpathy, Michael Leuschel, Michael J. Butler
2004 — conf
The Use of Formal Methods in the Analysis of Trust (Position Paper).
iTrust
Michael J. Butler, Michael Leuschel, Stéphane Lo Presti, Phillip Turner
2003 — conf
ProB: A Model Checker for B.
FME
Michael Leuschel, Michael J. Butler
2003 B conf
Towards Formalizing UML State Diagrams in CSP.
SEFM
Muan Yong Ng, Michael J. Butler
2003 — conf
Using B Refinement to Analyse Compensating Business Processes.
ZB
Carla Ferreira, Michael J. Butler
2003 — conf
Using SPIN and STeP to Verify Business Processes Specifications.
Ershov Memorial Conference
Juan Carlos Augusto, Michael J. Butler, Carla Ferreira, Stephen-John Craig
2002 J jnl
A System-Based Approach to the Formal Development of Embedded Controllers for a Railway.
Des. Autom. Embed. Syst.
Michael J. Butler
2002 — conf
An Approach to Combining B and Alloy.
ZB
Leonid Mikhailov, Michael J. Butler
2002 J jnl
Extending the concept of transaction compensation.
IBM Syst. J.
Mandy Chessell, Catherine Griffin, David Vines, Michael J. Butler, Carla Ferreira, Peter Henderson
2002 B ed.
Integrated Formal Methods, Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002, Proceedings
IFM
Michael J. Butler, Luigia Petre, Kaisa Sere
2002 J jnl
On the Use of Data Refinement in the Development of Secure Communications Systems.
Formal Aspects Comput.
Michael J. Butler
2002 C conf
Tool Support for Visualizing CSP in UML.
ICFEM
Muan Yong Ng, Michael J. Butler
2001 — conf
Transacted Memory for Smart Cards.
FME
Pieter H. Hartel, Michael J. Butler, Eduard de Jong, Mark Longley
2001 — conf
Using a Graphical Design Tool for Formal Specification.
PPIG
Colin F. Snook, Michael J. Butler
2000 — conf
A Generic Model for Assessing Process Quality.
IWSM
Manoranjan Satpathy, Rachel Harrison, Colin F. Snook, Michael J. Butler
2000 B conf
A Process Compensation Language.
IFM
Michael J. Butler, Carla Ferreira
2000 — conf
Performing Algorithmic Refinement before Data Refinement in B.
ZB
Michael J. Butler, Mairead Meagher
2000 J jnl
csp2B: A Practical Approach to Combining CSP and B.
Formal Aspects Comput.
Michael J. Butler
1999 J jnl
Calculational Derivation of Pointer Algorithms from Tree Operations.
Sci. Comput. Program.
Michael J. Butler
1999 J jnl
Reasoning about Grover's quantum search algorithm using probabilistic
ACM Trans. Program. Lang. Syst.
Michael J. Butler, Pieter H. Hartel
1999 — conf
The Operational Semantics of a Java Secure Processor.
Formal Syntax and Semantics of Java
Pieter H. Hartel, Michael J. Butler, Moshe Levy
1999 — conf
csp2B: A Practical Approach to Combining CSP and B.
World Congress on Formal Methods
Michael J. Butler
1998 J jnl
Fusion and Simultaneous Execution in the Refinement Calculus.
Acta Informatica
Ralph-Johan Back, Michael J. Butler
1997 — conf
An Approach to the Design of Distributed Systems with B AMN.
ZUM
Michael J. Butler
1996 — conf
Program Derivation Using the Refinement Calculator.
TPHOLs
Michael J. Butler, Thomas Långbacka
1996 J jnl
Stepwise Refinement of Communicating Systems.
Sci. Comput. Program.
Michael J. Butler
1995 J jnl
Action Systemes, Unbounded Nondeterminism, and Infinite Traces.
Formal Aspects Comput.
Michael J. Butler, Carroll Morgan
1995 — conf
An Action System Approach to the Steam Boiler Problem.
Formal Methods for Industrial Applications
Michael J. Butler, Emil Sekerinski, Kaisa Sere
1995 B conf
Exploring Summation and Product Operators in the Refinement Calculus.
MPC
Ralph-Johan Back, Michael J. Butler
1993 B conf
Refinement and Decomposition of Value-Passing Action Systems.
CONCUR
Michael J. Butler
1992 — —
A CSP approach to action systems.
Michael J. Butler
1991 — conf
Behavioural Extension for CSP.
VDM Europe (1)
Michael J. Butler
1990 — conf
Service Extension at the Specification Level.
Z User Workshop
Michael J. Butler