Professor Michael J Butler: Publications

2016

Dghaym, Dana, Trindade, Matheus Garay, Butler, Michael and Salehi Fathabadi, Asieh (2016) A graphical tool for event refinement structures in Event-B. In, Abstract State Machines, Alloy, B, TLA, VDM, and Z: Proceedings of the 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Linz, Austria, Springer, 269-274. (doi:10.1007/978-3-319-33600-8_20).

Butler, Michael, Schewe, Klaus-Dieter, Mashkoor, Atif and Biro, Miklos (eds.) (2016) Abstract State Machines, Alloy, B, TLA, VDM, and Z, 5th International Conference, ABZ 2016, Springer (Lecture Notes in Computer Science, 9675).

Butler, Michael, Giannakopoulou, Dimitra and Salaun, Gwen (eds.) (2016) Editorial. [in special issue: 12th Edition of Software Engineering and Formal Methods (SEFM)] Formal Aspects of Computing, 28, 179-180. (doi:10.1007/s00165-016-0368-0).

Butler, Michael (2016) Lectures on Modelling and Verification in Event-B. In, Spring School on Engineering Trustworthy Software Systems 2016, Chongqinq, China,

Butler, Michael and Hoang, Thai Son (eds.) (2016) Proceedings of the 6th Rodin User and Developer Workshop, 2016. , University of Southampton, 36pp.

Hoang, Son, Snook, Colin, Ladenberger, Lukas and Butler, Michael (2016) Validating the Requirements and Design of a Hemodialysis Machine Using iUML-B, BMotion Studio, and Co-simulation. Abstract State Machines, Alloy, B, TLA, VDM, and Z - 5th International Conference, ABZ 2016, Linz, Austria, May 23-27, 2016, Proceedings, 9675, 360-375. (doi:10.1007/978-3-319-33600-8_31).

2015

Butler, Michael, Conchon, Sylvain and Zaïdi, Fatiha (eds.) (2015) 17th International Conference on Formal Engineering Methods, ICFEM 2015, Springer (Lecture Notes in Computer Science, 9407).

Wilkinson, Toby, Butler, Michael, Paxton, Martin and Waldron, Xanthippe (2015) A Formal Approach to Multi-UAV Route Validation. In, Fourth International Workshop on Formal Techniques for Safety-Critical Systems,

Said, Mar Yah, Butler, Michael and Snook, Colin (2015) A Method of Refinement in UML-B. Software and Systems Modeling, 14, (4)

Alkhammash, Eman, Butler, Michael, Fathabadi, Asieh Salehi and Cîrstea, Corina (2015) Building traceable Event-B models from requirements. Science of Computer Programming, 1- 21. (doi:10.1016/j.scico.2015.06.002).

Banach, Richard, Butler, Michael, Qin, Shengchao, Verma, Nitika and Zhu, Huibiao (2015) Core Hybrid Event-B I: Single Hybrid Event-B machines. Science of Computer Programming , 105, (0), 92 - 123.

Eleftherakis, George, Butler, Michael and Hinchey, Mike (2015) Editorial. Formal Asp. Comput., 27, (3), 473.

Dalvandi, Mohammadsadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) From Event-B models to Dafny code contracts. In, 6th IPM International Conference on Fundamentals of Software Engineering (FSEN2015), Tehran, IR, 22 - 24 Apr 2015.

Salehi Fathabadi, Asieh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) Language and tool support for event refinement structures in Event-B. Formal Aspects of Computing, 27, (3), 499-523.

Butler, Michael, Abrial, Jean-Raymond and Banach, Richard (2015) Modelling and Refining Hybrid Systems in Event-B and Rodin. In, From Action System to Distributed Systems: The Refinement Approach. , Taylor & Francis.

Salehi Fathabadi, Asieh, Maeda-Nunez, Luis Alfonso, Butler, Michael, Al-Hashimi, Bashir and Merrett, Geoff (2015) Towards automatic code generation of run-time power management for embedded systems using formal methods. In, 9th International Symposium on Embedded Multicore/Many-core Systems-on-Chip (MCSoC-15), Turin, IT, 23 - 25 Sep 2015. 8pp.

Dalvandi, Mohammadsadegh, Butler, Michael and Rezazadeh, Abdolbaghi (2015) Transforming Event-B models to Dafny contracts. In, 15th International Workshop on Automated Verification of Critical Systems (AVoCS 2015), Edinburgh, GB, 01 - 04 Sep 2015.

2014

Wilkinson, Toby, Butler, Michael and Colley, John (2014) A Systematic Approach to Requirements Driven Test Generation for Safety Critical Systems. In, Model-Based Safety and Assessment - 4th International Symposium, {IMBSA} 2014, Munich, Germany, October 27-29, 2014. Proceedings , 43-56.

Salehi Fathabadi, Asieh, Snook, Colin and Butler, Michael (2014) Applying an integrated modelling process to run-time management of many-core systems. In, 11th International Conference on Integrated Formal Methods (iFM), Bertinoro, IT, 09 - 11 Sep 2014.

Savicks, Vitaly, Butler, Michael and Colley, John (2014) Co-simulating Event-B and continuous models via FMI. In, 2014 Summer Computer Simulation Conference, Monterey, US, 06 - 10 Jul 2014. Society for Modeling & Simulation International ( SCS ).

Savicks, Vitaly, Butler, Michael and Colley, John (2014) Co-simulation environment for Rodin: landing gear case study. In, 4th International ABZ 2014 Conference, Toulouse, FR, 02 - 04 Jun 2014. (doi:10.1007/978-3-319-07512-9_11).

Chaudemar, Jean-Charles , Savicks, Vitaly and Butler, Michael (2014) Co-simulation of Event-B and Ptolemy II Models via FMI. In, Embedded Real-time software and systems (ERTSS 2014)

Pereverzeva, Inna, Butler, Michael, Salehi Fathabadi, Asieh, Laibinis, Linas and Troubitsyna, Elena (2014) Formal derivation of distributed MapReduce. In, 4th International ABZ 2014 Conference, Toulouse, FR, 02 - 06 Jun 2014. 17pp.

Reis, Jose, Bicknell, Brett, Butler, Michael and Colley, John (2014) Innovative Approach for Requirements Verification of Closed Systems. In, Embedded Real-time software and systems (ERTSS 2014)

Butler, Michael and Hallerstede, Stefan (eds.) (2014) Proceedings of the 5th Rodin User and Developer Workshop, 2014, Southampton, GB, University of Southampton, 59pp.

Savicks, Vitaly, Butler, Michael, Colley, John and Bendisposto, Jens (2014) Rodin multi-simulation plug-in. In, 5th Rodin User and Developer Workshop, Toulouse, FR, 02 - 03 Jun 2014.

2013

Colley, John and Butler, Michael (2013) A Formal, Systematic Approach to STPA using Event-B Refinement and Proof. In, 21th Safety Critical System Symposium,

Banach, Richard and Butler, Michael (2013) A Hybrid Event-B Study of Lane Centering. In, Complex Systems Design & Management (CSD&M) 2013

Satpathy, M., Ramesh, S., Snook, Colin, Singh, N.K. and Butler, Michael (2013) A Mixed Approach to Rigorous Development of Control Designs. In, IEEE Multi-Conference on Systems and Control (MSC 2013)

Alkhammash, Eman, Salehi Fathabadi, Asieh, Butler, Michael and Cirstea, Corina (2013) Building Traceable Event-B Models from Requirements. In, Automated Verification of Critical Systems (AVoCS 2013)

Savicks, Vitaly, Butler, Michael, Bendisposto, Jens and Colley, John (2013) Co-simulation of Event-B and Continuous Models in Rodin. In, 4th Rodin User and Developer Workshop

Banach, Richard and Butler, Michael (2013) Cruise Control in Hybrid Event-B. In, International Colloquium on Theoretical Aspects of Computing (ICTAC)

Butler, Michael (2013) Mastering System Analysis and Design through Abstraction and Refinement. In, Engineering Dependable Software Systems. Summer School on Engineering Dependable Software Systems, Marktoberdorf, Germany, 2012 , IOS Press.

Butler, Michael, Colley, John, Edmunds, Andrew, Snook, Colin, Evans, Neil, Grant, Neil and Marshall, Helen (2013) Modelling and Refinement in CODA. In, Refine , 36-51.

Butler, Michael and Maamria, Issam (2013) Practical Theory Extension in Event-B. In, Festschrift Symposium in Honour of He Jifeng on the Occasion of His 70th Birthday

Yeganefard, Sanaz and Butler, Michael (2013) Problem Decomposition and Sub-Model Reconciliation of Control Systems in Event-B. In, IEEE International Workshop on Formal Methods Integration

Butler, Michael, Hallerstede, Stefan and Walden, Marina (eds.) (2013) Proceedings of the 4th Rodin User and Developer Workshop, Turku, FI, Turku Centre for Computer Science, 41pp. (TUCS Publication Series).

Ireland, Andrew, Grov, Gudmund, Llano, Maria Teresa and Butler, Michael (2013) Reasoned modelling critics: turning failed proofs into modelling guidance. [in special issue: Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010] Science of Computer Programming, 78, (3), 293-309. (doi:10.1016/j.scico.2011.03.006).

Satpathy, Manoranjan, Snook, Colin, Arora, Silky, Ramesh, S and Butler, Michael (2013) Systematic Development of Control Designs via Formal Refinement. In, International Conference on Model-Driven Engineering and Software Development

Butler, Michael, Voisin, Laurent and Muller, Thomas (2013) Tooling in DEPLOY. In, Romanovsky, Alexander and Thomas, Martin (eds.) Industrial Deployment of System Engineering Methods. , Springer.

2012

Bicknell, Brett, Reis, Jose, Butler, Michael, Colley, John and Snook, Colin (2012) A Practical Approach for Closed Systems Formal Verification Using Event-B. In, 10th International Conference on Software Engineering and Formal Methods (SEFM 2012) , 323-332.

Salehi Fathabadi, Asieh, Butler, Michael and Rezazadeh, Abdolbaghi (2012) A systematic approach to atomicity decomposition in Event-B. [in special issue: Software Engineering and Formal Methods. 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings] Lecture Notes in Computer Science, 7504, 78-93. (doi:10.1007/978-3-642-33826-7_6).

Edmunds, Andrew, Colley, John and Butler, Michael (2012) Building on the DEPLOY legacy: code generation and simulation. In, DS-Event-B-2012: Workshop on the experience of and advances in developing dependable systems in Event-B

Edmunds, Andrew, Lovell, Chris, Silva, Renato, Maamria, Issam and Butler, Michael (2012) Code generation update. In, Rodin User and Developer Workshop, Fontainebleau, FR, 27 - 29 Feb 2012. 2pp.

Yeganefard, Sanaz and Butler, Michael (2012) Control systems: phenomena and structuring functional requirement documents. In, 17th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2012)., Paris, FR, 18 - 20 Jul 2012. 10pp.

Lovell, Chris, Edmunds, Andy, Silva, Renato, Maamria, Issam and Butler, Michael (2012) Ensuring extensibility within code generation. In, Rodin User and Developer Workshop, Fontainebleau, FR, 27 - 29 Feb 2012.

Butler, Michael, Salehi Fathabadi, Asieh and Silva, Renato (2012) Event-B and Rodin. In, Boulanger, Jean-Louis (eds.) Industrial Use of Formal Methods: Formal Verification. London, GB, Chichester, GB, ISTE; Wiley, 215-245.

Edmunds, Andrew, Butler, Michael, Maamria, Issam, Silva, Renato and Lovell, Chris (2012) Event-B code generation: type extension with theories. In, ABZ 2012, Pisa, IT, 19 - 21 Jun 2012. 4pp.

Butler, Michael (2012) External and internal choice with event groups in Event-B. [in special issue: Celebrating the 60th Birthday of Carroll Morgan] FORMAL ASPECTS OF COMPUTING, 24, (4-6), 555-567. (doi:10.1007/s00165-012-0239-2).

Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2012) Formal modelling for Ada implementations: tasking Event-B. In, Ada-Europe 2012: 17th International Conference on Reliable Software Technologies, Stockholm, SE, 11 - 15 Jun 2012. 14pp.

2011

Salehi Fathabadi, Asieh, Rezazadeh, Abdolbaghi and Butler, Michael (2011) Applying Atomicity and Model Decomposition to a Space Craft System in Event-B. In, THIRD NASA FORMAL METHODS SYMPOSIUM, Pasadena, California, 18 - 20 Apr 2011.

Gondal, Ali, Poppleton, Mike and Butler, Michael (2011) Composing Event-B Specifications - Case-Study Experience. In, 10th International Conference on Software Composition, Zurich , Switzerland, 30 Jun - 01 Jul 2011. Springer, 100-115.

Silva, Renato, Pascal, Carine, Hoang, Thai Son and Butler, Michael (2011) Decomposition Tool for Event-B. Software: Practice and Experience, 41, (2), 199-208.

Butler, Michael and Schulte, Wolfram (2011) FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011, Springer

Edmunds, Andrew, Rezazadeh, Abdolbaghi and Butler, Michael (2011) From Event-B models to code: sensing, actuating, and the environment. At SBMF2011, Sao Paulo, BR, 26 - 28 Sep 2011. 6pp.

Sarshogh, Mohammad Reza and Butler, Michael (2011) Specification and refinement of discrete timing properties in Event-B. In, AVoCS 2011, Newcastle,

Yeganefard, Sanaz and Butler, Michael (2011) Structuring functional requirements of control systems to facilitate refinement-based formalisation. [in special issue: Automated Verification of Critical Systems 2011] Electronic Communications of the EASST, 46

Edmunds, Andrew and Butler, Michael (2011) Tasking Event-B: An Extension to Event-B for Generating Concurrent Code. In, PLACES 2011, Saarbrucken, Germany,

Snook, Colin, Savicks, Vitaly and Butler, Michael (2011) Verification of UML models by translation to UML-B. Lecture Notes in Computer Science, 6957, 251.

2010

Abrial, Jean-Raymond, Butler, Michael, Joshi, Rajev, Troubitsyna, Elena and Woodcock, Jim C. P. (2010) 09381 Extended Abstracts Collection — Refinement Based Methods for the Construction of Dependable Systems, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (Dagstuhl Seminar Proceedings, 09381 09381).

Sorge, Jennifer, Poppleton, Mike and Butler, Michael (2010) A Basis for Feature-Oriented Modelling in Event-B. In, ABZ2010, Orford, Canada, 23 - 25 Feb 2010.

Turner, Edd, Butler, Michael and Leuschel, Michael (2010) A Refinement-Based Correctness Proof of Symmetry Reduced Model Checking. In, ABZ 2010, Orford, Canada,

Salehi Fathabadi, Asieh and Butler, Michael (2010) Applying Event-B Atomicity Decomposition to a Multi Media Protocol. In, FMCO Formal Methods for Components and Objects Springer LNCS, 89-104.

Silva, Renato, Pascal, Carine, Hoang, T. Son and Butler, Michael (2010) Decomposition Tool for Event-B. In, Workshop on Tool Building in Formal Methods - ABZ Conference, Orford, Quebec, Canada,

Yeganefard, Sanaz, Butler, Michael and Rezazadeh, Abdolbaghi (2010) Evaluation of a Guideline by Formal Modelling of Cruise Control System in Event-B. In, Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, Washington DC, 13 - 14 Apr 2010. , 182-191.

Gondal, Ali, Poppleton, Mike, Butler, Michael and Snook, Colin (2010) Feature-Oriented Modelling Using Event-B. In, International Conference on Software Engineering Theory and Practice (SETP-10), Orlando, FL., USA, 12 - 14 Jul 2010.

Maamria, Issam, Butler, Michael, Edmunds, Andrew and Rezazadeh, Abdolbaghi (2010) On an Extensible Rule-based Prover for Event-B. In, ABZ2010, Orford, Canada, 23 - 25 Feb 2010.

Maamria, Issam, Butler, Michael, Edmunds, Andrew and Rezazadeh, Abdolbaghi (2010) On an extensible rule-based prover for event-B. In, Proceedings of ABZ 2010. ABZ2010 , Springer. (Lecture Notes in Computer Science).

Ireland, Andrew, Grov, Gudmund and Butler, Michael (2010) Reasoned Modelling Critics: Turning Failed Proofs into Modelling Guidance. In, ABZ 2010, Orford, Canada,

Maamria, Issam and Butler, Michael (2010) Rewriting and Well-De?nedness within a Proof System. In, Partiality and Recursion in Interactive Theorem Provers PAR-10

Abrial, Jean-Raymond, Butler, Michael, Hallerstede, Stefan, Hoang, Thai Son, Mehta, Farhad and Voisin, Laurent (2010) Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, 12, (6), 447-466. (doi:10.1007/s10009-010-0145-y).

Silva, Renato and Butler, Michael (2010) Shared Event Composition/Decomposition in Event-B. In, FMCO Formal Methods for Components and Objects, Graz, Austria, 29 Nov - 01 Dec 2010.

Edmunds, Andrew and Butler, Michael (2010) Tool Support for Event-B Code Generation. In, WS-TBFM2010

2009

Sorge, Jennifer, Poppleton, Michael and Butler, Michael (2009) A Basis for feature-oriented modelling in Event-B. Pre-print, 14pp.

Savicks, Vitaly, Snook, Colin and Butler, Michael (2009) Animation of UML-B State-machines.

Damchoom, Kriangsak and Butler, Michael (2009) Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. In, SBMF 2009, Gramado, Brazil, 19 - 21 Aug 2009. Springer LNCS, 134-152.

Said, Mar Yah, Butler, Michael and Snook, Colin (2009) Class and State Machine Re?nement in UML-B. In, Integration of Model-based Formal Methods and Tools (workshop at iFM 2009)

Butler, Michael (2009) Decomposition Structures for Event-B. In, Integrated Formal Methods iFM2009, Springer, LNCS 5423 Springer.

Silva, Renato, Pascal, Carine, Hoang, T.S. and Butler, Michael (2009) Decomposition tool for Event-B. Southampton, UK, University of Southampton, 4pp.

Ball, Elisabeth and Butler, Michael (2009) Event-B Patterns for Specifying Fault-Tolerance in Multi-Agent Interaction. In, Methods, Models and Tools for Fault Tolerance LNCS 5454. , Springer.

Pascal, Carine and Silva, Renato (2009) Event-B model decomposition. In, DEPLOY Plenary Technical Workshop 2009 21 - 23 Oct 2009. University of Southampton6pp.

Yadav, Divakar and Butler, Michael (2009) Formal Development of a Total Order Broadcast for Distributed Transactions using Event-B. In, Methods, Models and Tools for Fault Tolerance LNCS 5454. , Springer.

Butler, Michael (2009) Incremental Design of Distributed Systems with Event-B. In, Broy, Manfred, Sitou, Wassiou and Hoare, Tony (eds.) Engineering Methods and Tools for Software Safety and Security - Marktoberdorf Summer School 2008. , IOS Press, 131-160.

Said, Mar Yah, Butler, Michael and Snook, Colin (2009) Language and tool support for class and state machine refinement in UML-B. In, Cavalcanti, A. and Dams, D. (eds.) FM 2009: Formal Methods. FM2009 - 16th International Symposium on Formal Methods Berlin, DE, Heidelberg, DE, Springer, 579-595. (Lecture Notes in Computer Science, LNCS 5850). (doi:10.1007/978-3-642-05089-3_37).

Butler, Michael, Jones, Cliff B, Romanovsky, Alexander and Troubitsyna, Elena (2009) Methods, Models and Tools for Fault Tolerance, Springer (LNCS, 5454).

Colley, John and Butler, Michael (2009) On Proving with Event-B that a Pipelined Processor Model Implements its ISA Specification. In, Dagstuhl Seminar on Refinement Based Methods for the Construction of Dependable Systems, Dagstuhl,

Maamria, Issam, Butler, Michael, Edmunds, Andrew and Rezazadeh, Abdolbaghi (2009) On an Extensible Rule-based Prover for Event-B.

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

Silva, Renato and Butler, Michael (2009) Supporting Reuse Mechanisms for Developments in Event-B: Composition.

Silva, Renato and Butler, Michael (2009) Supporting Reuse of Event-B Developments through Generic Instantiation. In, Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, Brazil, 09 - 12 Dec 2009. Springer.

Silva, Renato and Butler, Michael (2009) Supporting Reuse of Event-B Developments through Generic Instantiation. In, International Conference on Formal Engineering Methods(ICFEM), Rio de Janeiro, Brazil, 07 - 12 Dec 2010.

Silva, Renato and Butler, Michael (2009) Supporting reuse mechanisms for developments in event-b: composition. Southampton, UK, Southampton University, 15pp.

Silva, Renato and Butler, Michael (2009) Supporting reuse of Event-B developments through generic instantiation. In, International Conference on Formal Engineering Methods (ICFEM 09), Rio de Janeiro, Brazil, 09 - 12 Dec 2009. 19pp.

Yadav, Divakar and Butler, Michael (2009) Verification of Liveness Properties in Distributed Systems. In, Second International Conference, IC3 2009, Noida, India, 17 - 19 Aug 2009.

2008

Abrial, Jean-Raymond, Butler, Michael, Hallerstede, Stefan and Voisin, Laurent (2008) A Roadmap for the Rodin Toolset. In, Abstract State Machines, B and Z, First International Conference ABZ 2008 , 347.

Boerger, Egon, Butler, Michael, Bowen, Jonathan and Boca, Paul (2008) ABZ2008 Conference - Short Papers.

Börger, Egon, Butler, Michael, Bowen, Jonathan P. and Boca, Paul (2008) Abstract State Machines, B and Z - First International Conference ABZ 2008, Springer (LNCS, 5238).

Butler, Michael and Yadav, Divakar (2008) An incremental development of the Mondex system in Event-B. Formal Aspects of Computing, 20, (1), 61-77. (doi:10.1007/s00165-007-0061-4).

Edmunds, Andrew and Butler, Michael (2008) Linking Event-B and Concurrent Object-Oriented Programs. In, Refine 2008 - International Refinement Workshop, Turku, finland,

Damchoom, Kriangsak, Butler, Michael and Abrial, Jean-Raymond (2008) Modelling and proof of a Tree-structured File System in Event-B and Rodin. In, ICFEM 2008 Springer, 25-44.

Leuschel, Michael and Butler, Michael (2008) ProB: an automated analysis toolset for the B method. International Journal on Software Tools for Technology Transfer, 10, (2), 185-203. (doi:10.1007/s10009-007-0063-9).

Snook, Colin and Butler, Michael (2008) UML-B and Event-B: an integration of languages and tools. In, The IASTED International Conference on Software Engineering - SE2008, Innsbruck, AT, 12 - 14 Feb 2008.

Snook, Colin and Butler, Michael (2008) UML-B: A plug-in for the Event-B tool set. In, Abstract State Machines, B and Z, First International Conference ABZ 2008 , 347.

2007

Satpathy, Manoranjan, Butler, Michael, Leuschel, Michael and Ramesh, S (2007) Automatic Testing from Formal Specifications. In, International Conference on Tests And Proofs (TAP), ETH Zurich, Switzerland, 12 - 13 Feb 2007.

Ball, Elisabeth and Butler, Michael (2007) Event-B Patterns for Specifying Fault-Tolerance in Multi-Agent Interaction. In, Methods, Models and Tools for Fault Tolerance, Oxford, UK,

Yadav, Divakar and Butler, Michael (2007) Formal Development of Fault Tolerant Transactions for a replicated Database using Ordered Broadcasts. In, Methods, Models and Tools for Fault Tolerance (MeMoT 2007), Oxford, , 33-42.

Butler, Michael, Hinchey, Michael G. and Larrondo-Petrie, María M. (eds.) (2007) Formal Methods and Software Engineering: 9th International Conference on Formal Engineering Methods, ICFEM 2007, Springer (Lecture Notes in Computer Science, 4789).

Yadav, Divakar and Butler, Michael (2007) Formal Specifications and Verification of Message Ordering Properties in a Broadcasting System using Event B.

Butler, Michael, Jones, Cliff, Romanovsky, Alexander and Troubitsyna, Elena (2007) Proceedings of the Workshop on Methods, Models and Tools for Fault Tolerance (MeMToFT 2007).

Rezazadeh, Abdolbaghi , Evans, Neil and Butler, Michael (2007) Redevelopment of an Industrial Case Study Using Event-B and Rodin. In, BCS-FACS Christmas 2007 Meeting - Formal Methods In Industry, London,

Turner, Edd, Leuschel, Michael, Spermann, Corinna and Butler, Michael (2007) Symmetry Reduced Model Checking for B. In, First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE '07), ECNU, Shanghai, China, 06 - 08 Jun 2007. IEEE Computer Society, 25-34.

Leuschel, Michael, Butler, Michael, Spermann, Corinna and Turner, Edd (2007) Symmetry Reduction for B by Permutation Flooding. In, 7th International B Conference, Besancon. , France, Springer.

Butler, Michael and Hallerstede, Stefan (2007) The Rodin Formal Modelling Tool. BCS-FACS Christmas 2007 Meeting - Formal Methods In Industry, London.

Leuschel, Michael, Cansell, Dominique and Butler, Michael (2007) Validating and Animating Higher-Order Recursive Functions in B. In, Festschrift for Egon Börger

2006

Evans, Neil and Butler, Michael (2006) A Proposal for Records in Event-B. In, Formal Methods 2006, McMaster, Canada, Springer, 221-235.

Abrial, Jean-Raymond, Butler, Michael, Hallerstede, Stefan and Voisin, Laurent (2006) An open extensible tool environment for Event-B. In, ICFEM 2006, Macau, Springer.

Lo Presti, Stéphane, Butler, Michael, Leuschel, Michael and Booth, Chris (2006) Holistic Trust Design of E-Services. In, Song, Ronggong (eds.) Trust in E-services: Technologies, Practices and Challenges. , .

Evans, Neil and Butler, Michael (2006) Incremental Construction of Large Specifications: Case Study and Techniques.

Butler, Michael (2006) On the Verified-by-Construction Approach. FACS FACTS

Ripon, Shamim and Butler, Michael (2006) Relating Semantic Models of Compensating CSP.

Yadav, Divakar and Butler, Michael (2006) Rigorous Design of Fault-Tolerant Transactions for Replicated Database Systems using Event B. In, Rigorous Development of Complex Fault-Tolerant Systems. , Lecture Notes in Computer Science, Springer , 2006, 343-363.

Butler, Michael, Jones, Cliff B., Romanovsky, Alexander and Troubitsyna, Elena (2006) Rigorous Development of Complex Fault-Tolerant Systems, Springer (Lecture Notes in Computer Science, 4157).

Leavens, Gary T., Abrial, Jean-Raymond, Batory, Don, Butler, Michael, Coglio, Alessandro, Fisler, Kathi, Hehner, Eric, Jones, Cliff B., Miller, Dale, Peyton-Jones, Simon, Sitaraman, Murali, Smith, Douglas R. and Stump, Aaron (2006) Roadmap for Enhanced Languages and Methods to Aid Verification. In, Generative Programming and Component Engineering, 5th International, Portland, Oregon, 22 - 26 Oct 2006. ACM.

Leuschel, Michael, Butler, Michael, Spermann, Corinna and Turner, Edd (2006) Symmetry Reduction for B by Permutation Flooding. In, B2007, Besancon, France,

Turner, Edd and Butler, Michael (2006) Symmetry Reduction in the ProB Model Checker. In, FM2006 Doctoral Symposium, McMaster University, Canada, 21 - 27 Aug 2006. Springer Verlag.

Snook, Colin and Butler, Michael (2006) UML-B: Formal modelling and design aided by UML. ACM Transactions on Software Engineering and Methodology, 15, (1), 92-122.

Ball, Elisabeth and Butler, Michael (2006) Using Decomposition to Model Multi-agent Interaction Protocols in Event-B. In, FM'06 Doctoral Symposium, McMaster University, Hamilton, Canada, Springer.

2005

Lo Presti, S, Butler, M, Leuschel, M and Booth, C (2005) A Trust Analysis Methodology for Pervasive Computing Systems. In, Falcone, R, Barber, S, Sabater, J and Singh, M (eds.) Trusting Agents for trusting Electronic Societies, LNCS Volume 3577. , Springer.

Butler, Michael, Hoare, C.A.R. and Ferreira, Carla (2005) A trace semantics for long-running transactions. In, 25 Years of CSP, London, Springer, 133-150.

Yadav, Divakar and Butler, Michael (2005) Application of Event B to Global Causal Ordering for Fault Tolerant Transactions. In, Workshop on Rigorous Engineering of Fault Tolerant Systems (REFT2005), Newcastle upon Tyne, 18 - 22 Jul 2005. , 93-102.

Leuschel, Michael and Butler, Michael (2005) Automatic Refinement Checking for B. In, ICFEM'05 Springer-Verlag.

Butler, Michael and Leuschel, Michael (2005) Combining CSP and B for Specification and Property Verification. In, Formal Methods 2005, Newcastle upon Tyne, 18 - 22 Jul 2005. Springer, 221-236.

Bruni, Roberto, Butler, Michael, Ferreira, Carla, Hoare, Tony, Melgratti, Hernan and Montanari, Ugo (2005) Comparing two approaches to compensable flow composition. In, CONCUR 2005, San Francisco, 23 - 26 Aug 2005.

Butler, Michael and Ripon, Shamim (2005) Executable Semantics for Compensating CSP. In, 2nd International Workshop on Web Services and Formal Methods, Versailles, Springer, 243- 256.

Lo Presti, Stephane and Butler, Michael (2005) Literature Survey on Trust.

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

Satpathy, Manoranjan, Leuschel, Michael and Butler, Michael, Gurevich, Yuri, Petrenko, Alexander K. and Kossatchev, Alexander (eds.) (2005) ProTest: An Automatic Test Environment for B Specifications. Electronic Notes in Theoretical Computer Science, 111, 113-136.

Butler, Michael, Jones, Cliff, Romanovsky, Alexander and Troubitsyna, Elena (2005) Proceedings of the Workshop on Rigorous Engineering of Fault-Tolerant Systems (REFT 2005). , University of Newcastle upon Tyne, School of Computing Science (Technical Report Series, CS-TR-).

Rezazadeh, Abdolbaghi and Butler, Michael (2005) Some Guidelines for Formal Development of Web-based Applications in B-Method. In, 4th International Conference of B and Z Users (ZB 2005), 13-15 April 2005,

Butler, Michael, Leuschel, Michael and Snook, Colin (2005) Tools for system validation with B abstract machines. In, ASM 2005: 12th International Workshop on Abstract State Machines, Paris,

Snook, Colin, Poppleton, Michael and Johnson, Ian (2005) Towards a methodology for rigorous development of generic requirements patterns. In, Workshop on Rigorous Engineering of Fault Tolerant Systems, Newcastle, UK, , 17-27.

2004

Butler, Michael and Ferreira, Carla (2004) An Operational Semantics for StAC, a Language for Modelling Long-running Business Transactions. In, Coordination 2004, Pisa, Springer.

Lo Presti, Stephane, Butler, Michael, Leuschel, Michael, Snook, Colin and Turner, Phillip (2004) Formal Modelling and Verification of Trust in a Pervasive Application.

Hallerstede, Stefan and Butler, Michael (2004) Performance Analysis of Probabilistic Action Systems. Formal Aspects of Computing, 16, (4), 313-331.

Snook, Colin, Butler, Michael, Edmunds, Andy and Johnson, Ian (2004) Rigorous development of reusable, domain-specific components, for complex applications. In, 3rd International Workshop on Critical Systems Development with UML, Lisbon, Technische Universitat Munchen, 115-129.

Snook, Colin, Butler, Michael and Oliver, Ian (2004) The UML-B Profile for formal systems modelling in UML. In, Mermet, J. (eds.) UML-B Specification for Proven Embedded Systems Design. , Springer.

Butler, Michael, Leuschel, Michael, Lo Presti, Stephane and Turner, Phillip (2004) The Use of Formal Methods in the Analysis of Trust (Position Paper). In, Second International Conference on Trust Management (iTrust 2004), Oxford, UK, 01 Mar - 29 Apr 2004. Springer, 333-339.

Snook, Colin and Butler, Michael (2004) U2B - A tool for translating UML-B models into B. In, Mermet, J. (eds.) UML-B Specification for Proven Embedded Systems Design. , Springer.

2003

Rezazadeh, Abdolbaghi and Butler, Michael (2003) Event-Based Modelling and Refinement of Distributed Monitoring and Control Systems. In, Refinement of Critical Systems (RCS'03)

Leuschel, Michael and Butler, Michael (2003) ProB: A Model Checker for B. Formal Methods Europe 2003, Pisa, Italy, Springer-Verlag, LNCS, 855-874.

Butler, Michael, Leuschel, Michael, Lo Presti, Stephane, Allsopp, David, Beautement, Patrick, Booth, Chris, Cusack, Mark and Kirton, Mike (2003) Towards a Trust Analysis Framework for Pervasive Computing Scenarios.

Ng, Muan Yong and Butler, Michael (2003) Towards formalizing UML State Diagrams in CSP. 1st IEEE International Conference on Software Engineering and Formal Methods, Brisbane, Australia, 25 - 26 Sep 2003. IEEE Computer Society, 138-147.

Butler, Michael and Ferreira, Carla (2003) Using B Refinement to Analyse Compensating Business Processes. In, ZB 2003: Third International Conference of B and Z Users, Turku, Springer.

Augusto, Juan, Butler, Michael, Ferreira, Carla and Craig, Stephen (2003) Using SPIN and STeP to Verify StAC Specifications. In, 5th International A.P.Ershov Conference on Perspectives of System Informatics, Novosibirsk, Russia,

Augusto, Juan Carlos, Leuschel, Michael, Butler, Michael and Ferreira, Carla (2003) Using the Extensible Model Checker XTL to Verify StAC Business Specifications. In, 3rd Workshop on Automated Verification of Critical Systems (AVoCS 2003), Southampton, 02 - 03 Apr 2003. , 253-266.

2002

Butler, Michael (2002) A System-based Approach to the Formal Development of Embedded Controllers for a Railway. Design Automation for Embedded Systems, 6, 355-366.

Mikhailov, Leonid and Butler, Michael (2002) An Approach to Combining B and Alloy. In, ZB'2002

Butler, Michael and Falampin, Jerome (2002) An Approach to Modelling and Refining Timing Properties in B. In, Refinement of Critical Systems (RCS)

Mikhailova, Anna, Doche, Marielle and Butler, Michael (2002) Contracts for Scenario-Based Testing of Object-Oriented Programs.

Butler, Michael, Ferreira, Carla, Henderson, Peter, Chessell, Mandy, Griffin, Catherine and Vines, David (2002) Extending the Concept of Transaction Compensation. IBM Systems Journal, 47, 743-758.

Butler, M. J. (2002) On the Use of Data Refinement in the Development of Secure Communications Systems. Formal Aspects of Computing, 14, (1), 2-34.

Ng, Muan Yong and Butler, Michael (2002) Tool Support for Visualizing CSP in UML. International Conference on Formal Engineering Methods(ICFEM), Shanghai, China, 21 - 25 Oct 2002. Springer Verlag, 287-298.

2001

Satpathy, Manoranjan, Harrison, Rachel, Snook, Colin and Butler, Michael (2001) A Comparative Study of Formal and Informal Specifications through an Industrial Case Study. In, IEEE/ IFIP Workshop on Formal Specification of Computer Based Systems (FSCBS'01)

Satpathy, Manoranjan, Harrison, Rachel, Snook, Colin and Butler, Michael (2001) A Generic Model for Assessing Process Quality. In, International Workshop on Software Measurement (IWSM2000) Springer.

Leuschel, Michael, Adhianto, Laksono, Butler, Michael, Ferreira, Carla and Mikhailov, Leonid (2001) Animation and Model Checking of CSP and B using Prolog Technology. In, Proceedings of the ACM Sigplan Workshop on Verification and Computational Logic VCL'2001 , 97-109.

Mikhailov, Leonid and Butler, Michael (2001) Combining B and Alloy. In, Formal Methods for Industrial Critical Systems

Butler, Michael, Hartel, Pieter, Jong, Eduard de and Longley, Mark (2001) Transacted Memory for Smart Cards. In, FME 2001, Formal Methods for Increasing Software Productivity Springer-Verlag, 478-99.

Snook, C. and Butler, M. J. (2001) Using a Graphical Design Tool for Formal Specification. In, Proceedings 13th Annual Workshop of the Psychology of Programming Interest Group

2000

Butler, Michael and Ferreira, Carla (2000) A Process Compensation Language. In, Integrated Formal Methods IFM2000 Springer, 61.

Butler, M. J. and Meagher, M. M. R. (2000) Performing Algorithmic Refinement before Data Refinement in B. In, Proc. ZB2000: Formal Specification and Development in Z and B Springer, 324-343.

DeRoure, David, Moreau, Luc, Butler, Michael, Chown, Tim and Hartel, Pieter (2000) Study of Security in Multi-Agent Architectures. , Department of Electronics and Computer Science, University of Southampton

Snook, Colin and Butler, Michael (2000) Verifying Dynamic Properties of UML Models by Translation to the B Language and Toolkit. In, UML 2000 Workshop, Dynamic Behaviour in UML Models: Semantic Questions

Butler, M. J. (2000) csp2B: A Practical Approach to Combining CSP and B. Formal Aspects of Computing, 12, 182-196.

1999

Butler, M. J. (1999) Calculational Derivation of Pointer Algorithms from Tree Operations. Science of Computer Programming, 33, (3), 221-260.

Butler, M. J. (1999) Distributed Electronic Mail System. Program Development by Refinement - Case Studies Using the B Method, Springer FACIT Series Springer-Verlag, Berlin, 301-322.

Butler, M. J. and Waldén, M. (1999) Parallel Programming with the B Method. Program Development by Refinement - Case Studies Using the B Method, Springer FACIT Series Springer-Verlag, Berlin, 183-195.

Hartel, P., Butler, M., Currie, A., Henderson, P., Leuschel, M., Martin, A., Smith, A., Ultes-Nitsche, U. and Walters, R.J. (1999) Questions and Answers About Ten Formal Methods. In, Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems STAR/CNR, Pisa, Italy, 179-203.

Butler, M. J. and Hartel, P. H. (1999) Reasoning about Grover's Quantum Search Algorithm using Probabilistic wp. ACM Transactions on Programming Languages and Systems, 21, (3), 417-430.

Hallerstede, S. and Butler, M. J. (1999) Refinement of Dynamic Systems. , University of Southampton

Hartel, P. H., Butler, M. J. and Levy, M. (1999) The Operational Semantics of a Java Secure Processor. In, Alves-Foss, J. (eds.) Formal Syntax and Semantics of Java, LNCS 1523. , Springer-Verlag, 313-52.

Butler, M. J. (1999) csp2B: A Practical Approach to Combining CSP and B. Proc. FM'99: World Congress on Formal Methods Springer-Verlag, 490-508.

1998

Butler, M. J. (1998) Event Ordering in Action Systems. In, Proc. Int. Refinement Workshop / Formal Methods Pacific'98, Springer Series in Discrete Mathematics and Theoretical Computer Science Springer-Verlag, Berlin, 61-80.

Back, R. J. R. and Butler, M. J. (1998) Fusion and Simultaneous Execution in the Refinement Calculus. Acta Informatica, 35, (11), 921-949.

Butler, M. J. (1998) Using Refinement to Analyse the Safety of an Authentication Protocol.

1997

Butler, M. J. (1997) Action System Analysis of an Authentication Protocol (extended abstract). Proc. Conf. Formal Methods Pacific'97, Springer Series in Discrete Mathematics and Theoretical Computer Science Springer-Verlag, Berlin, 287-288.

Butler, M. J. (1997) An Approach to the Design of Distributed Systems with B AMN. In, Proc. 10th Int. Conf. of Z Users: The Z Formal Specification Notation (ZUM), LNCS 1212 Springer-Verlag, Berlin, 223-241.

Butler, Michael, Hartel, Pieter, Jong, Eduard de and Longley, Mark (1997) Applying Formal Methods to the Design of Smart Card Software.

Butler, M. J. (1997) Review of Abrial, J.-R. The B-Book. The Computer J., 40, (1), 59-61.

Butler, M. J., Grundy, J., Långbacka, T., Ruksenas, R. and Wright, J. von (1997) The Refinement Calculator: Proof Support for Program Refinement. In, Proc. Conf. Formal Methods Pacific'97, Springer Series in Discrete Mathematics and Theoretical Computer Science Springer-Verlag, Berlin, 40-61.

1996

Butler, M. J., Sekerinski, E. and Sere, K. (1996) An Action System Approach to the Steam Boiler Problem. In, Formal Methods for Industrial Applications -- Specifying and Programming the Steam Boiler Control, LNCS 1165 Springer-Verlag, Berlin, 129-148.

Butler, M. J. (1996) An Approach to the Design of Distributed Systems with B AMN (extended version).

Butler, M. J. (1996) Calculational Derivation of Algorithms on Tree-based Pointer Structures. In, BCS-FACS Refinement Workshop Springer-Verlag Electronic Workshops in Computing.

Butler, M. J. and Waldén, M. (1996) Distributed System Development in B. In, Proc. First B Conf. IRIN (Institut de Recherche en Informatique de Nantes), 155-168.

Butler, M. J. and Långbacka, T. (1996) Program Derivation using the Refinement Calculator. In, Proc. 9th Int. Conf. on Theorem Proving in Higher Order Logics (TPHOLs'96), LNCS 1125 Springer-Verlag, Berlin, 93-108.

Butler, M. J. (1996) Stepwise Refinement of Communicating Systems. Science of Computer Programming, 27, (2), 139-173.

1995

Butler, M.J. and Morgan, C.C. (1995) Action Systems, Unbounded Nondeterminism, and Infinite Traces. Formal Aspects of Computing, 7, 37-53.

Back, R.J.R. and Butler, M.J. (1995) Exploring Summation and Product Operators in the Refinement Calculus. In, Mathematics of Program Construction Springer-Verlag.

1994

Butler, M.J. and Back, R.J.R. (1994) Applications of Summation and Product Operators in the Refinement Calculus. 6th Nordic Workshop on Programming Theory

Butler, M.J., Hedman, E., Nilson, P., Ruksenas, R., Waldén, M. and Zhao, Y. (1994) Specification of a Program Derivation Editor. (Reports in Mathematics and Computer Science A94-15).

1993

Butler, Michael and McDonnell, Eoin (1993) Experiment D: Application of Z to IN-Services Test Case.

Butler, M.J. (1993) Feature Interaction Analysis Using Z.

Butler, M.J. (1993) Refinement and Decomposition of Value-Passing Action Systemss in the Refinement Calculus. CONCUR'93 Springer-Verlag.

Butler, Michael and Airchinnigh, Micheal Mac an (1993) Service Specification Using Z.

1992

Butler, M.J. (1992) A CSP Approach to Action Systems. Oxford University, Computing Laboratory, Doctoral Thesis .

1991

Butler, M.J. (1991) Behavioural Extension for CSP Processes. VDM '91 Springer-Verlag.

1990

Butler, M.J. (1990) Service Extension at the Specification Level. Z User Meeting Springer-Verlag.

1989

Butler, M.J. (1989) Formal Techniques Applied to the X.400 Reliable Transfer Service. Programming Research Group, Oxford University Masters Thesis .