Skip to main content

Trinity College Dublin, The University of Dublin

Trinity Menu Trinity Search



Dr. Andrew Butterfield
Assistant Professor, Computer Science

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.

Publications and Further Research Outputs

Peer-Reviewed Publications

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, 2024 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 Conference Paper, 2024 URL

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 Conference Paper, 2023 TARA - Full Text 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, 2023 DOI TARA - Full Text

Andrew Butterfield, 'Formal Verification', RTEMS Software Engineering, master, https://docs.rtems.org/branches/master/eng/index.html, RTEMS.org, 2023, - Protocol or guideline, 2023 URL

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, 2022

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, 2022 DOI TARA - Full Text

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, 2022 DOI

Andrew Butterfield, FV3-202 Formal Verification Report, November, 2021, i,ii,1-15 Report, 2021 DOI TARA - Full Text

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, 2021 TARA - Full Text DOI

Mjeda, A. and Butterfield, A. and Noll, J., Business process modeling flexibility: A formal interpretation, 2019, pp467-474 Conference Paper, 2019

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 Journal Article, 2019 DOI TARA - Full Text

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 Journal Article, 2019 DOI TARA - Full Text

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 Journal Article, 2019 DOI TARA - Full Text

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, 2017 TARA - Full Text URL DOI

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, 2017 DOI TARA - Full Text Other

Butterfield, A., UTPcalc: a calculator for UTP predicates, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10134 LNCS, 2017, p197-216 Journal Article, 2017

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, 2017 TARA - Full Text

A Dictionary of Computer Science, 2016, [Andrew Butterfield, Gerard Ekembe Ngondi] Item in dictionary or encyclopaedia, etc, 2016

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, 2016 DOI

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 Conference Paper, 2016 TARA - Full Text

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, 2016 DOI

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 Conference Paper, 2016

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, 2016 TARA - Full Text URL DOI

Andrew Butterfield, IMA-KQP Phase 4: R1: Formal Methods Expertise " Final Report, July, 2016, p1 - 73 Report, 2016 TARA - Full Text DOI

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, 2016 DOI TARA - Full Text URL

Formal Aspects of Computing, ACM, [Responsible for handling submitted papers and overseeing the process of review and feedback. I make recommendations to the editor-in-chief.], 2015 Editorial Board, 2015

Beg, A., Butterfield, A., Development of a prototype translator from Circus to CSPm, ICOSST 2015 - 2015 International Conference on Open Source Systems and Technologies, Proceedings, ICOSST 2015 - 2015 International Conference on Open Source Systems and Technologies, Proceedings, Lahore; Pakistan, 17-19 Dec, 2015, pp16-23 Conference Paper, 2015 DOI

Jordan, H., Botterweck, G., Noll, J., Butterfield, A., Collier, R., A feature model of actor, agent, functional, object, and procedural programming languages, Science of Computer Programming, 98, (P2), 2015, p120-139 Journal Article, 2015

Howell Jordan, Goetz Botterweck, Andrew Butterfield, Rem Collier, John Noll, A Feature Model of Actor, Agent, Functional, Object, and Procedural Programming Languages, Science of Computer Programming, 98, (2), 2015, p120 - 139 Journal Article, 2015 TARA - Full Text 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, 2015

Riccardo Bresciani, Andrew Butterfield, A UTP approach towards probabilistic protocol verification, Security and Communication Networks, 7, 2014, p99 - 107 Journal Article, 2014 DOI

Butterfield, A., Sanán, D., Hinchey, M., Formalisation of a separation micro-kernel for common criteria certification, European Space Agency (Special Publication) ESA SP, SP 725, 2014 Conference Paper, 2014

David Sanan, Andrew Butterfield, Mike Hinchey, Separation Kernel Verification: The XtratuM Case Study, LNCS, Verified Software: Theories, Tools and Experiments, Vienna, July 17-18, 2014, edited by Dimitra Giannakopoulou, Daniel Kroening, Elizabeth Polgreen, Natarajan Shankar , 8471, Springer, 2014, pp133 - 149 Conference Paper, 2014 DOI TARA - Full Text

John Noll, Andrew Butterfield, Kevin Farrell, Tom Mason, Miles McGuire, Ross McKinley, GSD Sim: A Global Software Development Game, 2014 IEEE International Conference on Global Software Engineeering Workshops, 2014 Journal Article, 2014

Butterfield, A., U & middot;(TP)2: Higher-order equational reasoning by pointing, Electronic Proceedings in Theoretical Computer Science, EPTCS, 167, 2014, p14-22 Journal Article, 2014

Andrew Butterfield, UTP2: Higher-Order Equational Reasoning by Pointing, Electronic Proceedings in Theoretical Computer Science, Proceedings Eleventh Workshop on User Interfaces for Theorem Provers, Vienna, 17th July 2014, edited by Christoph Benzmüller and Bruno Woltzenlogel Paleo , 167, 2014, pp14 - 22 Conference Paper, 2014 DOI TARA - Full Text

Butterfield, A., The logic of U . (TP)2 , Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4th International Symposium on Unifying Theories of Programming, UTP 2012, Paris, 7681, 2013, pp124-143 Conference Paper, 2013 DOI

Riccardo Bresciani and Andrew Butterfield, A probabilistic theory of designs based on distributions, LNCS, UTP 2012 : 4th International Symposium on Unifying Theories of Programming, Paris, France, 27-28th August 2012, edited by Wolff, Burkhard; Gaudel, Marie-Claude; Feliachi, Abderrahmane , 7681, Springer, 2013, pp105 - 123 Conference Paper, 2013 DOI

Goetz Botterweck, Andrew Butterfield, Howell Jordan, Andreas Pleuss, David Sanán, and Emil Vassev, Methods and Tools for On-board Software Engineering - Final Report, European Space Agency, December, 2013, p1 - 10 Report, 2013

Riccardo Bresciani, Andrew Butterfield, From Distributions to Probabilistic Reactive Programs, LNCS, Theoretical Aspects of Computing - ICTAC 2013, Shanghai, China, 4-6th September 2013, edited by Zhiming Liu, Jim Woodcock, Huibiao ZHu , 8049, Springer, 2013, pp94 - 111 Conference Paper, 2013 DOI

Reasoning about I/O in Functional Programs in, editor(s)Viktoria Zsok, Zoltan Horvath, Rinus Plasmeijer , Central European Functional Programming School - Fourth Summer School, CEFP 2011, Heidelberg, Springer, 2012, pp93 - 141, [Andrew Butterfield] Book Chapter, 2012 DOI

Riccardo Bresciani, Andrew Butterfield, A UTP semantics of pGCL as a homogeneous relation, Integrated Formal Methods 2012, Pisa, Italy, June 19-21, 2012, edited by Diego Latella, Helen Treharne , 7321, 2012, 191-205 Conference Paper, 2012 DOI

Andrew Butterfield, Denotational Semantics of Handel-C, Formal Aspects of Computing, 23, (2), 2011, p153 - 170 Journal Article, 2011 DOI URL

Pawel Gancarski, Andrew Butterfield, Prioritized slotted-Circus, LNCS, 7th International Colloqium on Theoretical Aspects of Computing, Natal, Brazil, 1-3 September 2010, edited by David Déharbe and Ana Cavalcanti , 6255, 2010, pp91 - 105 Conference Paper, 2010 URL DOI

Butterfield, A., Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 5713 LNCS, 2010 Journal Article, 2010

Andrew Butterfield(ed.), Unifying Theories of Programming, 2nd International Symposium, UTP 2008, Dublin, Ireland, September 8-10, 2008, Revised Selected Papers., LNCS, Dublin, Ireland, 5713, September 8-10th, Springer, 2010 Proceedings of a Conference, 2010 DOI URL

Beg, A., Butterfield, A., Modelling flash devices with FDR: Progress and limits, Proceedings of the 8th International Conference on Frontiers of Information Technology, FIT'10, 2010 Journal Article, 2010

Riccardo Bresciani, Andrew Butterfield, ProVerif Analysis of the ZRTP Protocol, International Journal for Infonomics, 3, (3), 2010, p306 - 313 Journal Article, 2010 URL

Andrew Butterfield, Saoithin: A Theorem Prover for UTP, LNCS, Unifying Theories of Programming, Third International Symposium, UTP 2010, Shanghai, China, 15-16 November 2010, edited by Shenchao Qin , 6445, Springer, 2010, pp137 - 156 Conference Paper, 2010 URL DOI

Beg, A., Butterfield, A., Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation, Proceedings of the 8th International Conference on Frontiers of Information Technology, FIT'10, 2010 Journal Article, 2010

Bresciani, Riccardo and Butterfield, Andrew, Weakening the Dolev-Yao model through probability, SIN '09: Proceedings of the 2nd international conference on Security of information and networks, Famagusta, North Cyprus, 6th-10th October, edited by Atilla Elçi, Mehmet A. Orgun, & Alexander Chefranov , ACM, 2009, pp293 - 297 Conference Paper, 2009 DOI

Pawel Gancarski, Andrew Butterfield, Jim Woodcock, State Visibility and Communication in Unifying Theories of Programming, IEEE Computer Society, 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, Tianjin, China, July 29-31, edited by Wei-Ngan Chin and Shengchao Qin , IEEE Computer Society, 2009, pp47 - 54 Conference Paper, 2009 URL DOI

Andrew Butterfield, Leo Freitas, Jim Woodcock, Mechanising a Formal Model of Flash Memory, Science of Computer Programming, 74, (4), 2009, p219 - 237 Journal Article, 2009 DOI TARA - Full Text

Riccardo Bresciani and Andrew Butterfield, A formal security proof for the ZRTP Protocol, The 4th International Conference for Internet Technology and Secured Transactions (ICITST-2009), London, UK, Nov. 9-13th 2009, Infonomics Society, 2009, pp1 - 6 Conference Paper, 2009 DOI URL

Andrew Butterfield, Art O Cathain, Concurrent Models of Flash Memory Device Behaviour, Lecture Notes in Computer Science - Formal Methods: Foundations and Applications, 12th Brazilian Symposium on Formal Methods (SBMF 2009), Gramado, Brazil, 19-21 August, edited by Jim Woodcock, Marcel Oliveira , 5902, Springer, 2009, pp70-83 Conference Paper, 2009 TARA - Full Text DOI

Luca Longo, P. Dondio, R. Bresciani, S. Barret, A. Butterfield, Enabling Adaptation in trust computations, Computation World: Future Computing, Service Computation, Cognitive, Adpative, Content, Patterns, 2009, pp701 - 706 Conference Paper, 2009 DOI

Andrew Butterfield, Pawel Gancarski, The Denotational Semantics of Slotted-Circus, Lecture Notes in Computer Science, Formal Methods 2009, Eindhoven, Netherlands, 2-6th Nov, edited by Ana Cavalcanti and Dennis Dams , 5850, Springer, 2009, pp451-466 Conference Paper, 2009 DOI TARA - Full Text

Gancarski, P., Butterfield, A., The denotational semantics of slotted-circus, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 5850 LNCS, 2009, p451-466 Journal Article, 2009

Butterfield, A., A denotational semantics for handel-C, 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, 2007, 45-66pp Invited Talk, 2007 URL DOI

Andrew Butterfield, Adnan Sherif and Jim Woodcock, Slotted-Circus: A UTP-Family of Reactive Theories, Lecture Notes in Computer Science, Integrating Formal Methods 2007 (IFM2007), Oxford, UK, 2-5 July, edited by J. Davies and J. Gibbons , 4591, Springer, 2007, pp75-97 Conference Paper, 2007 TARA - Full Text DOI

Horváth, Z., Zsók, V., Butterfield, A., Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): Preface, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 4449 LNCS, 2007 Journal Article, 2007

Andrew Butterfield and JimWoodcock, A "Hardware Compiler" Semantics for Handel-C, Electronic Notes in Theoretical Computer Science, Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology (MFCSIT 2004), Dublin, Ireland, 22-23 July 2004, edited by A.K. Seda, T. Hurley, M. Schellekens, M. Mac an Airchinnigh and G. Strong , 161, Elsevier Science Direct, 2006, pp73 - 90 Conference Paper, 2006 DOI URL

Andrew Butterfield, 17th International Workshop on Implementations and Applications of Functional Languages, 19-21st Sep. 2005, 2006, Dublin, Ireland, A. Butterfield, C. Grelck, F. Huch, Springer, 4015, LNCS Meetings /Conferences Organised, 2006 URL

Malcolm Tyrrell, Joseph M. Morris, Andrew Butterfield and Arthur Hughes, A Lattice-Theoretic Model for an Algebra of Communicating Sequential Processes, LNCS, Theoretical Aspects of Computing - ICTAC 2006, Tunis, Tunisia, 20-24th Nov. 2006, edited by Kamel Barkaoui, Ana Cavalcanti and Antonio Cerone , 4281, Springer, 2006, pp123 - 137 Conference Paper, 2006 DOI URL

Andrew Butterfield and Malcolm Dowse, Deterministic Concurrent I/O, ACM SIGPLAN, The 11th ACM SIGPLAN International Conference on Functional Programming (ICFP 2006), Portland, Oregon, 18th-20th Sep. 2006, edited by Julia Lawall , ACM Press, 2006, pp148 - 159 Conference Paper, 2006 URL DOI

Andrew Butterfield and Jim Woodcock, prialt in Handel-C: an operational semantics, International Journal on Software Tools for Technology Transfer, 7, (3), 2005, p248 - 267 Journal Article, 2005 URL DOI

Malcolm Dowse, Andrew Butterfield, and Marko van Eekelen, A language for reasoning about concurrent functional i/o, LNCS, Implementation and Application of Functional Languages: 16th International Workshop, IFL 2004, Revised Selected Papers, Lubeck, Germany, 8-10th Sep. 2004, edited by C. Grelck, F. Huch, G. J. Michaelson , 3474, Springer, 2005, pp177 - 194 Conference Paper, 2005 URL DOI

Andrew Butterfield and Juan Biccaregui(ed.), 9th International Workshop on Formal Methods in Industrial Critical Systems (FMICS'04), Electronic Notes in Theoretical Computer Science, Linz, Austria, 133, 20-21 Sep. 2004, Elsevier Science Direct, 2004, 1-332 p Proceedings of a Conference, 2004 URL

Andrew Butterfield and Jim Woodcock, Semantic domains for handel-c., Electronic Notes in Theoretical Computer Science, 74, 2003 Conference Paper, 2003 DOI

Andrew Butterfield and Jim Woodcock, An operational semantics for handel-c., Electronic Notes in Theoretical Computer Science, 80, 2003 Conference Paper, 2003 DOI

Butterfield, Andrew and Dowse, Malcolm and Strong, Glenn, Proving make correct: I/O proofs in Haskell and Clean, Lecture Notes in Computer Science, Implementation of Functional Languages, 14th International Workshop, IFL 2002, Madrid, Spain, 16-18 September 2002, edited by R. Peña and T. Arts , 2670, 2002, pp16 - 18 Conference Paper, 2002 URL DOI

Butterfield, A., Strong, G, Proving Correctness of Programs with IO - A Paradigm Comparison, LNCS , 13th International workshop on the Implementation of Functional Languages, Stockholm, Sweden, September 2001, edited by Arts, T and Mohnen M , 2312, 2002, pp72 - 87 Conference Paper, 2002 DOI URL

Andrew Butterfield and Jim Woodcock, Semantics of prialt in Handel-C (tm), Communicating Process Architectures, edited by James Pascoe, Peter Welch, Roger Loader, and Vaidy Sunderam , 2002, pp1 - 16 Conference Paper, 2002

Andrew Butterfield and Glenn Strong, Proving correctness of programs with IO - A paradigm comparison, Lecture Notes in Computer Science, Implementation of Functional Languages, 13th International Workshop, IFL 2001, Stockholm, Sweden, September, edited by Thomas Arts and Markus Mohnen , 2312, 2001, pp72 - 87 Conference Paper, 2001 DOI

Andrew Butterfield and Glenn Strong(ed.), 5th Irish Workshop in Formal Methods, electronic Workshops in Computing, 2001 Proceedings of a Conference, 2001

Andrew Butterfield and Klemens Haegele(ed.), 3rd Irish Workshop in Formal Methods, electronic Workshops in Computing, 1999 Proceedings of a Conference, 1999

Andrew Butterfield and Sharon Flynn(ed.), 2nd Irish Workshop in Formal Methods, electronic Workshops in Computing, 1998 Proceedings of a Conference, 1998

Andrew Butterfield, Recursion Diagrams: ideas for a Geometry of Formal Methods, 3rd BCS-FACS Northern Formal Methods Workshop, electronic Workshops in Computing, Ilkley, West Yorkshire, U.K., September, edited by Andy Evans, David Duke, and Tony Clarke , 1998 Conference Paper, 1998

Andrew Butterfield, A VDM study of fault-tolerant stable storage: towards a computer engineering mathematics, LNCS, FME'93: Industrial-Strength Formal Methods, Odense, Denmark, March 1993, edited by J.C.P.Woodcock and P.G.Larsen , 670, Springer, 1993, pp216 - 234 Conference Paper, 1993

Andrew Butterfield, A functional/hierarchical Layout Tool. In Colloqium on Silicon Compilation, Savoy Place, London,, May, 1989, pp4/1 - 4/5 Conference Paper, 1989

Andrew Butterfield, From KARL to CIF, EURO CVIM 1986 - European Conference of Customer/Vendor Interfaces in Microelectronics, Gesellschaft f"ur Mathematikund Datenverarbeitung, University of Kaiserslautern, West Germany, September, edited by R. W. Hartenstein et al. , 1986, pp130 - 141 Conference Paper, 1986

Non-Peer-Reviewed Publications

Andrew Butterfield, Unifying Theories of Programming, Hamilton Institute Seminar, Maynooth University, Maynooth, 2023, Hamilton Institute, Maynooth University Invited Talk, 2023 TARA - Full Text

Andrew Butterfield, 'andrewbutterfield/ccs2csp v0.5.0.0', v0.5.0.0, https://zenodo.org/record/6861751#.Yw3uZuzMLUI, Zenodo.org, CERN, 2022, - Software, 2022 URL DOI URL

Andrew Butterfield, John Szymanski (eds.), A Dictionary of Electronics and Electrical Engineering, Fifth Edition, Oxford, UK, Oxford University Press, 2018 Book, 2018

Andrew Butterfield, Gerard Ekembe Ngondi (eds.), Oxford Dictionary of Computer Science, Seventh Edition, Oxford, UK, Oxford University Press, 2016, i - 627pp Book, 2016

Andrew Butterfield, 'Unifying Theories of Programming Theorem Prover', 0.97a9, bitbucket.org + own TCD webpages, 2013, - Software, 2013 URL URL

Riccardo Bresciani, Andrew Butterfield, Towards a UTP-style framework to deal with probabilities, Dublin, Ireland, TCD-CS Technical Reports, August, 2011, 1-29 Report, 2011 TARA - Full Text

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 Invited Talk, 2008 URL TARA - Full Text DOI

Foreword: Selected papers from the ninth international workshop on formal methods for industrial critical systems (FMICS 04), Linz, Austria Editorial Board, 2007

Andrew Butterfield and Jim Woodcock, Formalising Flash Memory: First Steps, ICECCS 2007, Auckland, New Zealand, 11th-14th July, 2007, IEEE Computer Society Invited Talk, 2007 DOI URL

Malcolm Dowse, Andrew Butterfield, Marko van Eekelen, and Maarten, Towards Machine Verified Proofs for I/O, nijmeegs institut voor informatica en informatiekunde, 2004, (NIIIR0415) Report, 2004

Andrew Butterfield, Thomas Arts and Wan Fokkink, 8th International Workshop on Formal Methods in Industrial Critical Systems (FMICS'03), ERCIM, 2003 Meetings /Conferences Organised, 2003

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, 2002

A. Butterfield, Denotational Semantics for prialt-free Handel-C, Department of Computer Science, University of Dublin, Trinity College, 2001, (TCD-CS-2001-53) Report, 2001

Andrew Butterfield and Glenn Strong, Comparing Proofs about I/O in Three Programming Paradigms, Department of Computer Science, University of Dublin, Trinity College, 2001, (TCD-CS-2001-31) Report, 2001

A. Butterfield, Interpretative Semantics for prialt-free Handel-C, Department of Computer Science, University of Dublin, Trinity College, 2001, (TCD-CS-2001-54) Report, 2001

Butterfield, A., 4th Irish Workshop in Formal Methods, electronic Workshops in Computing, 2000, David Sinclair Meetings /Conferences Organised, 2000

Ted Hurley, M"ýche"al Mac an Airchinnigh, Michel Schellekens, and Andrew Butterfield, First Irish Conference on the Mathematical Foundations of Electronic Notes in Theoretical Computer Science, July, 2000, Elsevier, 40 Meetings /Conferences Organised, 2000

Micheal Mac an Airchinnigh, Andrew Butterfield, Arthur Hughes, Handbook of Mathematics, 2000, - Miscellaneous, 2000 TARA - Full Text

Andrew Butterfield, Alexis Donnelly, and Malcom Tyrrell, OO-Motivated Process Algebra: A Calculus for CORBA-like Systems, Department of Computer Science, University of Dublin, Trinity College, 1999, (TCD-CS-1999-54) Report, 1999

J.M. Wing, J J.Woodcock, and Andrew Butterfield, World Congress on Formal Methods in the Development of Computing Systems, September, 1999, Springer, 1709, Lecture Notes in Computer Science Meetings /Conferences Organised, 1999

Andrew Butterfield, Recursion Diagrams: ideas for a Geometry of Formal Methods, Department of Computer Science, University of Dublin, Trinity College, 1999, (TCD-CS-1999-04) Report, 1999

Andrew Butterfield, Andy Evans, David Duke, and Tony Clarke, Electronic Workshops in Computing, September, 1998, Ilkley, West Yorkshire, U.K. Meetings /Conferences Organised, 1998

Andrew Butterfield, Andy Evans, David Duke, and Tony Clarke, Èlectronic Workshops in Computing, July, 1997, Ilkley, West Yorkshire, U.K. Meetings /Conferences Organised, 1997

Henry McLoughlin and Gerard O'Regan, 1st Irish Workshop in Formal Methods, electronic Workshops in Computing, 1997, 1997 Meetings /Conferences Organised, 1997

A. Butterfield, On mapped reduction, Department of Computer Science, University of Dublin, Trinity College, 1993, (TCD-CS-93-39) Report, 1993

A. Butterfield, The careful memory abstraction in stable storage, Department of Computer Science, University of Dublin, Trinity College, 1993, (TCD-CS-93-31) Report, 1993

A. Butterfield, Memory models: A formal analysis using VDM, Department of Computer Science, University of, 1992, (TCD-CS-92-27) Report, 1992

A. Butterfield, On curried function composition, Department of Computer Science, University of Dublin, Trinity College, 1992, (TCDCS-92-15) Report, 1992

B. Coghlan, J. Jones, and A. Butterfield, The sticks & stones project, Trinity College, Dublin, 1991, (TCD-CS-91-18) Report, 1991

Research Expertise

Description

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).

Projects

  • Title
    • RTEMS-SMP Qualification
  • Summary
    • RTEMS is an open-source real-time operating system that is widely used on satellites launched by the European Space Agency. Recent enhancements to RTEMS now require that it be be re-"qualified" as suitable for space-flight operations. We are part of a consortium that is doing a pre-qualification activity, which will not only lead to the use of the enhanced software in future missions, but will also be fed back into the open-source community that maintains RTEMS. The role of TCD, as part of Lero, the Irish Software Research Centre, is to explore the use of mathematically based reasoning and analysis techniques to assess the quality of the software.
  • Funding Agency
    • European Space Agency
  • Date From
    • 13/2/2019
  • Date To
    • 12/2/2021
  • Title
    • FMEIMAKQP - Formal Methods Expert for IMA Kernel Qualification Preparation
  • Summary
    • Research into how formal methods techniques could be deployed when certifying the correctness of a seperation kernel intended for managing on-board space software
  • Funding Agency
    • European Space Agency
  • Date From
    • Sep 2014
  • Date To
    • Jun 2016
  • Title
    • Methods and Tools for OnBoard Software Engineering
  • Summary
    • We developed a Reference Specification for a Partitioning, Separating Operating Microkernel, suitable for use onboard spacecraft. We then evaluated a suitable formal method to allow us to give a formal proof of the correctness of an implementation of that kernel, in code conforming to accepted safety critical standards. We then performed an initial feasibility study, to establish both the practicality and cost of such an approach to verification.
  • Funding Agency
    • European Space Agency
  • Date From
    • 01/06/2012
  • Date To
    • 31/11/2013
  • Title
    • PAISEAN: formal aspects
  • Summary
    • PAISEAN (Plan-driven, Agile, Inner-Source Environment Analysis Network) is a project as part of the 2nd phase of funding (2011-16) of the Lero CSET, with its PI base din UL.It looks at various aspects of software development processes in an increasingly agile and globalised working environment. This activity in TCD, focusses on formalising the language used to describe software development models, in order to support rigorous analysis, and certifiable tools for working in this space.
  • Funding Agency
    • SFI
  • Date From
    • Summer 2014
  • Date To
    • Summer 2015
  • Title
    • Formalising the Interface between Software and Hardware (FISH)
  • Summary
    • Verifying the correctness of safety-critical computer systems, particularly those that control machinery and vehicles, is an important but complex task. Many disparate aspects of the system need to modelled, each with their own peculiarities and interactions. This is why one of the Grand Challenges in Computer Science, GC6, on "Dependable Systems Evolution" focusses on techniques to mathematically verify the correctness of such systems. The goal of GC6 is to develop a repository of verified software components, consisting of formal specifications and software implementations along with proofs of correctness supported by automated proof tools and proof assistants. GC6 is a long-term research programme with a time horizon of ten to fifteen years. At present it is engaged in a series of research activities based around industrially inspired case-studies: recent such studies have included, for example, the validation of the Mondex smart-card's security protocols. A more recent case-study that has been adopted is that of a verified file-store for use in mission critical applications, suggested by NASA researchers who need such high-dependability systems for space research missions. This project builds on initial work on the formal modelling of flash memory systems, to use this case-study within GC6 to develop a comprehensive theoretical foundation for reasoning about hardware systems and their interface to software. This is viewed as being complementary to the notion of ``hardware/software co-Design'', that focusses on techniques for partitioning a system specification into hardware and software components in an efficient manner.
  • Funding Agency
    • SFI
  • Date From
    • 1st Sep. 2008
  • Date To
    • 30th Aug. 2011
  • Title
    • Unifying Synchronous Systems
  • Summary
    • This proposal will explore the development of a theory of hardware compilers within the UTP framework thus bridging the synchronous hardware, state-based, and message-based software domains under one theoretical umbrella. It is based on the observation that a denotational semantics for such languages corresponds to a discretely timed synchronous process algebra, and that there is a common theoretical framework independent of the fine detail and complexity needed to for particular language features. It is also intended that the theory will be accompanied by some methodology to assist in the resulting design process. This proposal will explore the development of a theory to allow system designers to develop embedded control systems in a manner that is safe and robust. It will achieve this by making it feasible for designer to prove the correctness of various safety-critical aspects of their systems, by allowing them to focus at each stage on what is important. As these systems are used to control vehicles such as cars and aircraft, as well as other machinery, assurance regarding their safe behaviour is vital and very much in the public interest.
  • Funding Agency
    • Science Foundation Ireland (SFI)
  • Date From
    • 1st Sep 2007
  • Date To
    • 30th Aug 2010
  • Title
    • Real World Formal Models for Pure Functional Programming
  • Summary
    • Looking at giving a formal semantics to the I/O behaviour of pure functional languages, with an emphasis on modelling the run-time systems.
  • Funding Agency
    • Enterprise Ireland
  • Date From
    • 2002
  • Date To
    • 2005
  • Title
    • DeStijl: Design and Specification Through Interfacing and Joining Languages
  • Summary
    • Exploring the unification of diverse formal specification and design languages by characterising the interfaces between the mathematical frameworks used to give their meanings.
  • Funding Agency
    • EU Contract no. CHRX-CT94-0591
  • Date From
    • 1996
  • Date To
    • 1999
  • Title
    • Formal Aspects of Corba Systems (FACS)
  • Summary
    • Development of formal models of appropriate subsets of the OMG Corba standard
  • Funding Agency
    • Enterprise Ireland
  • Date From
    • 1997
  • Date To
    • 2000

Keywords

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

Recognition

Representations

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

Awards and Honours

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

Memberships

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