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, Formal Aspects of Computing Journal. Feb 2015
Program Committee Chair: 2nd Irish Workshop in Formal Methods 1998
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
IFIP Technical Committee, Working Group 1.9/2.15 Software Verification, invited as observer April 2016 October 2016
Member of Irish Mathematical Society
Founder member of the Irish Formal Methods Special Interest Group (IFMSIG)
Committee Member, Formal Methods Europe (FME) 1994 present
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, 'Formal Verification', RTEMS Software Engineering, master, https://docs.rtems.org/branches/master/eng/index.html, 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
Mjeda, A. and Butterfield, A. and Noll, J., Business process modeling flexibility: A formal interpretation, 2019, pp467-474 , Notes: [cited By 0], Conference Paper, PUBLISHED
Gomes, A.O. and Butterfield, A., Circus2CSP: A tool for model-checking circus using FDR, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 11800 LNCS, 2019, p235-242 , Notes: [cited By 0], Journal Article, PUBLISHED  TARA - Full Text  DOI
Gomes, A.O. and Butterfield, A., Towards a model-checker for circus, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 11800 LNCS, 2019, p217-234 , Notes: [cited By 0], Journal Article, PUBLISHED  TARA - Full Text  DOI
Butterfield, A., The Inner and Outer Algebras of Unified Concurrency, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 11885 LNCS, 2019, p157-175 , Notes: [cited By 0], Journal Article, PUBLISHED  TARA - Full Text  DOI
  

Page 1 of 7
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, Gerard Ekembe Ngondi, 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-162 pp, Notes: [Article number 4492888], Invited Talk, PUBLISHED
Butterfield, A., A denotational semantics for handel-C , LNCS, Formal Methods and Hybrid Real-Time Systems, Essays in Honor of Dines Bjørner and Chaochen Zhou on the Occasion of Their 70th Birthdays, Macau, China, 2007, edited by Cliff B. Jones, Zhiming Liu, Jim Woodcock , 4700, Springer, 2007, pp45-66 , Conference Paper, PUBLISHED
Andrew Butterfield, A Denotational Semantics for Handel-C, Formal Methods and Hybrid Real-Time Systems 2007, Macau SAR, China, 24-25 September 2007, 2007, 45 - 66pp, Notes: [Essays in Honor of Dines Bjoerner and Chaochen Zhou on the Occasion of Their 70th Birthdays], Invited Talk, 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. 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

Current active interests and area of expertise

Using the model-checker SPIN to do test-generation for the open-source RTEMS operating system, in collaboration with the European Space Agency, and companies that help develop and maintain RTEMS.

Exploring UTP semantics for shared-variable concurrency as a baseline for exploring formal aspects of concurrent software development methodologies, in collaboration with Jim Woodcock.

Unifying Theories of Clocked Parallel Systems; Priority and Probability in same; Formal Semantics of Handel-C; UTP Theorem Prover development.

Past areas of interest: A new emerging area of interest and expertise is the application of formal modelling techniques to descriptions of complex software development processes, with a particular focus on the requirements of medical device software certification. Also of interest is being involved in advocating a more product-oriented approach to critical medical software certification, rather than the process focus that is currently employed. This work will be done in collaboration with colleagues from Lero.

Exploring the feasibility of formally proving the correctness of a Time-Space Partitioning Kernel (TSPK) , as part of the European Space Agency's Savoir-IMA activity.

Process Algbras with Unbounded Dual Non-determinism; External Effects of Functional I/O; Function-based Formal Methods. Silicon Compilation via Functional Languages;

FORMAL SEMANTICS OF HANDEL-C

Recent work has explored giving a formal semantics to Handel-C, by first considering a carefully chosen subset, designed to ensure all awkward language features are considered, to ensure full industrial applicability of the research results. This work has been done in collaboration with Professor Jim Woodcock of the university of York.

THEORIES OF CLOCKED PARALLEL SYSTEMS

I developed an expertise in the relatively new Unifying Theories Framework, with a view to using this framework to present my theories of hardware compilation in general, and Handel-C semantics in particular. Of particular interest in this area is an emerging theory of synchronous Circus, and a denotational semantics for Handel-C based on "hardware compilation". Also in collaboration with Professor Jim Woodcock.

EXTERNAL EFFECTS OF FUNCTIONAL I/O

A particularly strong move has been towards the formal modelling of input/output and real-world interactions in pure functional languages with referentially transparent I/O systems based either on monads, or uniqueness typing.

PROCESS ALGEBRAS WITH UNBOUNDED DUAL NON-DETERMINISM

In collaboration with Prof Joseph Morris at DCU, I am also working on a theory of process algebras with unbounded demonic and angelic non-determinism, developed by formally "lifting" a deterministic theory to the non-determinsistic level.

SILICON COMPILATION VIA FUNCTIONAL LANGUAGES:

My Ph.D. research (1990) explored the use of pure functional languages as a tool for supporting silicon compilation.

FUNCTIONAL-BASED FORMAL METHODS:

My main research interest then switched to formal modelling techniques with a pure functional flavour, as exemplified by work done as part of the "Irish School of VDM".

THE FACS PROJECT: I supervised a graduate student under the FACS project, looking into modifying the pi-calculus to describe the kinds of object-oriented systems developed using the CORBA object technology .

RESEARCH-LED CONSULTANCY In the period from July 1991, through to 1997/98, I was involved, through company "K&M Technologies", in research-led consultancy, looking to apply formal techniques in industry. Most clients were involved in telecommunications (Motorola, Ericsson). Some of this work was carried out through EU-funded RACE and ACTS projects (SCORE, Mobilise).