Prof. Michael Butler 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 (www.event-b.org). His research work encompasses applications, tools and methodology for formal methods. He has made key theoretical and methodological contributions to the Event-B formal method that enable it to scale to large complex systems. These contributions enable modular analysis in terms of how systems models are structured and analysed as well as methods for development of domain-specific mathematical theories that are reusable across multiple projects. Butler collaborates with engineers in various companies on verification and validation including AWE (safety critical embedded systems), Thales (rail systems), Tekever (autonomous systems) and members of the Aerospace Technology Institute (aerospace software). 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 ABZ 2018, 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 several journals (Formal Aspects of Computing, Critical Computer-Based Systems, Software Tools for Technology Transfer).