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 -Course Dir. BA ICT (Computer Science)


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.

  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
 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)
 Unifying Synchronous Systems

Page 1 of 2
Details Date
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
Language Skill Reading Skill Writing Skill Speaking
English Fluent Fluent Fluent
French Medium Basic Basic
Details Date From Date To
IFIP Technical Committee, Working Group 1.9/2.15 Software Verification, invited as observer April 2016 present
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, UTCP: compositional semantics for shared-variable concurrency, Lecture Notes in Computer Science, 20th Brazilian Symposium on Formal Methods (SBMF 2017), Recife, Brazil, 29 Nov - 1st Dec 201, LNCS, (10623), Springer, 2017, pp253 - 270, Conference Paper, PUBLISHED  TARA - Full Text  DOI  URL
Andrew Butterfield, UTPCalc - A calculator for UTP Predicates, LNCS, The 6th International Symposium on Unifying Theories of Programming, Reykjavik, Iceland, 5-6th June 2016, edited by Jonathan Bowen, Huibiao Zhu , 11304, Springer International Publishing, 2017, pp197 - 216, Conference Paper, PUBLISHED  TARA - Full Text  DOI  Other
Andrew Butterfield, Ciaran Costello, Domain-Specific Languages for Requirements Modelling (with a focus on IMA Separation Kernels), DASIA 2017 DAta Systems In Aerospace, Gothenburg, Sweden, 30th May - 1st June, 2017, pp1 - 5, Conference Paper, PUBLISHED
James Woodcock, Simon Foster, Andrew Butterfield, Heterogeneous Semantics and Unifying Theories, 7th International Symposium on Leveraging Applications of Formal Methods, Verification And Validation (ISoLA 2016), Corfu, Greece, 10-14 October 2016, edited by Tiziana Margaria, Bernhard Steffen , Springer International Publishing, 2016, pp374 - 394, Conference Paper, PUBLISHED  DOI
Andrew Butterfield, Anila Mjeda, John Noll, UTP Semantics for Shared-State, Concurrent, Context-Sensitive Process Models, 10th International Symposium on Theoretical Aspects of Software Engineering, TASE 2016, Shanghai, China, 17-19 July 2016, edited by Marcello Bonsangue, Yuxing Deng , IEEE Computer Society, 2016, pp93 - 100, Conference Paper, PUBLISHED  TARA - Full Text  DOI  URL
Artur O. Gomes and Andrew Butterfield, Modelling the Haemodialysis Machine with Circus, LNCS, Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, 23-27 May 2016, edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, and Miklos Biro , 9675, Springer International Publishing, 2016, pp409 - 424, Conference Paper, PUBLISHED  TARA - Full Text  DOI  URL
Andrew Butterfield, Alexandre Cortier, Kevin Hennessy, Mike Hinchey, Towards Formal Verification of Interrupts and Hypercalls, DASIA 2016 DAta Systems In Aerospace, Tallinn, Estonia, 10-05-2016, edited by L. Ouwehand , ESA Communications, ESTEC, NL, 2016, pp4 , Notes: [European Space Agency, (Special Publication) ESA SP, SP-736, 2016], Conference Paper, PUBLISHED
Mark Hann, Regis de Ferluc, Alexandre Cortier, Julien Galizzi, Andrew Butterfield, Qualification Strategy and Plan for Integrated Modular Avionics for Space Separation Kernel, ESA Communications, ESTEC, NL, DASIA 2016 DAta Systems In Aerospace, Tallinn, Estonia, 10 May 2016, edited by L. Ouwehand , 2016, pp1 - 4, Notes: [[European Space Agency (Special Publication) ESA-SP, SP-736, 2016]], Conference Paper, PUBLISHED
John Noll, Andrew Butterfield, Teaching Global Software Development through Game Design, GSE-Ed'16 First Intranational Workshop on Global Software Engineering Education, Orange County, California, USA, 2nd August 2016, edited by Sarah Beecham, Tony Clear , IEEE Computer Society, 2016, pp55 - 60, Conference Paper, PUBLISHED  DOI
Butterfield, A., Hinchey, M., Towards the adoption of formal techniques for kernel qualification, European Space Agency, (Special Publication) ESA SP, SP-732, 2015, Conference Paper, PUBLISHED
  

Page 1 of 6
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 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
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
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
Andrew Butterfield, Thomas Arts and Wan Fokkink, 8th International Workshop on Formal Methods in Industrial Critical Systems (FMICS'03), ERCIM, 2003, Meetings /Conferences Organised, PUBLISHED
Andrew Butterfield and Malcolm Tyrrell, Typing and Subtyping for an Object-Oriented Process Algebra, Department of Computer Science, University of Dublin, Trinity College, 2002, (TCD-CS-2002-13), Report, PUBLISHED

  

Page 1 of 3
Award Date
Foundation Scholarship, Trinity College May 1981
Gold Medal awarded with Degree Nov 1983
Dagstuhl Invitation: Seminar 14062 2nd-6th Feb 2014
Festschrift Invitation: Dines Bjoerner & Zhou Chaochen 2007
Current active interests and area of expertise

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

Developments of formal modelling techniques for On-board Space Software. This follows on from recent investigative work as a formal methods expert for ESA in the area of kernel qualification.

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

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.

Past areas of interest: 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).