Michael J. Butler

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: 323-332

Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, Laurent Voisin: Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6): 447-466 (2010)

Edd Turner, Michael J. Butler, Michael Leuschel: A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. ASM 2010: 231-244

Colin F. Snook, Vitaly Savicks, Michael J. Butler: Verification of UML Models by Translation to UML-B. FMCO 2010: 251-266

Shamim Ripon, Michael J. Butler: Formalizing cCSP Synchronous Semantics in PVS. CoRR abs/1001.3464 (2010)

Shamim Ripon, Michael J. Butler: Deriving Relationship Between Semantic Models - An Approach for cCSP. CoRR abs/1002.3330 (2010)

Michael J. Butler, Cliff B. Jones, Alexander Romanovsky, Elena Troubitsyna (Eds.): Methods, Models and Tools for Fault Tolerance. Lecture Notes in Computer Science 5454, Springer 2009, isbn 978-3-642-00866-5

Shamim Ripon, Michael J. Butler: PVS Embedding of cCSP Semantic Models and Their Relationship. Electr. Notes Theor. Comput. Sci. 250(2): 103-118 (2009)

Michael Leuschel, Dominique Cansell, Michael J. Butler: Validating and Animating Higher-Order Recursive Functions in B. Rigorous Methods for Software Construction and Analysis 2009: 78-92

Mar Yah Said, Michael J. Butler, Colin F. Snook: Language and Tool Support for Class and State Machine Refinement in UML-B. FM 2009: 579-595

Kriangsak Damchoom, Michael J. Butler: Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. SBMF 2009: 134-152

Michael Leuschel, Michael J. Butler: ProB: an automated analysis toolset for the B method. STTT 10(2): 185-203 (2008)

Colin F. Snook, Michael J. Butler: UML-B: A Plug-in for the Event-B Tool Set. ABZ 2008: 344

Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Laurent Voisin: A Roadmap for the Rodin Toolset. ABZ 2008: 347

Kriangsak Damchoom, Michael J. Butler, Jean-Raymond Abrial: Modelling and Proof of a Tree-Structured File System in Event-B and Rodin. ICFEM 2008: 25-44

Egon Börger, Michael J. Butler, Jonathan P. Bowen, Paul Boca (Eds.): Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings. Lecture Notes in Computer Science 5238, Springer 2008, isbn 978-3-540-87602-1

Michael Leuschel, Michael J. Butler, Corinna Spermann, Edd Turner: Symmetry Reduction for B by Permutation Flooding. B 2007: 79-93

Manoranjan Satpathy, Michael J. Butler, Michael Leuschel, S. Ramesh: Automatic Testing from Formal Specifications. TAP 2007: 95-113

Edd Turner, Michael Leuschel, Corinna Spermann, Michael J. Butler: Symmetry Reduced Model Checking for B. TASE 2007: 25-34

Colin F. Snook, Michael J. Butler: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1): 92-122 (2006)

Neil Evans, Michael J. Butler: A Proposal for Records in Event-B. FM 2006: 221-235

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: Roadmap for enhanced languages and methods to aid verification. GPCE 2006: 221-236

Jean-Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Laurent Voisin: An Open Extensible Tool Environment for Event-B. ICFEM 2006: 588-605

Michael J. Butler, Cliff B. Jones, Alexander Romanovsky, Elena Troubitsyna (Eds.): Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project]. Lecture Notes in Computer Science 4157, Springer 2006, isbn 3-540-48265-2

Manoranjan Satpathy, Michael Leuschel, Michael J. Butler: ProTest: An Automatic Test Environment for B Specifications. Electr. Notes Theor. Comput. Sci. 111: 113-136 (2005)

Michael J. Butler, Carla Ferreira, Muan Yong Ng: Precise Modelling of Compensating Business Transactions and its Application to BPEL. J. UCS 11(5): 712-743 (2005)

Michael J. Butler, Michael Leuschel, Colin F. Snook: Tools for System Validation with B Abstract Machines. Abstract State Machines 2005: 57-69

Roberto Bruni, Michael J. Butler, Carla Ferreira, C. A. R. Hoare, Hernán C. Melgratti, Ugo Montanari: Comparing Two Approaches to Compensable Flow Composition. CONCUR 2005: 383-397

Michael J. Butler, Shamim Ripon: Executable Semantics for Compensating CSP. EPEW/WS-FM 2005: 243-256

Michael J. Butler, Michael Leuschel: Combining CSP and B for Specification and Property Verification. FM 2005: 221-236

Michael Leuschel, Michael J. Butler: Automatic Refinement Checking for B. ICFEM 2005: 345-359

Abdolbaghi Rezazadeh, Michael J. Butler: Some Guidelines for Formal Development of Web-Based Applications in B-Method. ZB 2005: 472-492

Stefan Hallerstede, Michael J. Butler: Performance analysis of probabilistic action systems. Formal Asp. Comput. 16(4): 313-331 (2004)

Stéphane Lo Presti, Michael J. Butler, Michael Leuschel, Chris Booth: A Trust Analysis Methodology for Pervasive Computing Systems. Trusting Agents for Trusting Electronic Societies 2004: 129-143

Michael J. Butler, C. A. R. Hoare, Carla Ferreira: A Trace Semantics for Long-Running Transactions. 25 Years Communicating Sequential Processes 2004: 133-150

Michael J. Butler, Carla Ferreira: An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions. COORDINATION 2004: 87-104

Michael J. Butler, Michael Leuschel, Stéphane Lo Presti, Phillip Turner: The Use of Formal Methods in the Analysis of Trust (Position Paper). iTrust 2004: 333-339

Juan Carlos Augusto, Michael J. Butler, Carla Ferreira, Stephen-John Craig: Using SPIN and STeP to Verify Business Processes Specifications. Ershov Memorial Conference 2003: 207-213

Michael Leuschel, Michael J. Butler: ProB: A Model Checker for B. FME 2003: 855-874

Muan Yong Ng, Michael J. Butler: Towards Formalizing UML State Diagrams in CSP. SEFM 2003: 138-

Carla Ferreira, Michael J. Butler: Using B Refinement to Analyse Compensating Business Processes. ZB 2003: 477-496

Michael J. Butler: On the Use of Data Refinement in the Development of Secure Communications Systems. Formal Asp. Comput. 14(1): 2-34 (2002)

Mandy Chessell, Catherine Griffin, David Vines, Michael J. Butler, Carla Ferreira, Peter Henderson: Extending the concept of transaction compensation. IBM Systems Journal 41(4): 743-758 (2002)

Muan Yong Ng, Michael J. Butler: Tool Support for Visualizing CSP in UML. ICFEM 2002: 287-298

Leonid Mikhailov, Michael J. Butler: An Approach to Combining B and Alloy. ZB 2002: 140-161

Michael J. Butler, Luigia Petre, Kaisa Sere (Eds.): Integrated Formal Methods, Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002, Proceedings. Lecture Notes in Computer Science 2335, Springer 2002, isbn 3-540-43703-7

Pieter H. Hartel, Michael J. Butler, Eduard de Jong, Mark Longley: Transacted Memory for Smart Cards. FME 2001: 478-499

Michael J. Butler: csp2B: A Practical Approach to Combining CSP and B. Formal Asp. Comput. 12(3): 182-198 (2000)

Michael J. Butler, Carla Ferreira: A Process Compensation Language. IFM 2000: 61-76

Manoranjan Satpathy, Rachel Harrison, Colin F. Snook, Michael J. Butler: A Generic Model for Assessing Process Quality. IWSM 2000: 94-110

Michael J. Butler, Mairead Meagher: Performing Algorithmic Refinement before Data Refinement in B. ZB 2000: 324-343

Michael J. Butler: Calculational Derivation of Pointer Algorithms from Tree Operations. Sci. Comput. Program. 33(3): 221-260 (1999)

Michael J. Butler, Pieter H. Hartel: Reasoning about Grover's quantum search algorithm using probabilistic wp. ACM Trans. Program. Lang. Syst. 21(3): 417-429 (1999)

Michael J. Butler: csp2B: A Practical Approach to Combining CSP and B. World Congress on Formal Methods 1999: 490-508

Pieter H. Hartel, Michael J. Butler, Moshe Levy: The Operational Semantics of a Java Secure Processor. Formal Syntax and Semantics of Java 1999: 313-352

Ralph-Johan Back, Michael J. Butler: Fusion and Simultaneous Execution in the Refinement Calculus. Acta Inf. 35(11): 921-949 (1998)

Michael J. Butler: An Approach to the Design of Distributed Systems with B AMN. ZUM 1997: 223-241

Michael J. Butler: Stepwise Refinement of Communicating Systems. Sci. Comput. Program. 27(2): 139-173 (1996)

Michael J. Butler, Thomas Långbacka: Program Derivation Using the Refinement Calculator. TPHOLs 1996: 93-108

Michael J. Butler, Carroll Morgan: Action Systemes, Unbounded Nondeterminism, and Infinite Traces. Formal Asp. Comput. 7(1): 37-53 (1995)

Michael J. Butler, Emil Sekerinski, Kaisa Sere: An Action System Approach to the Steam Boiler Problem. Formal Methods for Industrial Applications 1995: 129-148

Ralph-Johan Back, Michael J. Butler: Exploring Summation and Product Operators in the Refinement Calculus. MPC 1995: 128-158

Michael J. Butler: Refinement and Decomposition of Value-Passing Action Systems. CONCUR 1993: 217-232

Michael J. Butler: Behavioural Extension for CSP. VDM Europe (1) 1991: 254-267

Michael J. Butler: Service Extension at the Specification Level. Z User Workshop 1990: 319-333