Michael J. Butler

According to our database1, Michael J. Butler
  • authored at least 132 papers between 1990 and 2017.
  • has a "Dijkstra number"2 of three.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2017
Derivation of algorithmic control structures in Event-B refinement.
Sci. Comput. Program., 2017

Core Hybrid Event-B II: Multiple cooperating Hybrid Event-B machines.
Sci. Comput. Program., 2017

Theory Plug-in for Rodin 3.x.
CoRR, 2017

Formal Modelling Techniques for Efficient Development of Railway Control Products.
Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2017

Analysing Security Protocols Using Refinement in iUML-B.
Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

Formal Development of Policing Functions for Intelligent Systems.
Proceedings of the 28th IEEE International Symposium on Software Reliability Engineering, 2017

Class-Diagrams for Abstract Data Types.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2017, 2017

Formal Analysis of Safety and Security Requirements of Critical Systems Supported by an Extended STPA Methodology.
Proceedings of the 2017 IEEE European Symposium on Security and Privacy Workshops, 2017

2016
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B.
CoRR, 2016

Modelling Hybrid Systems in Event-B and Hybrid Event-B: A Comparison of Water Tanks.
Proceedings of the Formal Methods and Software Engineering, 2016

Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-Simulation.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

A Graphical Tool for Event Refinement Structures in Event-B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2016

Modelling and Refining Hybrid Systems in Event-B and Rodin.
Proceedings of the From Action Systems to Distributed Systems - The Refinement Approach., 2016

2015
A method of refinement in UML-B.
Software and System Modeling, 2015

Core Hybrid Event-B I: Single Hybrid Event-B machines.
Sci. Comput. Program., 2015

Building traceable Event-B models from requirements.
Sci. Comput. Program., 2015

Language and tool support for event refinement structures in Event-B.
Formal Asp. Comput., 2015

Editorial.
Formal Asp. Comput., 2015

Editorial.
Formal Asp. Comput., 2015

Transforming Event-B Models to Dafny Contracts.
ECEASST, 2015

Towards Automatic Code Generation of Run-Time Power Management for Embedded Systems Using Formal Methods.
Proceedings of the IEEE 9th International Symposium on Embedded Multicore/Many-core Systems-on-Chip, 2015

From Event-B Models to Dafny Code Contracts.
Proceedings of the Fundamentals of Software Engineering - 6th International Conference, 2015

2014
Co-simulating event-B and continuous models via FMI.
Proceedings of the 2014 Summer Simulation Multiconference, 2014

A Systematic Approach to Requirements Driven Test Generation for Safety Critical Systems.
Proceedings of the Model-Based Safety and Assessment - 4th International Symposium, 2014

Applying an Integrated Modelling Process to Run-time Management of Many-Core Systems.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Formal Derivation of Distributed MapReduce.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013
Mastering System Analysis and Design through Abstraction and Refinement.
Proceedings of the Engineering Dependable Software Systems, 2013

Reasoned modelling critics: Turning failed proofs into modelling guidance.
Sci. Comput. Program., 2013

Editorial.
Formal Asp. Comput., 2013

Evaluation of Graphical Control Flow Management Approaches for Event-B Modelling.
ECEASST, 2013

Building Traceable Event-B Models from Requirements.
ECEASST, 2013

Modelling and Refinement in CODA
Proceedings of the Proceedings 16th International Refinement Workshop, 2013

Systematic Development of Control Designs via Formal Refinement.
Proceedings of the MODELSWARD 2013 - Proceedings of the 1st International Conference on Model-Driven Engineering and Software Development, Barcelona, Spain, 19, 2013

Problem decomposition and sub-model reconciliation of control systems in Event-B.
Proceedings of the IEEE 14th International Conference on Information Reuse & Integration, 2013

Cruise Control in Hybrid Event-B.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

A Hybrid Event-B Study of Lane Centering.
Proceedings of the Complex Systems Design & Management, 2013

A mixed approach to rigorous development of control designs.
Proceedings of the 2013 IEEE International Symposium on Computer-Aided Control System Design, 2013

Practical Theory Extension in Event-B.
Proceedings of the Theories of Programming and Formal Methods, 2013

Tooling.
Proceedings of the Industrial Deployment of System Engineering Methods, 2013

2012
External and internal choice with event groups in Event-B.
Formal Asp. Comput., 2012

Building on the DEPLOY Legacy: Code Generation and Simulation
CoRR, 2012

A Systematic Approach to Atomicity Decomposition in Event-B.
Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

A Practical Approach for Closed Systems Formal Verification Using Event-B.
Proceedings of the Software Engineering and Formal Methods - 10th International Conference, 2012

Control Systems: Phenomena and Structuring Functional Requirement Documents.
Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012

Event-B Code Generation: Type Extension with Theories.
Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

Formal Modelling for Ada Implementations: Tasking Event-B.
Proceedings of the Reliable Software Technologies - Ada-Europe 2012, 2012

2011
Decomposition tool for event-B.
Softw., Pract. Exper., 2011

Structuring Functional Requirements of Control Systems to Facilitate Refinement-based Formalisation.
ECEASST, 2011

Specification and refinement of discrete timing properties in Event-B.
ECEASST, 2011

Composing Event-B Specifications - Case-Study Experience.
Proceedings of the Software Composition - 10th International Conference, SC 2011, Zurich, 2011

Applying Atomicity and Model Decomposition to a Space Craft System in Event-B.
Proceedings of the NASA Formal Methods, 2011

2010
Rodin: an open toolset for modelling and reasoning in Event-B.
STTT, 2010

Editorial.
Formal Asp. Comput., 2010

Rewriting and Well-Definedness within a Proof System
Proceedings of the Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers, 2010

Deriving Relationship Between Semantic Models - An Approach for cCSP
CoRR, 2010

Formalizing cCSP Synchronous Semantics in PVS
CoRR, 2010

Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B.
Proceedings of the Second NASA Formal Methods Symposium, 2010

Rewriting and Well-Definedness within a Proof System.
Proceedings of the Partiality and Recursion in Interactive Theorem Provers, 2010

Verification of UML Models by Translation to UML-B.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

Shared Event Composition/Decomposition in Event-B.
Proceedings of the Formal Methods for Components and Objects - 9th International Symposium, 2010

A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking.
Proceedings of the Abstract State Machines, 2010

A Basis for Feature-Oriented Modelling in Event-B.
Proceedings of the Abstract State Machines, 2010

On an Extensible Rule-Based Prover for Event-B.
Proceedings of the Abstract State Machines, 2010

Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance.
Proceedings of the Abstract State Machines, 2010

2009
Formal Development of a Total Order Broadcast for Distributed Transactions Using Event-B.
Proceedings of the Methods, 2009

Event-B Patterns for Specifying Fault-Tolerance in Multi-agent Interaction.
Proceedings of the Methods, 2009

PVS Embedding of cCSP Semantic Models and Their Relationship.
Electr. Notes Theor. Comput. Sci., 2009

Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B.
Proceedings of the Formal Methods: Foundations and Applications, 2009

Decomposition Structures for Event-B.
Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

Supporting Reuse of Event-B Developments through Generic Instantiation.
Proceedings of the Formal Methods and Software Engineering, 2009

Verification of Liveness Properties in Distributed Systems.
Proceedings of the Contemporary Computing - Second International Conference, 2009

Applying Event-B Atomicity Decomposition to a Multi Media Protocol.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Language and Tool Support for Class and State Machine Refinement in UML-B.
Proceedings of the FM 2009: Formal Methods, 2009

09381 Extended Abstracts Collection - Refinement Based Methods for the Construction of Dependable Systems.
Proceedings of the Refinement Based Methods for the Construction of Dependable Systems, 13.09., 2009

Validating and Animating Higher-Order Recursive Functions in B.
Proceedings of the Rigorous Methods for Software Construction and Analysis, 2009

2008
ProB: an automated analysis toolset for the B method.
STTT, 2008

An incremental development of the Mondex system in Event-B.
Formal Asp. Comput., 2008

Linking Event-B and Concurrent Object-Oriented Programs.
Electr. Notes Theor. Comput. Sci., 2008

Modelling and Proof of a Tree-Structured File System in Event-B and Rodin.
Proceedings of the Formal Methods and Software Engineering, 2008

UML-B: A Plug-in for the Event-B Tool Set.
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

A Roadmap for the Rodin Toolset.
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007
Symmetry Reduced Model Checking for B.
Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

Automatic Testing from Formal Specifications.
Proceedings of the Tests and Proofs, First International Conference, 2007

Symmetry Reduction for B by Permutation Flooding.
Proceedings of the B 2007: Formal Specification and Development in B, 2007

2006
UML-B: Formal modeling and design aided by UML.
ACM Trans. Softw. Eng. Methodol., 2006

Guest Editorial Editorial for the FAC Special Issue based on derivative papers from "Refine '05".
Formal Asp. Comput., 2006

Rigorous Design of Fault-Tolerant Transactions for Replicated Database Systems Using Event B.
Proceedings of the Rigorous Development of Complex Fault-Tolerant Systems [FP6 IST-511599 RODIN project], 2006

An Open Extensible Tool Environment for Event-B.
Proceedings of the Formal Methods and Software Engineering, 2006

Roadmap for enhanced languages and methods to aid verification.
Proceedings of the Generative Programming and Component Engineering, 2006

A Proposal for Records in Event-B.
Proceedings of the FM 2006: Formal Methods, 2006

2005
Precise Modelling of Compensating Business Transactions and its Application to BPEL.
J. UCS, 2005

ProTest: An Automatic Test Environment for B Specifications.
Electr. Notes Theor. Comput. Sci., 2005

Some Guidelines for Formal Development of Web-Based Applications in B-Method.
Proceedings of the ZB 2005: Formal Specification and Development in Z and B, 2005

Automatic Refinement Checking for B.
Proceedings of the Formal Methods and Software Engineering, 2005

Combining CSP and B for Specification and Property Verification.
Proceedings of the FM 2005: Formal Methods, 2005

Executable Semantics for Compensating CSP.
Proceedings of the Formal Techniques for Computer Systems and Business Processes, 2005

Comparing Two Approaches to Compensable Flow Composition.
Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

Tools for System Validation with B Abstract Machines.
Proceedings of the 12th International Workshop on Abstract State Machines, 2005

2004
Performance analysis of probabilistic action systems.
Formal Asp. Comput., 2004

The Use of Formal Methods in the Analysis of Trust (Position Paper).
Proceedings of the Trust Management, Second International Conference, 2004

An Operational Semantics for StAC, a Language for Modelling Long-Running Business Transactions.
Proceedings of the Coordination Models and Languages, 6th International Conference, 2004

A Trace Semantics for Long-Running Transactions.
Proceedings of the Communicating Sequential Processes: The First 25 Years, 2004

A Trust Analysis Methodology for Pervasive Computing Systems.
Proceedings of the Trusting Agents for Trusting Electronic Societies, 2004

2003
Using B Refinement to Analyse Compensating Business Processes.
Proceedings of the ZB 2003: Formal Specification and Development in Z and B, 2003

Towards Formalizing UML State Diagrams in CSP.
Proceedings of the 1st International Conference on Software Engineering and Formal Methods (SEFM 2003), 2003

ProB: A Model Checker for B.
Proceedings of the FME 2003: Formal Methods, 2003

Using SPIN and STeP to Verify Business Processes Specifications.
Proceedings of the Perspectives of Systems Informatics, 2003

2002
Extending the concept of transaction compensation.
IBM Systems Journal, 2002

On the Use of Data Refinement in the Development of Secure Communications Systems.
Formal Asp. Comput., 2002

A System-Based Approach to the Formal Development of Embedded Controllers for a Railway.
Design Autom. for Emb. Sys., 2002

An Approach to Combining B and Alloy.
Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

Tool Support for Visualizing CSP in UML.
Proceedings of the Formal Methods and Software Engineering, 2002

2001
Transacted Memory for Smart Cards.
Proceedings of the FME 2001: Formal Methods for Increasing Software Productivity, 2001

2000
csp2B: A Practical Approach to Combining CSP and B.
Formal Asp. Comput., 2000

Performing Algorithmic Refinement before Data Refinement in B.
Proceedings of the ZB 2000: Formal Specification and Development in Z and B, First International Conference of B and Z Users, York, UK, August 29, 2000

A Generic Model for Assessing Process Quality.
Proceedings of the New Approaches in Software Measurement, 10th International Workshop, 2000

A Process Compensation Language.
Proceedings of the Integrated Formal Methods, Second International Conference, 2000

1999
Reasoning about Grover's quantum search algorithm using probabilistic wp.
ACM Trans. Program. Lang. Syst., 1999

Calculational Derivation of Pointer Algorithms from Tree Operations.
Sci. Comput. Program., 1999

The Operational Semantics of a Java Secure Processor.
Proceedings of the Formal Syntax and Semantics of Java, 1999

csp2B: A Practical Approach to Combining CSP and B.
Proceedings of the FM'99 - Formal Methods, 1999

1998
Fusion and Simultaneous Execution in the Refinement Calculus.
Acta Inf., 1998

1997
An Approach to the Design of Distributed Systems with B AMN.
Proceedings of the ZUM '97: The Z Formal Specification Notation, 1997

1996
Stepwise Refinement of Communicating Systems.
Sci. Comput. Program., 1996

Program Derivation Using the Refinement Calculator.
Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

1995
Action Systemes, Unbounded Nondeterminism, and Infinite Traces.
Formal Asp. Comput., 1995

Exploring Summation and Product Operators in the Refinement Calculus.
Proceedings of the Mathematics of Program Construction, 1995

An Action System Approach to the Steam Boiler Problem.
Proceedings of the Formal Methods for Industrial Applications, 1995

1993
Refinement and Decomposition of Value-Passing Action Systems.
Proceedings of the CONCUR '93, 1993

1992
A CSP approach to action systems.
PhD thesis, 1992

1991
Behavioural Extension for CSP.
Proceedings of the VDM '91, 1991

1990
Service Extension at the Specification Level.
Proceedings of the Z User Workshop, 1990


  Loading...