Michael J. Butler

ORCID

Publication Activity (10 Years)

Years Active: 1990-2024
Publications (10 Years): 66

Top Venues

ABZ

Sci. Comput. Program.

ICECCS

CoRR

University of Oxford, UK (PHD)

Education History

University of Oxford, UK

PHD

Publications

Haider Al-Shareefy, Michael J. Butler, Thai Son Hoang
An AIC-based approach for articulating unpredictable problems in open complex environments. CoRR (2024)
Asieh Salehi Fathabadi, Colin F. Snook, Thai Son Hoang, Robert Thorburn, Michael J. Butler, Leonardo Aniello, Vladimiro Sassone
Designing Exception Handling Using Event-B. ABZ (2024)
Fahad Alotaibi, Thai Son Hoang, Asieh Salehi Fathabadi, Michael J. Butler
Event-B Development of Modelling Human Intervention Request in Self-driving Vehicle Systems. ABZ (2024)
Mehmet Said Nur Yagmahan, Abdolbaghi Rezazadeh, Michael J. Butler
An Event-B Formal Model for Access Control and Resource Management of Serverless Apps. ABZ (2024)
Thai Son Hoang, Laurent Voisin, Karla Vanessa Morris Wright, Colin F. Snook, Michael J. Butler
Semantics Formalisation - From Event-B Contexts to Theories. ABZ (2024)
Michael Akintunde, Victoria Young, Vahid Yazdanpanah, Asieh Salehi Fathabadi, Pauline Leonard, Michael J. Butler, Luc Moreau
Verifiably Safe and Trusted Human-AI Systems: A Socio-technical Perspective. TAS (2023)
Fahad Alotaibi, Thai Son Hoang, Michael J. Butler
A Rigorous Iterative Analysis Approach for Capturing the Safety Requirements of Self-Driving Vehicle Systems. COMPSAC (2023)
Karla Vanessa Morris Wright, Thai Son Hoang, Colin F. Snook, Michael J. Butler
Formal Language Semantics for Triggered Enable Statecharts with a Run-to-Completion Scheduling. ICTAC (2023)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea, Thai Son Hoang
A fairness-based refinement strategy to transform liveness properties in Event-B models. Sci. Comput. Program. 225 (2023)
Asieh Salehi Fathabadi, Colin F. Snook, Dana Dghaym, Thai Son Hoang, Fahad Alotaibi, Michael J. Butler
Designing Critical Systems Using Hierarchical STPA and Event-B. ABZ (2023)
Haider Al-Shareefy, Michael J. Butler, Thai Son Hoang
AIC Approach for Intelligent Systems Requirements Elicitation. ICSRS (2023)
Fahad Alotaibi, Thai Son Hoang, Michael J. Butler
High-Level Rigorous Template for Analysing Safety Properties of Self-driving Vehicle Systems. COMPSAC (2022)
Karla Morris, Colin F. Snook, Thai Son Hoang, Geoffrey C. Hulette, Robert C. Armstrong, Michael J. Butler
Formal verification and validation of run-to-completion style state charts using Event-B. Innov. Syst. Softw. Eng. 18 (4) (2022)
Robert Thorburn, Vladimiro Sassone, Asieh Salehi Fathabadi, Leonardo Aniello, Michael J. Butler, Dana Dghaym, Thai Son Hoang
A lightweight approach to the concurrent use and integration of SysML and formal methods in systems design. MoDELS (Companion) (2022)
Thai Son Hoang, Colin F. Snook, Dana Dghaym, Asieh Salehi Fathabadi, Michael J. Butler
Building an Extensible Textual Framework for the Rodin Platform. SEFM Workshops (2022)
Asieh Salehi Fathabadi, Dana Dghaym, Thai Son Hoang, Michael J. Butler, Colin F. Snook
Generating SPARK from Event-B, Providing Fundamental Safety and Security. MEDI Workshops (2022)
Colin F. Snook, Michael J. Butler, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym
Developing the UML-B Modelling Tools. SEFM Workshops (2022)
Colin F. Snook, Thai Son Hoang, Dana Dghaym, Asieh Salehi Fathabadi, Michael J. Butler
Domain-specific scenarios for refinement-based methods. J. Syst. Archit. 112 (2021)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea, Thai Son Hoang
Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions. TASE (2021)
Dana Dghaym, Thai Son Hoang, Michael J. Butler, Runshan Hu, Leonardo Aniello, Vladimiro Sassone
Verifying System-Level Security of a Smart Ballot Box. ABZ (2021)
Asieh Salehi Fathabadi, Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler
Extensible Record Structures in Event-B. ABZ (2021)
Asieh Salehi Fathabadi, Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler
Refinable Record Structures in Formal Methods. MEDI Workshops (2021)
Thai Son Hoang, Colin F. Snook, Dana Dghaym, Asieh Salehi Fathabadi, Michael J. Butler
The CamilleX Framework for the Rodin Platform. ABZ (2021)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
Real-Time Trigger-Response Properties for Event-B Applied to the Pacemaker. TASE (2020)
Michael J. Butler, Alexander Raschke
Abstract State Machines, Alloy, B, TLA, VDM and Z (ABZ 2018). Sci. Comput. Program. 197 (2020)
Asieh Salehi Fathabadi, Mohammadsadegh Dalvandi, Michael J. Butler, Bashir M. Al-Hashimi
Verifying Cross-Layer Interactions Through Formal Model-Based Assertion Generation. IEEE Embed. Syst. Lett. 12 (3) (2020)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
Formalizing hierarchical scheduling for refinement of real-time systems. Sci. Comput. Program. 189 (2020)
Karla Morris, Colin F. Snook, Thai Son Hoang, Geoffrey C. Hulette, Robert C. Armstrong, Michael J. Butler
Refinement and Verification of Responsive Control Systems. ABZ (2020)
Karla Morris, Colin F. Snook, Thai Son Hoang, Geoffrey C. Hulette, Robert Armstrong, Michael J. Butler
Formal Verification of Run-to-Completion Style Statecharts Using Event-B. ECSA Companion (2020)
Michael J. Butler, Philipp Körner, Sebastian Krings, Thierry Lecomte, Michael Leuschel, Luis-Fernando Mejia, Laurent Voisin
The First Twenty-Five Years of Industrial Use of the B-Method. FMICS (2020)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
Trace semantics and refinement patterns for real-time properties in event-B models. Sci. Comput. Program. 197 (2020)
Michael J. Butler, Thai Son Hoang, Alexander Raschke, Klaus Reichl
Introduction to special section on the ABZ 2018 case study: Hybrid ERTMS/ETCS Level 3. Int. J. Softw. Tools Technol. Transf. 22 (3) (2020)
Michael J. Butler, Dana Dghaym, Thai Son Hoang, Tope Omitola, Colin F. Snook, Andreas Fellner, Rupert Schlick, Thorsten Tarrach, Tomas Fischer, Peter Tummeltshammer
Behaviour-Driven Formal Model Development of the ETCS Hybrid Level 3. ICECCS (2019)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
Towards Refinement Semantics of Real-Time Trigger-Response Properties in Event-B. TASE (2019)
Mohammadsadegh Dalvandi, Michael J. Butler, Asieh Salehi Fathabadi
SEB-CG: Code Generation Tool with Algorithmic Refinement Support for Event-B. FM Workshops (1) (2019)
Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler
Domain-Specific Scenarios for Refinement-Based Methods. MEDI Workshops (2019)
Tope Omitola, Abdolbaghi Rezazadeh, Michael J. Butler
Making (Implicit) Security Requirements Explicit for Cyber-Physical Systems: A Maritime Use Case Security Analysis. DEXA Workshops (2019)
Giles Howard, Michael J. Butler, John Colley, Vladimiro Sassone
A methodology for assuring the safety and security of critical infrastructure based on STPA and Event-B. Int. J. Crit. Comput. Based Syst. 9 (1/2) (2019)
Asieh Salehi Fathabadi, Michael J. Butler, Sheng Yang, Luis Alfonso Maeda-Nunez, James R. B. Bantock, Bashir M. Al-Hashimi, Geoff V. Merrett
A model-based framework for software portability and verification in embedded power management systems. J. Syst. Archit. 82 (2018)
Dana Dghaym, Colin F. Snook, Thai Son Hoang, Michael J. Butler
Reusing Formal Models via Lifting. ICECCS (2018)
Colin F. Snook, Thai Son Hoang, Dana Dghaym, Michael J. Butler, Tomas Fischer, Rupert Schlick, Keming Wang
Behaviour-Driven Formal Model Development. ICFEM (2018)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
Semantics of Real-Time Trigger-Response Properties in Event-B. TASE (2018)
Karla Morris, Colin F. Snook, Thai Son Hoang, Robert Armstrong, Michael J. Butler
Refinement of Statecharts with Run-to-Completion Semantics. FTSCS (2018)
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh, Asieh Salehi Fathabadi
Verifiable Code Generation from Scheduled Event-B Models. ABZ (2018)
Thai Son Hoang, Michael J. Butler, Klaus Reichl
The Hybrid ERTMS/ETCS Level 3 Case Study. ABZ (2018)
James Snook, Michael J. Butler, Thai Son Hoang
Developing A New Language to Construct Algebraic Hierarchies for Event-B. SETTA (2018)
Chenyang Zhu, Michael J. Butler, Corina Cîrstea
Refinement of Timing Constraints for Concurrent Tasks with Scheduling. ABZ (2018)
Thai Son Hoang, Colin F. Snook, Asieh Salehi Fathabadi, Michael J. Butler, Lukas Ladenberger
Validating and verifying the requirements and design of a haemodialysis machine using the Rodin toolset. Sci. Comput. Program. 158 (2018)
Michael J. Butler, Klaus-Dieter Schewe
Introduction to the ABZ 2016 Special issue. Sci. Comput. Program. 158 (2018)
Naoto Sato, Hironobu Kuruma, Masanori Kaneko, Yuichiroh Nakagawa, Hideto Ogawa, Thai Son Hoang, Michael J. Butler
DeepSaucer: Unified Environment for Verifying Deep Neural Networks. CoRR (2018)
Giles Howard, Michael J. Butler, John Colley, Vladimiro Sassone
Formal Analysis of Safety and Security Requirements of Critical Systems Supported by an Extended STPA Methodology. EuroS&P Workshops (2017)
Thai Son Hoang, Colin F. Snook, Dana Dghaym, Michael J. Butler
Class-Diagrams for Abstract Data Types. ICTAC (2017)
Ahmed Al-Brashdi, Michael J. Butler, Abdolbaghi Rezazadeh
Incremental Database Design using UML-B and Event-B. IMPEX/FM&MDD (2017)
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh
Derivation of algorithmic control structures in Event-B refinement. Sci. Comput. Program. 148 (2017)
Dana Dghaym, Michael J. Butler, Asieh Salehi Fathabadi
Extending ERS for Modelling Dynamic Workflows in Event-B. ICECCS (2017)
Richard Banach, Michael J. Butler, Shengchao Qin, Huibiao Zhu
Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines. Sci. Comput. Program. 139 (2017)
Colin F. Snook, Thai Son Hoang, Michael J. Butler
Analysing Security Protocols Using Refinement in iUML-B. NFM (2017)
Michael J. Butler, Dana Dghaym, Tomas Fischer, Thai Son Hoang, Klaus Reichl, Colin F. Snook, Peter Tummeltshammer
Formal Modelling Techniques for Efficient Development of Railway Control Products. RSSRail (2017)
Chris Bogdiukiewicz, Michael J. Butler, Thai Son Hoang, Martin Paxton, James Snook, Xanthippe Waldron, Toby Wilkinson
Formal Development of Policing Functions for Intelligent Systems. ISSRE (2017)
Thai Son Hoang, Dana Dghaym, Colin F. Snook, Michael J. Butler
A Composition Mechanism for Refinement-Based Methods. ICECCS (2017)
Thai Son Hoang, Laurent Voisin, A. Salehi, Michael J. Butler, Toby Wilkinson, N. Beauger
Theory Plug-in for Rodin 3.x. CoRR (2017)
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. ABZ (2016)
Dana Dghaym, Matheus Garay Trindade, Michael J. Butler, Asieh Salehi Fathabadi
A Graphical Tool for Event Refinement Structures in Event-B. ABZ (2016)
Ashish Darbari, Iain Singleton, Michael J. Butler, John Colley
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B. CoRR (2016)
Michael J. Butler
Editorial. Formal Aspects Comput. 28 (2) (2016)
Richard Banach, Michael J. Butler
Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks. ICFEM (2016)
George Eleftherakis, Michael J. Butler, Mike Hinchey
Editorial. Formal Aspects Comput. 27 (3) (2015)
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh
From Event-B Models to Dafny Code Contracts. FSEN (2015)
Eman H. Alkhammash, Michael J. Butler, Asieh Salehi Fathabadi, Corina Cîrstea
Building traceable Event-B models from requirements. Sci. Comput. Program. 111 (2015)
Mohammadsadegh Dalvandi, Michael J. Butler, Abdolbaghi Rezazadeh
Transforming Event-B Models to Dafny Contracts. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 72 (2015)
Richard Banach, Michael J. Butler, Shengchao Qin, Nitika Verma, Huibiao Zhu
Core Hybrid Event-B I: Single Hybrid Event-B machines. Sci. Comput. Program. 105 (2015)
Asieh Salehi Fathabadi, Michael J. Butler, Abdolbaghi Rezazadeh
Language and tool support for event refinement structures in Event-B. Formal Aspects Comput. 27 (3) (2015)
Michael J. Butler, Einar Broch Johnsen, Luigia Petre
Editorial. Formal Aspects Comput. 27 (4) (2015)
Mar Yah Said, Michael J. Butler, Colin F. Snook
A method of refinement in UML-B. Softw. Syst. Model. 14 (4) (2015)
Asieh Salehi Fathabadi, Luis Alfonso Maeda-Nunez, Michael J. Butler, Bashir M. Al-Hashimi, Geoff V. Merrett
Towards Automatic Code Generation of Run-Time Power Management for Embedded Systems Using Formal Methods. MCSoC (2015)
Inna Pereverzeva, Michael J. Butler, Asieh Salehi Fathabadi, Linas Laibinis, Elena Troubitsyna
Formal Derivation of Distributed MapReduce. ABZ (2014)
Vitaly Savicks, Michael J. Butler, John Colley
Co-simulating event-B and continuous models via FMI. SummerSim (2014)
Vitaly Savicks, Michael J. Butler, John Colley
Co-simulation Environment for Rodin: Landing Gear Case Study. ABZ (Case Study) (2014)
Toby Wilkinson, Michael J. Butler, John Colley
A Systematic Approach to Requirements Driven Test Generation for Safety Critical Systems. IMBSA (2014)
Asieh Salehi Fathabadi, Colin F. Snook, Michael J. Butler
Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems. IFM (2014)
Sanaz Yeganefard, Michael J. Butler
Problem decomposition and sub-model reconciliation of control systems in Event-B. IRI (2013)
Michael J. Butler, Issam Maamria
Practical Theory Extension in Event-B. Theories of Programming and Formal Methods (2013)
Manoranjan Satpathy, Colin F. Snook, Silky Arora, S. Ramesh, Michael J. Butler
Systematic Development of Control Designs via Formal Refinement. MODELSWARD (2013)
Andrew Ireland, Gudmund Grov, Maria Teresa Llano, Michael J. Butler
Reasoned modelling critics: Turning failed proofs into modelling guidance. Sci. Comput. Program. 78 (3) (2013)
Jonathan P. Bowen, Michael J. Butler, Steve Reeves, Mike Hinchey
Editorial. Formal Aspects Comput. 25 (3) (2013)
Eman H. Alkhammash, Asieh Salehi Fathabadi, Michael J. Butler, Corina Cîrstea
Building Traceable Event-B Models from Requirements. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013)
Michael J. Butler, John Colley, Andrew Edmunds, Colin F. Snook, Neil Evans, Neil Grant, Helen Marshall
Modelling and Refinement in CODA Refine@IFM (2013)
Richard Banach, Michael J. Butler
Cruise Control in Hybrid Event-B. ICTAC (2013)
Richard Banach, Michael J. Butler
A Hybrid Event-B Study of Lane Centering. CSDM (2013)
Dana Dghaym, Michael J. Butler, Asieh Salehi Fathabadi
Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 66 (2013)
Manoranjan Satpathy, S. Ramesh, Colin F. Snook, Neeraj Kumar Singh, Michael J. Butler
A mixed approach to rigorous development of control designs. CACSD (2013)
Andrew Edmunds, Abdolbaghi Rezazadeh, Michael J. Butler
Formal Modelling for Ada Implementations: Tasking Event-B. Ada-Europe (2012)
Andrew Edmunds, Michael J. Butler, John Colley
Building on the DEPLOY Legacy: Code Generation and Simulation CoRR (2012)
Michael J. Butler
External and internal choice with event groups in Event-B. Formal Aspects Comput. 24 (4-6) (2012)
Andrew Edmunds, Michael J. Butler, Issam Maamria, Renato Silva, Chris Lovell
Event-B Code Generation: Type Extension with Theories. ABZ (2012)
Asieh Salehi Fathabadi, Michael J. Butler, Abdolbaghi Rezazadeh
A Systematic Approach to Atomicity Decomposition in Event-B. SEFM (2012)
Sanaz Yeganefard, Michael J. Butler
Control Systems: Phenomena and Structuring Functional Requirement Documents. ICECCS (2012)
Brett Bicknell, Jose Reis, Michael J. Butler, John Colley, Colin F. Snook
A Practical Approach for Closed Systems Formal Verification Using Event-B. SEFM (2012)
Ali Gondal, Michael Poppleton, Michael J. Butler
Composing Event-B Specifications - Case-Study Experience. SC@TOOLS (2011)
Renato Silva, Carine Pascal, Thai Son Hoang, Michael J. Butler
Decomposition tool for event-B. Softw. Pract. Exp. 41 (2) (2011)

Michael J. Butler.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Michael J. Butler