Search the dblp DataBase
Michael J. Butler :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Stéphane Lo Presti , Michael J. Butler , Michael Leuschel , Chris Booth A Trust Analysis Methodology for Pervasive Computing Systems. [Citation Graph (0, 0)][DBLP ] Trusting Agents for Trusting Electronic Societies, 2004, pp:129-143 [Conf ] Michael Leuschel , Michael Butler , Corinna Spermann , Edd Turner Symmetry Reduction for B by Permutation Flooding. [Citation Graph (0, 0)][DBLP ] B, 2007, pp:79-93 [Conf ] Michael J. Butler , C. A. R. Hoare , Carla Ferreira A Trace Semantics for Long-Running Transactions. [Citation Graph (0, 0)][DBLP ] 25 Years Communicating Sequential Processes, 2004, pp:133-150 [Conf ] Roberto Bruni , Michael J. Butler , Carla Ferreira , C. A. R. Hoare , Hernán C. Melgratti , Ugo Montanari Comparing Two Approaches to Compensable Flow Composition. [Citation Graph (0, 0)][DBLP ] CONCUR, 2005, pp:383-397 [Conf ] Michael J. Butler Refinement and Decomposition of Value-Passing Action Systems. [Citation Graph (0, 0)][DBLP ] CONCUR, 1993, pp:217-232 [Conf ] Michael J. Butler , Carla Ferreira An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions. [Citation Graph (0, 0)][DBLP ] COORDINATION, 2004, pp:87-104 [Conf ] Michael J. Butler , Emil Sekerinski , Kaisa Sere An Action System Approach to the Steam Boiler Problem. [Citation Graph (0, 0)][DBLP ] Formal Methods for Industrial Applications, 1995, pp:129-148 [Conf ] Michael Butler , Shamim Ripon Executable Semantics for Compensating CSP. [Citation Graph (0, 0)][DBLP ] EPEW/WS-FM, 2005, pp:243-256 [Conf ] Juan Carlos Augusto , Michael J. Butler , Carla Ferreira , Stephen-John Craig Using SPIN and STeP to Verify Business Processes Specifications. [Citation Graph (0, 0)][DBLP ] Ershov Memorial Conference, 2003, pp:207-213 [Conf ] Michael J. Butler Behavioural Extension for CSP. [Citation Graph (0, 0)][DBLP ] VDM Europe (1), 1991, pp:254-267 [Conf ] Michael J. Butler csp2B: A Practical Approach to Combining CSP and B. [Citation Graph (0, 0)][DBLP ] World Congress on Formal Methods, 1999, pp:490-508 [Conf ] Michael J. Butler , Michael Leuschel Combining CSP and B for Specification and Property Verification. [Citation Graph (0, 0)][DBLP ] FM, 2005, pp:221-236 [Conf ] Neil Evans , Michael Butler A Proposal for Records in Event-B. [Citation Graph (0, 0)][DBLP ] FM, 2006, pp:221-235 [Conf ] Pieter H. Hartel , Michael J. Butler , Eduard de Jong , Mark Longley Transacted Memory for Smart Cards. [Citation Graph (0, 0)][DBLP ] FME, 2001, pp:478-499 [Conf ] Michael Leuschel , Michael J. Butler ProB: A Model Checker for B. [Citation Graph (0, 0)][DBLP ] FME, 2003, pp:855-874 [Conf ] Gary T. Leavens , Jean-Raymond Abrial , Don S. Batory , Michael 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. [Citation Graph (0, 0)][DBLP ] GPCE, 2006, pp:221-236 [Conf ] Jean-Raymond Abrial , Michael Butler , Stefan Hallerstede , Laurent Voisin An Open Extensible Tool Environment for Event-B. [Citation Graph (0, 0)][DBLP ] ICFEM, 2006, pp:588-605 [Conf ] Muan Yong Ng , Michael J. Butler Tool Support for Visualizing CSP in UML. [Citation Graph (0, 0)][DBLP ] ICFEM, 2002, pp:287-298 [Conf ] Michael Leuschel , Michael J. Butler Automatic Refinement Checking for B. [Citation Graph (0, 0)][DBLP ] ICFEM, 2005, pp:345-359 [Conf ] Michael J. Butler , Carla Ferreira A Process Compensation Language. [Citation Graph (0, 0)][DBLP ] IFM, 2000, pp:61-76 [Conf ] Michael J. Butler , Michael Leuschel , Stéphane Lo Presti , Phillip Turner The Use of Formal Methods in the Analysis of Trust (Position Paper). [Citation Graph (0, 0)][DBLP ] iTrust, 2004, pp:333-339 [Conf ] Manoranjan Satpathy , Rachel Harrison , Colin F. Snook , Michael J. Butler A Generic Model for Assessing Process Quality. [Citation Graph (0, 0)][DBLP ] IWSM, 2000, pp:94-110 [Conf ] Pieter H. Hartel , Michael J. Butler , Moshe Levy The Operational Semantics of a Java Secure Processor. [Citation Graph (0, 0)][DBLP ] Formal Syntax and Semantics of Java, 1999, pp:313-352 [Conf ] Ralph-Johan Back , Michael J. Butler Exploring Summation and Product Operators in the Refinement Calculus. [Citation Graph (0, 0)][DBLP ] MPC, 1995, pp:128-158 [Conf ] Muan Yong Ng , Michael J. Butler Towards Formalizing UML State Diagrams in CSP. [Citation Graph (0, 0)][DBLP ] SEFM, 2003, pp:138-0 [Conf ] Michael J. Butler , Thomas Långbacka Program Derivation Using the Refinement Calculator. [Citation Graph (0, 0)][DBLP ] TPHOLs, 1996, pp:93-108 [Conf ] Michael J. Butler An Approach to the Design of Distributed Systems with B AMN. [Citation Graph (0, 0)][DBLP ] ZUM, 1997, pp:223-241 [Conf ] Michael J. Butler , Mairead Meagher Performing Algorithmic Refinement before Data Refinement in B. [Citation Graph (0, 0)][DBLP ] ZB, 2000, pp:324-343 [Conf ] Carla Ferreira , Michael J. Butler Using B Refinement to Analyse Compensating Business Processes. [Citation Graph (0, 0)][DBLP ] ZB, 2003, pp:477-496 [Conf ] Michael J. Butler Service Extension at the Specification Level. [Citation Graph (0, 0)][DBLP ] Z User Workshop, 1990, pp:319-333 [Conf ] Leonid Mikhailov , Michael J. Butler An Approach to Combining B and Alloy. [Citation Graph (0, 0)][DBLP ] ZB, 2002, pp:140-161 [Conf ] Abdolbaghi Rezazadeh , Michael J. Butler Some Guidelines for Formal Development of Web-Based Applications in B-Method. [Citation Graph (0, 0)][DBLP ] ZB, 2005, pp:472-492 [Conf ] Ralph-Johan Back , Michael J. Butler Fusion and Simultaneous Execution in the Refinement Calculus. [Citation Graph (0, 0)][DBLP ] Acta Inf., 1998, v:35, n:11, pp:921-949 [Journal ] Manoranjan Satpathy , Michael Leuschel , Michael J. Butler ProTest: An Automatic Test Environment for B Specifications. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2005, v:111, n:, pp:113-136 [Journal ] Michael J. Butler csp2B: A Practical Approach to Combining CSP and B. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 2000, v:12, n:3, pp:182-198 [Journal ] Michael J. Butler On the Use of Data Refinement in the Development of Secure Communications Systems. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 2002, v:14, n:1, pp:2-34 [Journal ] Michael J. Butler , Carroll Morgan Action Systemes, Unbounded Nondeterminism, and Infinite Traces. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 1995, v:7, n:1, pp:37-53 [Journal ] Stefan Hallerstede , Michael J. Butler Performance analysis of probabilistic action systems. [Citation Graph (0, 0)][DBLP ] Formal Asp. Comput., 2004, v:16, n:4, pp:313-331 [Journal ] Mandy Chessell , Catherine Griffin , David Vines , Michael J. Butler , Carla Ferreira , Peter Henderson Extending the concept of transaction compensation. [Citation Graph (0, 0)][DBLP ] IBM Systems Journal, 2002, v:41, n:4, pp:743-758 [Journal ] Michael J. Butler , Carla Ferreira , Muan Yong Ng Precise Modelling of Compensating Business Transactions and its Application to BPEL. [Citation Graph (0, 0)][DBLP ] J. UCS, 2005, v:11, n:5, pp:712-743 [Journal ] Michael J. Butler Stepwise Refinement of Communicating Systems. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 1996, v:27, n:2, pp:139-173 [Journal ] Michael J. Butler Calculational Derivation of Pointer Algorithms from Tree Operations. [Citation Graph (0, 0)][DBLP ] Sci. Comput. Program., 1999, v:33, n:3, pp:221-260 [Journal ] Michael J. Butler , Pieter H. Hartel Reasoning about Grover's quantum search algorithm using probabilistic wp . [Citation Graph (0, 0)][DBLP ] ACM Trans. Program. Lang. Syst., 1999, v:21, n:3, pp:417-429 [Journal ] Michael Butler , Michael Leuschel , Colin Snook Tools for System Validation with B Abstract Machines. [Citation Graph (0, 0)][DBLP ] Abstract State Machines, 2005, pp:57-69 [Conf ] Edd Turner , Michael Leuschel , Corinna Spermann , Michael Butler Symmetry Reduced Model Checking for B. [Citation Graph (0, 0)][DBLP ] TASE, 2007, pp:25-34 [Conf ] Manoranjan Satpathy , Michael Butler , Michael Leuschel , S. Ramesh Automatic Testing from Formal Specifications. [Citation Graph (0, 0)][DBLP ] TAP, 2007, pp:95-113 [Conf ] UML-B: A Plug-in for the Event-B Tool Set. [Citation Graph (, )][DBLP ] A Roadmap for the Rodin Toolset. [Citation Graph (, )][DBLP ] A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. [Citation Graph (, )][DBLP ] Validating and Animating Higher-Order Recursive Functions in B. [Citation Graph (, )][DBLP ] Language and Tool Support for Class and State Machine Refinement in UML-B. [Citation Graph (, )][DBLP ] Modelling and Proof of a Tree-Structured File System in Event-B and Rodin. [Citation Graph (, )][DBLP ] Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. [Citation Graph (, )][DBLP ] Formalizing cCSP Synchronous Semantics in PVS [Citation Graph (, )][DBLP ] Deriving Relationship Between Semantic Models - An Approach for cCSP [Citation Graph (, )][DBLP ] PVS Embedding of cCSP Semantic Models and Their Relationship. [Citation Graph (, )][DBLP ] Search in 0.006secs, Finished in 0.008secs