| 2026 | ESOP | Rely-Guarantee Is Coinductive - - A Proof-Centered Investigation of Inductively Approximated Coinduction -. | John Derrick, Chelsea Edmonds, Andrei Popescu, Jamie Wright |
| 2025 | IFM | Model Checking Buffered Durable Linearizability in CSP. | Chelsea Edmonds, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim |
| 2024 | VMCAI | A Fully Verified Persistency Library. | Stefan Bodenmller, John Derrick, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim |
| 2020 | FORTE | Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. | Eleni Bila, Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim |
| 2019 | FM | Verifying Correctness of Persistent Concurrent Data Structures. | John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, Heike Wehrheim |
| 2019 | PPoPP | Verifying C11 programs operationally. | Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick |
| 2019 | SEFM | Incorporating Data into EFSM Inference. | Michael Foster, Achim D. Brucker, Ramsay G. Taylor, Siobhn North, John Derrick |
| 2018 | ICFEM | Formalising Extended Finite State Machine Transition Merging. | Michael Foster, Ramsay G. Taylor, Achim D. Brucker, John Derrick |
| 2018 | IFM | Making Linearizability Compositional for Partially Ordered Executions. | Simon Doherty, Brijesh Dongol, Heike Wehrheim, John Derrick |
| 2018 | TASE | Observational Models for Linearizability Checking on Weak Memory Models. | Kirsten Winter, Graeme Smith, John Derrick |
| 2017 | FORTE | An Observational Approach to Defining Linearizability on Weak Memory Models. | John Derrick, Graeme Smith |
| 2016 | OPODIS | Proving Opacity of a Pessimistic STM. | Simon Doherty, Brijesh Dongol, John Derrick, Gerhard Schellhorn, Heike Wehrheim |
| 2016 | PDP | Choreography-Based Analysis of Distributed Message Passing Programs. | Ramsay Taylor, Emilio Tuosto, Neil Walkinshaw, John Derrick |
| 2016 | SAC | Invariant generation for linearizability proofs. | Graeme Smith, John Derrick |
| 2016 | SEFM | Linearizability and Causality. | Simon Doherty, John Derrick |
| 2015 | ECOOP | Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. | Brijesh Dongol, John Derrick, Lindsay Groves, Graeme Smith |
| 2015 | FM | Verifying Opacity of a Transactional Mutex Lock. | John Derrick, Brijesh Dongol, Gerhard Schellhorn, Oleg Travkin, Heike Wehrheim |
| 2015 | FM | A Framework for Correctness Criteria on Weak Memory Models. | John Derrick, Graeme Smith |
| 2014 | FM | Quiescent Consistency: Defining and Verifying Relaxed Linearizability. | John Derrick, Brijesh Dongol, Gerhard Schellhorn, Bogdan Tofan, Oleg Travkin, Heike Wehrheim |
| 2014 | ICTAC | Reasoning Algebraically About Refinement on TSO Architectures. | Brijesh Dongol, John Derrick, Graeme Smith |
| 2014 | IFM | Verifying Linearizability on TSO Architectures. | John Derrick, Graeme Smith, Brijesh Dongol |
| 2013 | ICTAC | A High-Level Semantics for Program Execution under Total Store Order Memory. | Brijesh Dongol, Oleg Travkin, John Derrick, Heike Wehrheim |
| 2013 | IFM | Automatic Inference of Erlang Module Behaviour. | Ramsay Taylor, Kirill Bogdanov, John Derrick |
| 2012 | CAV | How to Prove Algorithms Linearisable. | Gerhard Schellhorn, Heike Wehrheim, John Derrick |
| 2011 | FM | Verifying Linearisability with Potential Linearisation Points. | John Derrick, Gerhard Schellhorn, Heike Wehrheim |
| 2011 | FORTE | Relational Concurrent Refinement: Timed Refinement. | John Derrick, Eerke A. Boiten |
| 2009 | FM | Iterative Refinement of Reverse-Engineered Models by Model-Based Testing. | Neil Walkinshaw, John Derrick, Qiang Guo |
| 2009 | IFM | Modelling Divergence in Relational Concurrent Refinement. | Eerke A. Boiten, John Derrick |
| 2008 | FORTE | Verifying Erlang Telecommunication Systems with the Process Algebra CRL. | Qiang Guo, John Derrick, Csaba Hoch |
| 2007 | IFM | Proving Linearizability Via Non-atomic Refinement. | John Derrick, Gerhard Schellhorn, Heike Wehrheim |
| 2006 | ICFEM | Issues in Implementing a Model Checker for Z. | John Derrick, Siobhn North, Tony Simons |
| 2006 | SEFM | Filtering Retrenchments into Refinements. | Richard Banach, John Derrick |
| 2003 | EDOC | Addressing Computational Viewpoint Design. | David H. Akehurst, John Derrick, A. Gill Waters |
| 2002 | FM | Verifying Erlang Code: A Resource Locker Case-Study. | Thomas Arts, Clara Benac Earle, John Derrick |
| 2002 | ICFEM | A UML Approach to the Design of Open Distributed Systems. | Behzad Bordbar, John Derrick, A. Gill Waters |
| 2002 | ICFEM | Abstract Specification in Object-Z and CSP. | Graeme Smith, John Derrick |
| 2000 | ICFEM | A Case Study in Partial Specification: Consistency and Refinement for Object-Z. | Chris Taylor, John Derrick, Eerke A. Boiten |
| 2000 | IFM | Specification and Analysis of Automata-Based Designs. | Jeremy W. Bryans, Lynne Blair, Howard Bowman, John Derrick |
| 2000 | IFM | Structural Refinement in Object-Z/CSP. | John Derrick, Graeme Smith |
| 2000 | MPC | Liberating Data Refinement. | Eerke A. Boiten, John Derrick |
| 1999 | EDOC | Formalising ODP enterprise policies. | Maarten W. A. Steen, John Derrick |
| 1999 | FM | Non-atomic Refinement in Z. | John Derrick, Eerke A. Boiten |
| 1999 | IFM | Specifying Component and Context Specification Using Promotion. | John Derrick, Eerke A. Boiten |
| 1997 | FM | Viewpoint Consistency in Z and LOTOS: A Case Study. | Eerke A. Boiten, Howard Bowman, John Derrick, Maarten Steen |
| 1997 | FORTE | Disjunction of LOTOS Specifications. | Maarten Steen, Howard Bowman, John Derrick, Eerke A. Boiten |
| 1997 | ICFEM | Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP. | Graeme Smith, John Derrick |
| 1997 | IM | Formal Specification and Testing of a Management Architecture. | G. P. A. Fernandes, John Derrick |
| 1996 | FM | Consistency and Refinement for Partial Specification in Z. | Eerke A. Boiten, John Derrick, Howard Bowman, Maarten Steen |
| 1996 | FORTE | Comparing LOTOS and Z Refinement Relations. | John Derrick, Howard Bowman, Eerke A. Boiten, Maarten Steen |
| 1995 | IM | Formal description techniques for object management. | John Derrick, Peter F. Linington, Simon J. Thompson |
| 1995 | SAC | Modelling distributed systems using Z. | Howard Bowman, John Derrick |
| 1994 | PODC | Consistency and Conformance in ODP (Abstract). | Howard Bowman, John Derrick |
| 1994 | PODC | Modelling Garbage Collection Algorithms Using CCS and Temporal Logic (Abstract). | Howard Bowman, John Derrick, Richard E. Jones |