| 2021 | SEFM | Translation of CCS into CSP, Correct up to Strong Bisimulation. | Gerard Ekembe Ngondi, Vasileios Koutavas, Andrew Butterfield |
| 2019 | FM | Towards a Model-Checker for Circus. | Artur Oliveira Gomes, Andrew Butterfield |
| 2019 | FM | Circus2CSP: A Tool for Model-Checking Circus Using FDR. | Artur Oliveira Gomes, Andrew Butterfield |
| 2019 | MODELSWARD | Business Process Modeling Flexibility: A Formal Interpretation. | Anila Mjeda, Andrew Butterfield, John Noll |
| 2016 | ICGSE | Teaching Global Software Development through Game Design. | John Noll, Andrew Butterfield |
| 2016 | ISoLA | Heterogeneous Semantics and Unifying Theories. | Jim Woodcock, Simon Foster, Andrew Butterfield |
| 2016 | TASE | UTP Semantics for Shared-State, Concurrent, Context-Sensitive Process Models. | Andrew Butterfield, Anila Mjeda, John Noll |
| 2014 | ICGSE | GSD Sim: A Global Software Development Game. | John Noll, Andrew Butterfield, Kevin Farrell, Tom Mason, Miles McGuire, Ross McKinley |
| 2013 | ICTAC | From Distributions to Probabilistic Reactive Programs. | Riccardo Bresciani, Andrew Butterfield |
| 2012 | IFM | A UTP Semantics of pGCL as a Homogeneous Relation. | Riccardo Bresciani, Andrew Butterfield |
| 2010 | FIT | Modelling flash devices with FDR: progress and limits. | Arshad Beg, Andrew Butterfield |
| 2010 | FIT | Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation. | Arshad Beg, Andrew Butterfield |
| 2010 | ICTAC | Prioritized slotted-Circus. | Pawel Gancarski, Andrew Butterfield |
| 2009 | FM | The Denotational Semantics of slotted-Circus. | Pawel Gancarski, Andrew Butterfield |
| 2009 | SIN | Weakening the Dolev-Yao model through probability. | Riccardo Bresciani, Andrew Butterfield |
| 2009 | TASE | State Visibility and Communication in Unifying Theories of Programming. | Andrew Butterfield, Pawel Gancarski, Jim Woodcock |
| 2008 | ICECCS | POSIX and the Verification Grand Challenge: A Roadmap. | Leo Freitas, Jim Woodcock, Andrew Butterfield |
| 2007 | ICECCS | Formalising Flash Memory: First Steps. | Andrew Butterfield, Jim Woodcock |
| 2007 | IFM | Slotted-Circus. | Andrew Butterfield, Adnan Sherif, Jim Woodcock |
| 2006 | ICFP | Modelling deterministic concurrent I/O. | Malcolm Dowse, Andrew Butterfield |
| 2006 | ICTAC | A Lattice-Theoretic Model for an Algebra of Communicating Sequential Processes. | Malcolm Tyrrell, Joseph M. Morris, Andrew Butterfield, Arthur Hughes |
| 1993 | FM | A VDM Study of Fault-Tolerant Stable Storage - Towards a Computer Engineering Mathematics. | Andrew Butterfield |