Prof. Michael Butler

Prof. Michael Butler  leads the Electronics and Software Systems Group. He is internationally recognised for research on formal software engineering methods for complex systems. He leads the development of the Rodin toolset; a formal method framework for system-level modelling and analysis ( His research work encompasses applications, tools and methodology for formal methods. He plays a leading role in the development of several tools for B and Event-B especially the Rodin toolset and the ProB model checker.  In the ADVANCE FP7 project (, Butler plays the role of scientific coordinator ensuring the Rodin tool development is coordinated across multiple sites and is properly aligned with the needs of the ADVANCE industrial partners. His work on model decomposition for Event-B is now being implemented and used in Rodin. He was worked on a number of significant formal developments in Event-B including an electronic funds system and a flash-based file system. Butler collaborates with engineers in AWE (safety critical embedded systems), Alstom (rail systems), Critical Software (smart grids) and Systerel (embedded systems). In the PRiME Project, Butler leads the development of run-time energy and reliability management methods, verification and software engineering.    Butler serves on the PCs of many international conferences.  He is Co-Chair of ICFEM 2014, a leading international conference on formal methods.  He is a Fellow of the British Computer Society, is Chair of IFIP WG 2.3 Programming Methodology and is on the Editorial Board of the Formal Aspects of Computing journal.