Meeting of the Association for Symbolic Logic Leeds 1967. - M. H. Lob; F. R. Drake; John Derrick (J. Symb. Log., 1968)

Meeting of the Association for Symbolic Logic: Orleans, France, 1972. - J. P. Calais; John Derrick; Gabriel Sabbagh (J. Symb. Log., 1974)

Consistency and Conformance in ODP (Abstract). - Howard Bowman; John Derrick (PODC, 1994)

Modelling Garbage Collection Algorithms Using CCS and Temporal Logic (Abstract). - Howard Bowman; John Derrick; Richard E. Jones (PODC, 1994)

Formal description techniques for object management. - John Derrick; Peter F. Linington; Simon J. Thompson (Integrated Network Management, 1995)

A True Concurrency Semantics for Quality of Service Specification and Validation. - Howard Bowman; John Derrick (MMNET, 1995)

Composition of LOTOS specifications. - Maarten Steen; Howard Bowman; John Derrick (PSTV, 1995)

Modelling distributed systems using Z. - Howard Bowman; John Derrick (SAC, 1995)

Viewpoints and Objects. - Howard Bowman; John Derrick; Maarten Steen (ZUM, 1995)

Consistency and Refinement for Partial Specification in Z. - Eerke A. Boiten; John Derrick; Howard Bowman; Maarten Steen (FME, 1996)

Comparing LOTOS and Z Refinement Relations. - John Derrick; Howard Bowman; Eerke A. Boiten; Maarten Steen (FORTE, 1996)

Issues in multiparadigm viewpoint specification. - Eerke A. Boiten; Howard Bowman; John Derrick; Maarten Steen (ISAW/Viewpoints@FSE, 1996)

Cross-viewpoint consistency in open distributed processing. - Howard Bowman; John Derrick; Peter W. A. Linington; Maarten W. A. Steen (Softw. Eng. J., 1996)

Extending LOTOS with Time: A True Concurrency Perspective. - Howard Bowman; John Derrick (ARTS, 1997)

Viewpoint Consistency in Z and LOTOS: A Case Study. - Eerke A. Boiten; Howard Bowman; John Derrick; Maarten Steen (FME, 1997)

Disjunction of LOTOS Specifications. - Maarten Steen; Howard Bowman; John Derrick; Eerke A. Boiten (FORTE, 1997)

Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP. - Graeme Smith 001; John Derrick (ICFEM, 1997)

Formal Specification and Testing of a Management Architecture. - G. P. A. Fernandes; John Derrick (Integrated Network Management, 1997)

Weak Refinement in Z. - John Derrick; Eerke A. Boiten; Howard Bowman; Maarten Steen (ZUM, 1997)

Consistency of Partial Process Specifications. - Maarten Steen; John Derrick; Eerke A. Boiten; Howard Bowman (AMAST, 1998)

Testing Refinements by Refining Tests. - John Derrick; Eerke A. Boiten (ZUM, 1998)

Specifying and Refining Internal Operations in Z. - John Derrick; Eerke A. Boiten; Howard Bowman; Maarten Steen (Formal Aspects Comput., 1998)

Constraint-oriented style for object-oriented formal specification. - Tommaso Bolognesi; John Derrick (IEE Proc. Softw., 1998)

Formalising ODP enterprise policies. - Maarten W. A. Steen; John Derrick (EDOC, 1999)

Non-atomic Refinement in Z. - John Derrick; Eerke A. Boiten (World Congress on Formal Methods, 1999)

A Junction between State Based and Behavioural Specification (Invited Talk). - Howard Bowman; John Derrick (FMOODS, 1999)

Specifying Component and Context Specification Using Promotion. - John Derrick; Eerke A. Boiten (IFM, 1999)

Stochastic Specification and Verification. - Jeremy W. Bryans; John Derrick (IWFM, 1999)

Calculating upward and downward simulations of state-based specifications. - John Derrick; Eerke A. Boiten (Inf. Softw. Technol., 1999)

Constructive Consistency Checking for Partial Specification in Z. - Eerke A. Boiten; John Derrick; Howard Bowman; Maarten Steen (Sci. Comput. Program., 1999)

Strategies for Consistency Checking Based on Unification. - Howard Bowman; Eerke A. Boiten; John Derrick; Maarten Steen (Sci. Comput. Program., 1999)

Testing Refinements of State-based Formal Specifications. - John Derrick; Eerke A. Boiten (Softw. Test. Verification Reliab., 1999)

Refinement of objects and operations in Object-Z. - John Derrick; Eerke A. Boiten (FMOODS, 2000)

A Case Study in Partial Specification: Consistency and Refinement for Object-Z. - Chris Taylor; John Derrick; Eerke A. Boiten (ICFEM, 2000)

Specification and Analysis of Automata-Based Designs. - Jeremy W. Bryans; Lynne Blair; Howard Bowman; John Derrick (IFM, 2000)

Structural Refinement in Object-Z/CSP. - John Derrick; Graeme Smith 001 (IFM, 2000)

Liberating Data Refinement. - Eerke A. Boiten; John Derrick (MPC, 2000)

Guards, Preconditions, and Refinement in Z. - Ralph Miarka; Eerke A. Boiten; John Derrick (ZB, 2000)

Viewpoint consistency in ODP. - Eerke A. Boiten; Howard Bowman; John Derrick; Peter F. Linington; Maarten Steen (Comput. Networks, 2000)

Stochastic Model Checking for Multimedia - Jeremy W. Bryans; Howard Bowman; John Derrick (CoRR, 2000)

Teaching Communication Protocols. - John Derrick; Sally Fincher (Comput. Sci. Educ., 2000)

A single complete refinement rule for Z. - John Derrick (J. Log. Comput., 2000)

Concurrent and Real-Time Systems: The CSP Approach, Steve Schneider, Wiley, 2000 (Book Review). - John Derrick (Softw. Test. Verification Reliab., 2000)

Editorial: special issue on specification-based testing. - Robert M. Hierons; John Derrick (Softw. Test. Verification Reliab., 2000)

Guest Editors' Introduction: Formal Methods for Object Oriented Distributed Systems. - Howard Bowman; John Derrick; Ed Brinksma (IEEE Trans. Software Eng., 2000)

Author Obliged to Submit Paper before 4 July: Policies in an Enterprise Specification. - James B. Cole; John Derrick; Zoran Milosevic; Kerry Raymond (POLICY, 2001)

Analysis of a Multimedia Stream using Stochastic Process Algebra. - Howard Bowman; Jeremy W. Bryans; John Derrick (Comput. J., 2001)

Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP. - Graeme Smith 001; John Derrick (Formal Methods Syst. Des., 2001)

Verifying Erlang Code: A Resource Locker Case-Study. - Thomas Arts; Clara Benac Earle; John Derrick (FME, 2002)

Interpreting ODP Viewpoint Specification: Observations from a Case Study. - Chris Taylor; Eerke A. Boiten; John Derrick (FMOODS, 2002)

A UML Approach to the Design of Open Distributed Systems. - Behzad Bordbar; John Derrick; A. Gill Waters (ICFEM, 2002)

Abstract Specification in Object-Z and CSP. - Graeme Smith 001; John Derrick (ICFEM, 2002)

Handling Inconsistencies in Z Using Quasi-Classical Logic. - Ralph Miarka; John Derrick; Eerke A. Boiten (ZB, 2002)

Using UML to specify QoS constraints in ODP. - Behzad Bordbar; John Derrick; A. Gill Waters (Comput. Networks, 2002)

Unifying concurrent and relational refinement. - Eerke A. Boiten; John Derrick (Refine, 2002)

Preface. - John Derrick; Eerke A. Boiten; Jim Woodcock 001; Joakim von Wright (Refine, 2002)

Combining Component Specifications in Object-Z and CSP. - John Derrick; Eerke A. Boiten (Formal Aspects Comput., 2002)

A Formal Framework for Viewpoint Consistency. - Howard Bowman; Maarten Steen; Eerke A. Boiten; John Derrick (Formal Methods Syst. Des., 2002)

ODP computational-to-information viewpoint mappings: a translation of CORBA IDL to Z. - Chris Taylor; Eerke A. Boiten; John Derrick (IEE Proc. Softw., 2002)

Recent Advances in Refinement. - John Derrick; Eerke A. Boiten (Abstract State Machines, 2003)

Addressing Computational Viewpoint Design. - David H. Akehurst; John Derrick; A. Gill Waters (EDOC, 2003)

Design and Verification of Distributed Multi-media Systems. - David H. Akehurst; John Derrick; A. Gill Waters (FMOODS, 2003)

Timed CSP and Object-Z. - John Derrick (ZB, 2003)

Using Coupled Simulations in Non-atomic Refinement. - John Derrick; Heike Wehrheim (ZB, 2003)

Relational Concurrent Refinement. - John Derrick; Eerke A. Boiten (Formal Aspects Comput., 2003)

Structural Refinement of Systems Specified in Object-Z and CSP. - John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2003)

A Relational Framework for the Integration of Specifications. - Eerke A. Boiten; John Derrick (Trans. SDPS, 2003)

Model checking stochastic automata. - Jeremy W. Bryans; Howard Bowman; John Derrick (ACM Trans. Comput. Log., 2003)

Linear Temporal Logic and Z Refinement. - John Derrick; Graeme Smith 001 (AMAST, 2004)

Programming Methodology A. McIver and C. Morgan, editors, Springer-Verlag, 2002. - John Derrick (J. Funct. Program., 2004)

Development of a verified Erlang program for resource locking. - Thomas Arts; Clara Benac Earle; John Derrick (Int. J. Softw. Tools Technol. Transf., 2004)

Verifying fault-tolerant Erlang programs. - Clara Benac Earle; Lars-Åke Fredlund; John Derrick (Erlang Workshop, 2005)

Formal Program Development with Approximations. - Eerke A. Boiten; John Derrick (ZB, 2005)

Non-atomic Refinement in Z and CSP. - John Derrick; Heike Wehrheim (ZB, 2005)

Preface. - John Derrick; Eerke A. Boiten (REFINE, 2005)

Model Checking Downward Simulations. - Graeme Smith 001; John Derrick (REFINE, 2005)

Guest Editorial Integrated Formal Methods. - Eerke A. Boiten; John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2005)

Introduction. - Tommaso Bolognesi; John Derrick (Softw. Syst. Model., 2005)

Model Transformations Incorporating Multiple Views. - John Derrick; Heike Wehrheim (AMAST, 2006)

Issues in Implementing a Model Checker for Z. - John Derrick; Siobhán North; Tony Simons 001 (ICFEM, 2006)

Filtering Retrenchments into Refinements. - Richard Banach; John Derrick (SEFM, 2006)

Preface. - Bernhard K. Aichernig; Eerke A. Boiten; John Derrick; Lindsay Groves (Refine@ICFEM, 2006)

Relational Concurrent Refinement with Internal Operations. - John Derrick; Eerke A. Boiten (Refine@ICFEM, 2006)

Guest Editorial. - John Derrick; Mark Harman; Robert M. Hierons (Formal Aspects Comput., 2006)

Verifying data refinements using a model checker. - Graeme Smith 001; John Derrick (Formal Aspects Comput., 2006)

Verification of timed Erlang/OTP components using the process algebra mucrl. - Qiang Guo 001; John Derrick (Erlang Workshop, 2007)

Proving Linearizability Via Non-atomic Refinement. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (IFM, 2007)

On using data abstractions for model checking refinements. - John Derrick; Heike Wehrheim (Acta Informatica, 2007)

Preface. - Eerke A. Boiten; John Derrick; Graeme Smith 001 (REFINE@IFM, 2007)

Using Model Checking to Automatically Find Retrieve Relations. - John Derrick; Graeme Smith 001 (REFINE@IFM, 2007)

Z2SAL - Building a Model Checker for Z. - John Derrick; Siobhán North; Anthony J. H. Simons (ABZ, 2008)

Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (FMOODS, 2008)

Verifying Erlang Telecommunication Systems with the Process Algebra µCRL. - Qiang Guo 001; John Derrick; Csaba Hoch (FORTE, 2008)

Preface. - Eerke A. Boiten; John Derrick; Gerhard Schellhorn (Refine@FM, 2008)

More Relational Concurrent Refinement: Traces and Partial Relations. - John Derrick; Eerke A. Boiten (Refine@FM, 2008)

Iterative Refinement of Reverse-Engineered Models by Model-Based Testing. - Neil Walkinshaw; John Derrick; Qiang Guo 001 (FM, 2009)

Property-Based Testing - The ProTest Project. - John Derrick; Neil Walkinshaw; Thomas Arts; Clara Benac Earle; Francesco Cesarini; Lars-Åke Fredlund; Víctor M. Gulías; John Hughes 001; Simon J. Thompson (FMCO, 2009)

Incrementally Discovering Testable Specifications from Program Executions. - Neil Walkinshaw; John Derrick (FMCO, 2009)

Modelling Divergence in Relational Concurrent Refinement. - Eerke A. Boiten; John Derrick (IFM, 2009)

Applying Testability Transformations to Achieve Structural Coverage of Erlang Programs. - Qiang Guo 001; John Derrick; Neil Walkinshaw (TestCom/FATES, 2009)

Using formal specifications to support testing. - Robert M. Hierons; Kirill Bogdanov 002; Jonathan P. Bowen; Rance Cleaveland; John Derrick; Jeremy Dick; Marian Gheorghe 001; Mark Harman; Kalpesh Kapoor; Paul J. Krause; Gerald Lüttgen; Anthony J. H. Simons; et al. (ACM Comput. Surv., 2009)

Preface. - Eerke A. Boiten; John Derrick; Steve Reeves (REFINE@FMWeek, 2009)

Relational Concurrent Refinement: Automata. - John Derrick; Eerke A. Boiten (REFINE@FMWeek, 2009)

Relational concurrent refinement part II: Internal operations and outputs. - Eerke A. Boiten; John Derrick; Gerhard Schellhorn (Formal Aspects Comput., 2009)

Increasing Functional Coverage by Inductive Testing: A Case Study. - Neil Walkinshaw; Kirill Bogdanov 002; John Derrick; Javier París (ICTSS, 2010)

Model-Checking Erlang - A Comparison between EtomCRL2 and McErlang. - Qiang Guo 001; John Derrick; Clara Benac Earle; Lars-Åke Fredlund (TAIC PART, 2010)

Editorial. - Eerke A. Boiten; Michael J. Butler; John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2010)

Incompleteness of relational simulations in the blocking paradigm. - Eerke A. Boiten; John Derrick (Sci. Comput. Program., 2010)

Model transformations across views. - John Derrick; Heike Wehrheim (Sci. Comput. Program., 2010)

Verifying Linearisability with Potential Linearisation Points. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (FM, 2011)

Relational Concurrent Refinement: Timed Refinement. - John Derrick; Eerke A. Boiten (FMOODS/FORTE, 2011)

Building a refinement checker for Z - John Derrick; Siobhán North; Anthony J. H. Simons (Refine@FM, 2011)

Z2SAL: a translation-based model checker for Z. - John Derrick; Siobhán North; Anthony J. H. Simons (Formal Aspects Comput., 2011)

Selected papers of the Refinement Workshop Turku (2008). - Eerke A. Boiten; John Derrick; Gerhard Schellhorn (Sci. Comput. Program., 2011)

Formally based tool support for model checking Erlang applications. - Qiang Guo 001; John Derrick (Int. J. Softw. Tools Technol. Transf., 2011)

Mechanically verified proof obligations for linearizability. - John Derrick; Gerhard Schellhorn; Heike Wehrheim (ACM Trans. Program. Lang. Syst., 2011)

How to Prove Algorithms Linearisable. - Gerhard Schellhorn; Heike Wehrheim; John Derrick (CAV, 2012)

Using Behaviour Inference to Optimise Regression Test Sets. - Ramsay Taylor; Mathew Hall; Kirill Bogdanov 002; John Derrick (ICTSS, 2012)

Proving linearisability via coarse-grained abstraction - Brijesh Dongol; John Derrick (CoRR, 2012)

Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic. - Brijesh Dongol; John Derrick; Ian J. Hayes (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

Editorial. - Eerke A. Boiten; John Derrick; Jin Song Dong; Steve Reeves (Formal Aspects Comput., 2012)

Temporal-logic property preservation under Z refinement. - John Derrick; Graeme Smith 001 (Formal Aspects Comput., 2012)

A High-Level Semantics for Program Execution under Total Store Order Memory. - Brijesh Dongol; Oleg Travkin; John Derrick; Heike Wehrheim (ICTAC, 2013)

Automatic Inference of Erlang Module Behaviour. - Ramsay Taylor; Kirill Bogdanov 002; John Derrick (IFM, 2013)

Data refinement for true concurrency - Brijesh Dongol; John Derrick (Refine@IFM, 2013)

From ODP viewpoint consistency to Integrated Formal Methods. - Eerke A. Boiten; John Derrick (Comput. Stand. Interfaces, 2013)

Simplifying proofs of linearisability using layers of abstraction. - Brijesh Dongol; John Derrick (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Refinement in Z and Object-Z - Foundations and Advanced Applications (2. ed.). - John Derrick; Eerke A. Boiten (Springer, 2014)

Synapse: automatic behaviour inference and implementation comparison for Erlang. - Pablo Lamela Seijas; Simon J. Thompson; Ramsay Taylor; Kirill Bogdanov 002; John Derrick (Erlang Workshop, 2014)

Admit Your Weakness: Verifying Correctness on TSO Architectures. - Graeme Smith 001; John Derrick; Brijesh Dongol (FACS, 2014)

Quiescent Consistency: Defining and Verifying Relaxed Linearizability. - John Derrick; Brijesh Dongol; Gerhard Schellhorn; Bogdan Tofan; Oleg Travkin; Heike Wehrheim (FM, 2014)

Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Lindsay Groves; Brijesh Dongol (Haifa Verification Conference, 2014)

Reasoning Algebraically About Refinement on TSO Architectures. - Brijesh Dongol; John Derrick; Graeme Smith 001 (ICTAC, 2014)

Verifying Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Brijesh Dongol (IFM, 2014)

Verifying linearizability: A comparative survey. - Brijesh Dongol; John Derrick (CoRR, 2014)

Editorial. - Eerke A. Boiten; John Derrick; Steve Reeves (Formal Aspects Comput., 2014)

Relational concurrent refinement part III: traces, partial relations and automata. - John Derrick; Eerke A. Boiten (Formal Aspects Comput., 2014)

Deriving real-time action systems with multiple time bands using algebraic reasoning. - Brijesh Dongol; Ian J. Hayes; John Derrick (Sci. Comput. Program., 2014)

A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. - Gerhard Schellhorn; John Derrick; Heike Wehrheim (ACM Trans. Comput. Log., 2014)

Defining Correctness Conditions for Concurrent Objects in Multicore Architectures. - Brijesh Dongol; John Derrick; Lindsay Groves; Graeme Smith 001 (ECOOP, 2015)

Smother: an MC/DC analysis tool for Erlang. - Ramsay Taylor; John Derrick (Erlang Workshop, 2015)

Verifying Opacity of a Transactional Mutex Lock. - John Derrick; Brijesh Dongol; Gerhard Schellhorn; Oleg Travkin; Heike Wehrheim (FM, 2015)

A Framework for Correctness Criteria on Weak Memory Models. - John Derrick; Graeme Smith 001 (FM, 2015)

mu2: A Refactoring-Based Mutation Testing Framework for Erlang. - Ramsay Taylor; John Derrick (ICTSS, 2015)

Verifying Linearisability: A Comparative Survey. - Brijesh Dongol; John Derrick (ACM Comput. Surv., 2015)

Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. - Brijesh Dongol; John Derrick (Sci. Comput. Program., 2015)

Relational Concurrent Refinement - Partial and Total Frameworks. - John Derrick; Eerke A. Boiten (From Action Systems to Distributed Systems, 2016)

Proving Opacity of a Pessimistic STM. - Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (OPODIS, 2016)

Choreography-Based Analysis of Distributed Message Passing Programs. - Ramsay Taylor; Emilio Tuosto; Neil Walkinshaw; John Derrick (PDP, 2016)

Invariant generation for linearizability proofs. - Graeme Smith 001; John Derrick (SAC, 2016)

Linearizability and Causality. - Simon Doherty; John Derrick (SEFM, 2016)

Causal Linearizability. - Simon Doherty; John Derrick (CoRR, 2016)

Inferring extended finite state machine models from software executions. - Neil Walkinshaw; Ramsay Taylor; John Derrick (Empir. Softw. Eng., 2016)

A Proof Method for Linearizability on TSO Architectures. - John Derrick; Graeme Smith 001; Lindsay Groves; Brijesh Dongol (Provably Correct Systems, 2017)

An Observational Approach to Defining Linearizability on Weak Memory Models. - John Derrick; Graeme Smith 001 (FORTE, 2017)

Formalising Extended Finite State Machine Transition Merging. - Michael Foster 001; Ramsay G. Taylor; Achim D. Brucker; John Derrick (ICFEM, 2018)

Making Linearizability Compositional for Partially Ordered Executions. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (IFM, 2018)

Observational Models for Linearizability Checking on Weak Memory Models. - Kirsten Winter; Graeme Smith 001; John Derrick (TASE, 2018)

Brief Announcement: Generalising Concurrent Correctness to Weak Memory. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (DISC, 2018)

Causal Linearizability: Compositionality for Partially Ordered Executions. - Simon Doherty; John Derrick; Brijesh Dongol; Heike Wehrheim (CoRR, 2018)

Mechanized proofs of opacity: a comparison of two techniques. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Oleg Travkin; Heike Wehrheim (Formal Aspects Comput., 2018)

Verifying Correctness of Persistent Concurrent Data Structures. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (FM, 2019)

Verifying C11 programs operationally. - Simon Doherty; Brijesh Dongol; Heike Wehrheim; John Derrick (PPoPP, 2019)

Incorporating Data into EFSM Inference. - Michael Foster 001; Achim D. Brucker; Ramsay G. Taylor; Siobhán North; John Derrick (SEFM, 2019)

Modelling concurrent objects running on the TSO and ARMv8 memory models. - Kirsten Winter; Graeme Smith 001; John Derrick (Sci. Comput. Program., 2019)

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory. - Eleni Bila; Simon Doherty; Brijesh Dongol; John Derrick; Gerhard Schellhorn; Heike Wehrheim (FORTE, 2020)

Inference of Extended Finite State Machines. - Michael Foster 001; Achim D. Brucker; Ramsay G. Taylor; John Derrick (Arch. Formal Proofs, 2020)

A Formal Model of Extended Finite State Machines. - Michael Foster 001; Achim D. Brucker; Ramsay G. Taylor; John Derrick (Arch. Formal Proofs, 2020)

Reverse-Engineering EFSMs with Data Dependencies. - Michael Foster 001; John Derrick; Neil Walkinshaw (ICTSS, 2021)

Brief Announcement: On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (DISC, 2021)

On Strong Observational Refinement and Forward Simulation. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (CoRR, 2021)

Verifying correctness of persistent concurrent data structures: a sound and complete method. - John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Formal Aspects Comput., 2021)

Modularising Verification Of Durable Opacity. - Eleni Bila; John Derrick; Simon Doherty; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (Log. Methods Comput. Sci., 2022)

A Fully Verified Persistency Library. - Stefan Bodenmüller; John Derrick; Brijesh Dongol; Gerhard Schellhorn; Heike Wehrheim (VMCAI (2), 2024)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)

CSP Artifact for Model Checking Buffered Durable Linearizability. - Chelsea Edmonds; Brijesh Dongol; John Derrick; Heike Wehrheim; Gerhard Schellhorn (Zenodo, 2025)