Andrew Butterfield

Biography

I entered Trinity College Dublin in October 1979 to study Engineering, becoming scholar in 1981, specialising in Computing, and graduating in 1983, Ist class, with Gold Medal. I then embarked on a PhD in TCD, exploring so-called "Silicon Compilers", software tools that transformed computer programs into hardware implemented. During this time I undertook some teaching at TCD, delivering a course on Digital Electronics to 2nd year Computer Science students. I obtained my PhD in 1990, and left to take up computing consultancy, first with Telecom Phonewatch in 1990, then a startup company, and then with K&M Technologies, advising telecommunication companies about abstract modelling. In Jan 1992 I was appointed to my current position as Lecturer in Computer Science at TCD. My research focus changed, towards the formal mathematical modelling of computing systems, with an emphasis on mathematical proof as the main vehicle for verifying system correctness. I also continued to act for K&M Technologies in a consultant role, thereby becoming an active member of Formal Methods Europe, a role I have continued to this day. My early research into formal methods was with a dialect of the Vienna Development Method (VDM) that had a functional/algebraic focus, with an emphasis on data refinement. This was coupled with an interest in pure lazy functional programming languages and concurrency, leading to research that developed formal models of the external I/O behaviour of functional languages. In a long running collaboration with Jim Woodcock, I started exploring semanitcs of hardware compilation languages, most notably Handel-C. This had true (hardware) parallelism, message-passing (CSP-style), and an event-based choice statement that had a notion of priority. Priority is hard to model and reason about, but we succeeded in developing a range of semantic models for this language. In 2003 while on a research visit to UKC, I developed an interest in Unifying Theories of Programming (UTP), and particularly a language called Circus, itself a fusion of Z and CSP. I started looking at a discrete-time version of Circus, with a view to using it to give a UTP semantics to Handel-C. This lead to a generic theory of "slotted-Circus" based on a very general notion of a time. I got SFI research funds to get PhD students to explore the semantics of priority and probability in this setting. In 2007, it was becoming increasingly clear that the kind of "by-hand" proofs we were doing for our slotted-Circus UTP theory work were pushing the limit of what could be done by hand. After investigating existing tools, I chose to start developing my own prototype theorem prover. Since 2003, I have been involved to some degree with Lero: the Irish Software Research Centre, a SFI Research Centre headquartered in the University of Limerick, with TCD, UCC, UCD, DCU, NUIG, NUIM, and DkIT as academic partners. I have been involved in the PAISEAN project, exploring formal semantics for a software/business process description language, that is being applied by colleagues to clinical pathway modelling. Through Lero I got involved in 2012, 2013 with a European Space Agency funded project (MTOBSE) were we developed a specification and formal model of a Separation-Partitioning O/S Kernel, and exploring the feasibility of proving its code to be correct. A follow-up to this in 2014-2016 was another ESA funded project (FMEIMAKQP) where I provided formal methods expertise to an activity that was preparing a process for certifying the correctness of such kernels. My collaboration with Prof Woodcock, involvement in the Lero PAISEAN project, and experiences with kernel verification issues for ESA, have all been the inspiration for my current research focus: developing a compositional, local, UTP formal semantics for shared-variable concurrency, and the various methodologies for developing trustworthy software in this space.

Research Interest

Algebra; Automata; Computational mathematics, discrete mathematics; Computer Design Models; Computer Hardware; Computer Programming Languages; Computer Software; Computer Theory; CONCURRENCY THEORY; Discrete Mathematics; Finite Mathematics; Formal Methods; Formal Semantics; Foundations and methods; Functional Programming; Hardware Compilation; Logic; Mathematical logic, set theory, combinatorics, semantics; Mathematics of computing; MEDICAL DEVICE SOFTWARE; Philosophy of Mathematics; Program Verification; Refinement Calculus; Set Theory; SOFTWARE CERTIFICATION; Software Engineering; Unifying Theories of Programming