Skip to main content

Trinity College Dublin, The University of Dublin

Menu Search


Trinity College Dublin By using this website you consent to the use of cookies in accordance with the Trinity cookie policy. For more information on cookies see our cookie policy.

      
Profile Photo

Dr. Andrew Butterfield

Assistant Professor (Computer Science)
OREILLY INSTITUTE

 Andrew.Butterfield@tcd.ie

 3531896 2517


Biography

I entered Trinity College Dublin in October 1979 to study Engineering, then continuing to do a PhD in TCD, exploring software tools that transform computer programs into hardware implementations. During this time I taught a course on Digital Electronics to 2nd year Computer Science students. After a period of self-employed consultancy, 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 semantics of hardware compilation languages, most notably Handel-C. This had an event-based choice statement that had a notion of priority. Priority is hard to model ,but we succeeded in solving this problem 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. This led to my most recent project (RTEMS Space Profile) which involves myself and a research fellow applying formal methods to verify critical parts of a recent multi-core upgrade of RTEMS (Real-Time Executive for Multiprocessor Systems). This is open-source software and the results of our research are in the process of being added into their repository. The results are also supporting postgraduate projects to extend our results.

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 long-term 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 Tags

  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

Research Projects

 RTEMS-SMP Qualification
 FMEIMAKQP - Formal Methods Expert for IMA Kernel Qualification Preparation
 Methods and Tools for OnBoard Software Engineering
 PAISEAN: formal aspects
 Formalising the Interface between Software and Hardware (FISH)

Page 1 of 2

Representations

Details Date
Editorial Board, ACM Journal, Formal Aspects of Computing https://dl.acm.org/journal/fac/editorial-board Highlight - acting as representative of the Editorial Board looking after a special issue with guest editors (https://dl.acm.org/doi/pdf/10.1007/s00165-018-0463-5) 2015 - present
Editorial Board, Formal Aspects of Computing Journal. Feb 2015
Program Committee Chair: 2nd Irish Workshop in Formal Methods 1998
PhD External Examiner, University of York, William Barnett 2022
PhD External Examiner, University of Oxford, Michael Smith 2009
PhD External Examiner, Dublin City University, Benjamin Aziz 2003
Program Committee Chair: 3rd Irish Workshop in Formal Methods 1999
Program Committee Chair: 5th Irish Workshop in Formal Methods 2001
Program Committee co-Chair: FMICS2004 - Ninth International Workshop on Formal Methods for Industrial Critical Systems Sep 2004
Program Committee co-Chair, IFL 2005 17th International Workshop on Implementation and Application of Functional Languages, Dublin Sep 2005
Program Committee co-Chair, IFL 2006 18th International Workshop on Implementation and Application of Functional Languages, Budapest
Program Committee Chair, UTP'08, 2nd International Symposium on Unifying Theories of Programming, Dublin Sep 2008
Programme Committee co-Chair: FM2016-DS : Doctoral Symposium 2016
Program Committee: 1st Irish Workshop in Formal Methods 1997
Program Committee: NFMW97 Northern Formal Methods Workshop, Ilkely Sep 1997
Program Committee: NFMW98 Northern Formal Methods Workshop, Ilkely Sep 1998
Program Committee: FM99 - World Congress on Formal Methods in the Development of Computing Systems, Toulouse Sep 1999
Program Committee: 4th Irish Workshop in Formal Methods 2000
Program Committee: 1st Conference on Mathematical Foundations of Computer Science and Information Technology 2000
Program Committee: 2nd Conference on Mathematical Foundations of Computer Science and Information Technology 2002
Program Committee: 6th International Workshop in Formal Methods 2003
Program Committee: FMICS2003 - Eighth International Workshop on Formal Methods for Industrial Critical Systems 2003
Program Committee: 3rd Conference on Mathematical Foundations of Computer Science and Information Technology 2004
Program Committee: IFL 2004 16th International Workshop on Implementation and Application of Functional Languages, Lubeck Sep 2004
FMICS2005 - Tenth International Workshop on Formal Methods for Industrial Critical Systems 2005
Program Committee: Trends in Functional Programming 2005
Program Committee: 4th Conference on Mathematical Foundations of Computer Science and Information Technology 2006
External Examiner: M.Sc. in Software Engineering, Dublin City University, 2005-2011 Sep 2005-Aug 2011
Program Committee member, ICFEM10, 12th International Conference on Formal Engineering Methods, Shanghai Nov 2010
Program Committee member, UTP10, 3rd International Symposium on Unifying Theories of Programming, Shanghai Nov 2010
Program Committee: ICFEM 2011 13th International Conference on Formal Engineering Methods 25-28/10/2011
Program Committee member, ICTAC10 7th International Colloquium on Theoretical Aspects of Computing, Natal, Brazil Sep 2010
Program Committee member, ICFEM09 11th International Conference on Formal Engineering Methods, Rio de Janeiro Dec 2009
Program Committee member, TFM2009, 2nd Int. FME Conference on Teaching Formal Methods, Eindhoven Nov 2009
Program Committee member, IFL 2009 21st International Workshop on Implementation and Application of Functional Languages, South Orange NJ Sep 2009
Program Committee member, SBMF 2009, Brazilian Symposium on Formal Methods, Gramado Aug 2009
Program Committee member, TFP08 The Ninth Symposium on Trends in Functional Programming, Nijmegen May 2008
Program Committee member, ICTAC'07 The 4th International Colloquium on Theoretical Aspects of Computing, Macau SAR Sep 2007
Program Committee member, ICTAC11 8th International Colloquium on Theoretical Aspects of Computing, Johannesburg, South Africa, 2011 31st Aug 2011
Programme Committee Member, FM 2011: 17TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS, Limerick. June 2011
Program Committee: Refine11 - BCS-FACS Refinement Workshop 2011 2011-06-20
Program Committee: SBMF2011 - Brazilian Symposium on Formal Methods 26-30/9/2011
Program committee: UTP 2012 - 4th International Symposium on Unifying Theories of Programming Aug 2012
Program committee: SBMF 2012 15th Brazilian Symposium on Formal Methods Sep 2012
Program committee: FM 2012 - 18th International Symposium on Formal Methods Aug 2012
Program committee: IFL2012 - 24th International Symposium on the Implementation and Application of Functional Languages Aug-Sep 2012
Programme Committee - FM2014, 19th International Conference on Formal Methods May 12-16th 2014
Program Committee member, ICFEM13 15th International Conference on Formal Engineering Methods, Auckland, NZ Oct/Nov 2013
National STEM Internship Working Group 2013-14
Programme Committee: IEEE International Workshop on Formal Methods Integration (FMi 2013) 2013
Programme Committee: 5th International Symposium on Unifying Theories of Programming (UTP-2014) 2014
Programme Committee: IEEE International Workshop on Formal Methods Integration (FMi 2015) 2015
Program Committee: FM2015, 20th International Conference on Formal Methods 2015
Program Committee: TASE2016 - 10th International Symposium on Theoretical Aspects of Software Engineering 2016
Program Committee: 6th International Symposium on Unifying Theories of Programming (UTP2016) 2016
Programme Committee - FM2016, 21st International Conference on Formal Methods 2016
Program Committee: TASE2017 - 11th International Symposium on Theoretical Aspects of Software Engineering 13th Sep 2017
Programme Committee FM2018-DS : Doctoral Symposium July 14th 2018
Program Committee: TASE2019 - 13th International Symposium on Theoretical Aspects of Software Engineering 29th July 2019
Program Committee: 7th International Symposium on Unifying Theories of Programming (UTP2019) 8th October 2019
ABZ 2020: 7th International Conference on Rigorous State Based Methods postponed
ABZ 2021: 8th International Conference on Rigorous State Based Methods 9th june 2021

Languages

Language Skill Reading Skill Writing Skill Speaking
English Fluent Fluent Fluent
French Medium Basic Basic

Memberships

Membership of Professional Institutions, Associations, Societies

Details Date From Date To
Editorial Board, Journal of Formal Aspects of Computing, ACM 2015 present
IFIP Technical Committee, Working Group 1.9/2.15 Software Verification, invited as observer April 2016 October 2016
Founder member of the Irish Formal Methods Special Interest Group (IFMSIG) 1993 now inactive
Committee Member, Formal Methods Europe (FME) 1994 present
Andrew Butterfield, Towards an Algebra for Unifying Theories of Concurrent Programming (UTCP), LNCS, The Application of Formal Methods, University of York, UK, 4th September 2024, edited by Simon Foster and Augusto Sampaio , 14900, Springer Nature, 2024, pp203 - 232, Conference Paper, PUBLISHED  DOI
Andrew Butterfield, Donnchadh Griffin-Carroll, Deploying Promela/Spin-based Test Generation on RTEMS: Progress and Prospects, DASIA (Data Systems In Aerospace), Opatija, Croatia, May 28th-30th 2024, ASD-Eurospace, 2024, pp3 , Notes: [https://eurospace.org/dasia-conference-aspx/], Conference Paper, PUBLISHED  URL
Andrew Butterfield and Frédéric Tuong, Applying Formal Verification to an Open-Source Real-Time Operating System, Theories of Programming and Formal Methods, Shanghai, China, 15/09/2023, edited by Jonathan P. Bowen, Qin Li, Qiwen Xu. , LNCS 14080, Springer Nature Switzerland, 2023, pp348 - 366, Conference Paper, PUBLISHED  TARA - Full Text  DOI
Andrew Butterfield, Deploying Promela/Spin-based test generation on RTEMS: A progress report, DASIA (Data Systems in Eurospace), Sitges, Spain, June 6-8th 2023, ASD Eurospace, 2023, pp6 , Notes: [see https://eurospace.org/dasia-conference-aspx/], Conference Paper, PUBLISHED  TARA - Full Text  URL
Andrew Butterfield, 'Formal Verification', RTEMS Software Engineering, master, https://docs.rtems.org/branches/master/eng/index.html, RTEMS.org, 2023, -, Protocol or guideline, PUBLISHED  URL
Gerard Ekembe Ngondi, Vasileios Koutavas, Andrew Butterfield, From CCS to CSP: the m-among-n Synchronisation Approach, Electronic Proceedings in Theoretical Computer Science, Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, Warsaw, Poland, 12th September 2022, edited by Valentina Castiglioni, Claudio Antares. , Open Publishing Association, 2022, pp60 - 74, Conference Paper, PUBLISHED  TARA - Full Text  DOI
Gerard Ekembe Ngondi, Vasileios Koutavas, Andrew Butterfield, Translation of CCS into CSP, Correct up to Strong Bisimulation, Mathematical Structures in Computer Science, 2022, Journal Article, SUBMITTED
Andrew Butterfield, Review of Understanding Programming Languages by Cliff B. Jones, Review of Understanding Programming Languages , by Cliff B. Jones , Formal Aspects of Computing, 2022, p60 - 74, Review, PUBLISHED  DOI
Gerard Ekembe Ngondi, Vasileios Koutavas, Andrew Butterfield, Translation of CCS into CSP, Correct up to Strong Bisimulation, Springer LNCS, Software Engineering and Formal Methods (SEFM 21), online, 6-10th December 2021, edited by Radu Calinescu, Corina S. Pasareanu , 13085, Springer, 2021, pp243 - 261, Conference Paper, PUBLISHED  TARA - Full Text  DOI
Andrew Butterfield, FV3-202 Formal Verification Report, November, 2021, i,ii,1-15, Report, PUBLISHED  TARA - Full Text  DOI
  

Page 1 of 9
Andrew Butterfield, Unifying Theories of Programming, Hamilton Institute Seminar, Maynooth University, Maynooth, 2023, Hamilton Institute, Maynooth University, Invited Talk, PRESENTED
Andrew Butterfield, 'andrewbutterfield/ccs2csp v0.5.0.0', v0.5.0.0, https://zenodo.org/record/6861751#.Yw3uZuzMLUI, Zenodo.org, CERN, 2022, -, Software, PUBLISHED
Andrew Butterfield, John Szymanski (eds.), A Dictionary of Electronics and Electrical Engineering, Fifth Edition, Oxford, UK, Oxford University Press, 2018, Notes: [We edited the Fifth Edition, revising etries and adding new ones.], Book, PUBLISHED
Andrew Butterfield, Gerard Ekembe Ngondi (eds.), Oxford Dictionary of Computer Science, Seventh Edition, Oxford, UK, Oxford University Press, 2016, i - 627pp, Notes: [We acted as editors for 7th edition, which included deleting, revising and adding in entries.], Book, PUBLISHED
Andrew Butterfield, 'Unifying Theories of Programming Theorem Prover', 0.97a9, bitbucket.org + own TCD webpages, 2013, -, Notes: [Development started in 2007 and is ongoing. Associated Peer-reviewed publications at UTP2010 and UTP 2012 conferences.], Software, PUBLISHED
Riccardo Bresciani, Andrew Butterfield, Towards a UTP-style framework to deal with probabilities, Dublin, Ireland, TCD-CS Technical Reports, August, 2011, 1-29, Report, PUBLISHED
Freitas, L. , Woodcock, J. , Butterfield, A., POSIX and the verification grand challenge: A roadmap, IEEE International Conference on Engineering of Complex Computer Systems, ICECCS, 2008, 153-162pp, Notes: [Article number 4492888], Invited Talk, PUBLISHED
Foreword: Selected papers from the ninth international workshop on formal methods for industrial critical systems (FMICS 04), Linz, Austria, Editorial Board, PUBLISHED
Andrew Butterfield and Jim Woodcock, Formalising Flash Memory: First Steps, ICECCS 2007, Auckland, New Zealand, 11th-14th July, 2007, IEEE Computer Society, Notes: [paper invited for special session on Grand Challenges - Complex Program Verifier], Invited Talk, PUBLISHED
Malcolm Dowse, Andrew Butterfield, Marko van Eekelen, and Maarten, Towards Machine Verified Proofs for I/O, nijmeegs institut voor informatica en informatiekunde, 2004, (NIIIR0415), Notes: [URL: http://www.cs.kun.nl/research/reports/. ], Report, PUBLISHED

  

Page 1 of 3

Awards and Honours

Award Date
Invite to Symposium in honour of Prof. Jim Woodcock 3rd September 2024
Elected to TCD Fellowship 22nd April 2024
Invite to Symposium in honour of Prof. He Jifeng 15th September 2023
Invite to UTP Symposium in honour of Prof. Tony Hoare 8th October 2019
Dagstuhl Invitation: Seminar 14062 2nd-6th Feb 2014
Festschrift Invitation: Dines Bjoerner & Zhou Chaochen 2007
Gold Medal awarded with Degree Nov 1983
Foundation Scholarship, Trinity College May 1981

Research Interests

Description Of Research Interests

My PhD (1990) was in software for chip designs, but I switched my research to theoretical studies on the use of logic to prove the correctness of computer systems (Formal Methods). Initial research focussed on specialised programming languages, working with colleagues here at TCD. A major step was starting a collaboration in 1999 with Jim Woodcock (then at Oxford) where I assisted him in developing a formal semantics for a hardware description language called Handel-C. Here my PhD expertise helped out as the problem we had to formalise covered both software and hardware aspects. Jim Woodcock introduced me to the Unifying Theories of Programming (UTP) paradigm linking diverse theories about computing systems into a common framework. Early work focussed on a general theory of time-slots, with notions of priorities and probabilities. This then switched to a verification grand challenge regarding file-systems, especially flash drives. More recent work has focussed on a deep theory of concurrency, and developing software tools to support theory development. My involvement in Lero, the Irish Software Research Centre, led to me being asked by the European Space Agency to bring formal methods expertise to an activity to qualify the RTEMS operating system for spaceflight. The impact of this is that formal notations and verification software we produced are now part of data-packages ESA provides for missions, and has been fed back into RTEMS itself. My current focus is now on using UTP to show the correctness of how these formal notations interact with each other. The idea is that the ESA work now becomes a testbed for my theories. Over time I supervised four postdocs: two funded by the EU: Claus Pahl (1996) and Gerard Ekembe Ngondi (2020-22), and two funded by ESA: David Sanan (2011-13) and Frederic Tuong (2019-21).