Virtual participation: Zoom details available here
Speaker: Dr Andrew Butterfield, Trinity College Dublin
Title: "Unifying Theories of Programming: bringing order to the Formal Methods Tower of Babel"
Abstract: Formal Methods is a discipline of Computer Science that looks at using mathematical reasoning techniques to verify the correctness of solutions to computing problems. This involves developing mathematical semantics for both implementation and specification languages, and finding a formal bridge to link both. As far back as 1966, Peter Landin published a paper called 'The next 700 programming languages', and formal techniques have since proliferated in number to match. In 1998 Tony Hoare and He Jifeng published 'Unifying Theories of Programming' (UTP), detailing one way of achieving some degree of unification, based on the use of classical predicate logic. This seminar gives an overview of results in this area, with digressions into the topic of formal-methods vs. testing, the importance of tools (and verifying same), and experiences working with a real-time operating system used for space mission. Along the way it addresses the following questions: Why is concurrent programming so hard? It is; Why is logic so hard? It shouldn't be.
Biography: Andrew started his research career in looking at ways to transform hardware designs in a correctness-preserving way to result in more efficient chip layout (PhD 1990). He then switched into formal methods and functional programming languages research. In the 90s he banded together with other formal methods researchers in Ireland to form the Irish Formal Methods Special Interest Group. In addition to regular meetings, it also ran an annual Irish Formal Methods Workshop that attracted submissions and visitors from abroad. In 2003 he started working on UTP, becoming an active member of that community, which continues to this day. His recent research has been funded by the European Space Agency, looking at using formal verification techniques for operating system software. This culminated in getting formal methods techniques into the eco-system of RTEMS, an open-source real time operating system used in many ESA missions. In addition to publishing conference and journal papers, he has served on program committees, organised conferences, special journal editions, and is currently an Associate Editor for the ACM journal Formal Aspects of Computing.