| 2008 |
|---|
| 54 | | Egon Börger,
Michael J. Butler,
Jonathan P. Bowen,
Paul Boca:
Abstract State Machines, B and Z, First International Conference, ABZ 2008, London, UK, September 16-18, 2008. Proceedings
Springer 2008 |
| 53 | EE | Colin F. Snook,
Michael J. Butler:
UML-B: A Plug-in for the Event-B Tool Set.
ABZ 2008: 344 |
| 52 | EE | Jean-Raymond Abrial,
Michael J. Butler,
Stefan Hallerstede,
Laurent Voisin:
A Roadmap for the Rodin Toolset.
ABZ 2008: 347 |
| 51 | EE | 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 |
| 50 | EE | Michael Leuschel,
Michael J. Butler:
ProB: an automated analysis toolset for the B method.
STTT 10(2): 185-203 (2008) |
| 2007 |
|---|
| 49 | EE | Michael Leuschel,
Michael J. Butler,
Corinna Spermann,
Edd Turner:
Symmetry Reduction for B by Permutation Flooding.
B 2007: 79-93 |
| 48 | EE | Manoranjan Satpathy,
Michael J. Butler,
Michael Leuschel,
S. Ramesh:
Automatic Testing from Formal Specifications.
TAP 2007: 95-113 |
| 47 | EE | Edd Turner,
Michael Leuschel,
Corinna Spermann,
Michael J. Butler:
Symmetry Reduced Model Checking for B.
TASE 2007: 25-34 |
| 2006 |
|---|
| 46 | | Michael J. Butler,
Cliff B. Jones,
Alexander Romanovsky,
Elena Troubitsyna:
Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project]
Springer 2006 |
| 45 | EE | Neil Evans,
Michael J. Butler:
A Proposal for Records in Event-B.
FM 2006: 221-235 |
| 44 | EE | 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 |
| 43 | EE | Jean-Raymond Abrial,
Michael J. Butler,
Stefan Hallerstede,
Laurent Voisin:
An Open Extensible Tool Environment for Event-B.
ICFEM 2006: 588-605 |
| 42 | EE | 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) |
| 2005 |
|---|
| 41 | EE | Michael J. Butler,
Michael Leuschel,
Colin F. Snook:
Tools for System Validation with B Abstract Machines.
Abstract State Machines 2005: 57-69 |
| 40 | EE | 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 |
| 39 | EE | Michael J. Butler,
Shamim Ripon:
Executable Semantics for Compensating CSP.
EPEW/WS-FM 2005: 243-256 |
| 38 | EE | Michael J. Butler,
Michael Leuschel:
Combining CSP and B for Specification and Property Verification.
FM 2005: 221-236 |
| 37 | EE | Michael Leuschel,
Michael J. Butler:
Automatic Refinement Checking for B.
ICFEM 2005: 345-359 |
| 36 | EE | Abdolbaghi Rezazadeh,
Michael J. Butler:
Some Guidelines for Formal Development of Web-Based Applications in B-Method.
ZB 2005: 472-492 |
| 35 | EE | Manoranjan Satpathy,
Michael Leuschel,
Michael J. Butler:
ProTest: An Automatic Test Environment for B Specifications.
Electr. Notes Theor. Comput. Sci. 111: 113-136 (2005) |
| 34 | EE | 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) |
| 2004 |
|---|
| 33 | EE | Michael J. Butler,
C. A. R. Hoare,
Carla Ferreira:
A Trace Semantics for Long-Running Transactions.
25 Years Communicating Sequential Processes 2004: 133-150 |
| 32 | EE | Michael J. Butler,
Carla Ferreira:
An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions.
COORDINATION 2004: 87-104 |
| 31 | EE | 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 |
| 30 | EE | 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 |
| 29 | EE | Stefan Hallerstede,
Michael J. Butler:
Performance analysis of probabilistic action systems.
Formal Asp. Comput. 16(4): 313-331 (2004) |
| 2003 |
|---|
| 28 | EE | 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 |
| 27 | EE | Michael Leuschel,
Michael J. Butler:
ProB: A Model Checker for B.
FME 2003: 855-874 |
| 26 | EE | Muan Yong Ng,
Michael J. Butler:
Towards Formalizing UML State Diagrams in CSP.
SEFM 2003: 138- |
| 25 | EE | Carla Ferreira,
Michael J. Butler:
Using B Refinement to Analyse Compensating Business Processes.
ZB 2003: 477-496 |
| 2002 |
|---|
| 24 | | Michael J. Butler,
Luigia Petre,
Kaisa Sere:
Integrated Formal Methods, Third International Conference, IFM 2002, Turku, Finland, May 15-18, 2002, Proceedings
Springer 2002 |
| 23 | EE | Muan Yong Ng,
Michael J. Butler:
Tool Support for Visualizing CSP in UML.
ICFEM 2002: 287-298 |
| 22 | EE | Leonid Mikhailov,
Michael J. Butler:
An Approach to Combining B and Alloy.
ZB 2002: 140-161 |
| 21 | EE | Michael J. Butler:
On the Use of Data Refinement in the Development of Secure Communications Systems.
Formal Asp. Comput. 14(1): 2-34 (2002) |
| 20 | EE | 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) |
| 2001 |
|---|
| 19 | EE | Pieter H. Hartel,
Michael J. Butler,
Eduard de Jong,
Mark Longley:
Transacted Memory for Smart Cards.
FME 2001: 478-499 |
| 2000 |
|---|
| 18 | EE | Michael J. Butler,
Carla Ferreira:
A Process Compensation Language.
IFM 2000: 61-76 |
| 17 | EE | Manoranjan Satpathy,
Rachel Harrison,
Colin F. Snook,
Michael J. Butler:
A Generic Model for Assessing Process Quality.
IWSM 2000: 94-110 |
| 16 | EE | Michael J. Butler,
Mairead Meagher:
Performing Algorithmic Refinement before Data Refinement in B.
ZB 2000: 324-343 |
| 15 | EE | Michael J. Butler:
csp2B: A Practical Approach to Combining CSP and B.
Formal Asp. Comput. 12(3): 182-198 (2000) |
| 1999 |
|---|
| 14 | EE | 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 |
| 13 | EE | Michael J. Butler:
csp2B: A Practical Approach to Combining CSP and B.
World Congress on Formal Methods 1999: 490-508 |
| 12 | EE | 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) |
| 11 | | Michael J. Butler:
Calculational Derivation of Pointer Algorithms from Tree Operations.
Sci. Comput. Program. 33(3): 221-260 (1999) |
| 1998 |
|---|
| 10 | EE | Ralph-Johan Back,
Michael J. Butler:
Fusion and Simultaneous Execution in the Refinement Calculus.
Acta Inf. 35(11): 921-949 (1998) |
| 1997 |
|---|
| 9 | | Michael J. Butler:
An Approach to the Design of Distributed Systems with B AMN.
ZUM 1997: 223-241 |
| 1996 |
|---|
| 8 | | Michael J. Butler,
Thomas Långbacka:
Program Derivation Using the Refinement Calculator.
TPHOLs 1996: 93-108 |
| 7 | | Michael J. Butler:
Stepwise Refinement of Communicating Systems.
Sci. Comput. Program. 27(2): 139-173 (1996) |
| 1995 |
|---|
| 6 | | Michael J. Butler,
Emil Sekerinski,
Kaisa Sere:
An Action System Approach to the Steam Boiler Problem.
Formal Methods for Industrial Applications 1995: 129-148 |
| 5 | | Ralph-Johan Back,
Michael J. Butler:
Exploring Summation and Product Operators in the Refinement Calculus.
MPC 1995: 128-158 |
| 4 | | Michael J. Butler,
Carroll Morgan:
Action Systemes, Unbounded Nondeterminism, and Infinite Traces.
Formal Asp. Comput. 7(1): 37-53 (1995) |
| 1993 |
|---|
| 3 | | Michael J. Butler:
Refinement and Decomposition of Value-Passing Action Systems.
CONCUR 1993: 217-232 |
| 1991 |
|---|
| 2 | | Michael J. Butler:
Behavioural Extension for CSP.
VDM Europe (1) 1991: 254-267 |
| 1990 |
|---|
| 1 | | Michael J. Butler:
Service Extension at the Specification Level.
Z User Workshop 1990: 319-333 |
