John Derrick

Orcid: 0000-0002-6631-8914

According to our database1, John Derrick authored at least 174 papers between 1968 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2024
A Fully Verified Persistency Library.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2024

2022
Modularising Verification Of Durable Opacity.
Log. Methods Comput. Sci., 2022

2021
Verifying correctness of persistent concurrent data structures: a sound and complete method.
Formal Aspects Comput., 2021

On Strong Observational Refinement and Forward Simulation.
CoRR, 2021

Brief Announcement: On Strong Observational Refinement and Forward Simulation.
Proceedings of the 35th International Symposium on Distributed Computing, 2021

Reverse-Engineering EFSMs with Data Dependencies.
Proceedings of the Testing Software and Systems, 2021

2020
A Formal Model of Extended Finite State Machines.
Arch. Formal Proofs, 2020

Inference of Extended Finite State Machines.
Arch. Formal Proofs, 2020

Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory.
Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2020

2019
Modelling concurrent objects running on the TSO and ARMv8 memory models.
Sci. Comput. Program., 2019

Incorporating Data into EFSM Inference.
Proceedings of the Software Engineering and Formal Methods - 17th International Conference, 2019

Verifying C11 programs operationally.
Proceedings of the 24th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2019

Verifying Correctness of Persistent Concurrent Data Structures.
Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

2018
Mechanized proofs of opacity: a comparison of two techniques.
Formal Aspects Comput., 2018

Causal Linearizability: Compositionality for Partially Ordered Executions.
CoRR, 2018

Brief Announcement: Generalising Concurrent Correctness to Weak Memory.
Proceedings of the 32nd International Symposium on Distributed Computing, 2018

Observational Models for Linearizability Checking on Weak Memory Models.
Proceedings of the 2018 International Symposium on Theoretical Aspects of Software Engineering, 2018

Making Linearizability Compositional for Partially Ordered Executions.
Proceedings of the Integrated Formal Methods - 14th International Conference, 2018

Formalising Extended Finite State Machine Transition Merging.
Proceedings of the Formal Methods and Software Engineering, 2018

2017
An Observational Approach to Defining Linearizability on Weak Memory Models.
Proceedings of the Formal Techniques for Distributed Objects, Components, and Systems, 2017

A Proof Method for Linearizability on TSO Architectures.
Proceedings of the Provably Correct Systems, 2017

2016
Inferring extended finite state machine models from software executions.
Empir. Softw. Eng., 2016

Causal Linearizability.
CoRR, 2016

Linearizability and Causality.
Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Invariant generation for linearizability proofs.
Proceedings of the 31st Annual ACM Symposium on Applied Computing, 2016

Choreography-Based Analysis of Distributed Message Passing Programs.
Proceedings of the 24th Euromicro International Conference on Parallel, 2016

Proving Opacity of a Pessimistic STM.
Proceedings of the 20th International Conference on Principles of Distributed Systems, 2016

Relational Concurrent Refinement - Partial and Total Frameworks.
Proceedings of the From Action Systems to Distributed Systems - The Refinement Approach., 2016

2015
Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems.
Sci. Comput. Program., 2015

Verifying Linearisability: A Comparative Survey.
ACM Comput. Surv., 2015

mu2: A Refactoring-Based Mutation Testing Framework for Erlang.
Proceedings of the Testing Software and Systems, 2015

A Framework for Correctness Criteria on Weak Memory Models.
Proceedings of the FM 2015: Formal Methods, 2015

Verifying Opacity of a Transactional Mutex Lock.
Proceedings of the FM 2015: Formal Methods, 2015

Smother: an MC/DC analysis tool for Erlang.
Proceedings of the 14th ACM SIGPLAN Workshop on Erlang 2015, 2015

Defining Correctness Conditions for Concurrent Objects in Multicore Architectures.
Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014
A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures.
ACM Trans. Comput. Log., 2014

Deriving real-time action systems with multiple time bands using algebraic reasoning.
Sci. Comput. Program., 2014

Relational concurrent refinement part III: traces, partial relations and automata.
Formal Aspects Comput., 2014

Editorial.
Formal Aspects Comput., 2014

Verifying linearizability: A comparative survey.
CoRR, 2014

Verifying Linearizability on TSO Architectures.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Reasoning Algebraically About Refinement on TSO Architectures.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

Using Coarse-Grained Abstractions to Verify Linearizability on TSO Architectures.
Proceedings of the Hardware and Software: Verification and Testing, 2014

Quiescent Consistency: Defining and Verifying Relaxed Linearizability.
Proceedings of the FM 2014: Formal Methods, 2014

Admit Your Weakness: Verifying Correctness on TSO Architectures.
Proceedings of the Formal Aspects of Component Software - 11th International Symposium, 2014

Synapse: automatic behaviour inference and implementation comparison for Erlang.
Proceedings of the Thirteenth ACM SIGPLAN workshop on Erlang, 2014

Refinement in Z and Object-Z - Foundations and Advanced Applications (2. ed.).
Springer, ISBN: 978-1-4471-5354-2, 2014

2013
Simplifying proofs of linearisability using layers of abstraction.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013

From ODP viewpoint consistency to Integrated Formal Methods.
Comput. Stand. Interfaces, 2013

Data refinement for true concurrency
Proceedings of the Proceedings 16th International Refinement Workshop, 2013

Automatic Inference of Erlang Module Behaviour.
Proceedings of the Integrated Formal Methods, 10th International Conference, 2013

A High-Level Semantics for Program Execution under Total Store Order Memory.
Proceedings of the Theoretical Aspects of Computing - ICTAC 2013, 2013

2012
Temporal-logic property preservation under Z refinement.
Formal Aspects Comput., 2012

Editorial.
Formal Aspects Comput., 2012

Fractional Permissions and Non-Deterministic Evaluators in Interval Temporal Logic.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012

Proving linearisability via coarse-grained abstraction
CoRR, 2012

Using Behaviour Inference to Optimise Regression Test Sets.
Proceedings of the Testing Software and Systems, 2012

How to Prove Algorithms Linearisable.
Proceedings of the Computer Aided Verification - 24th International Conference, 2012

2011
Mechanically verified proof obligations for linearizability.
ACM Trans. Program. Lang. Syst., 2011

Formally based tool support for model checking Erlang applications.
Int. J. Softw. Tools Technol. Transf., 2011

Selected papers of the Refinement Workshop Turku (2008).
Sci. Comput. Program., 2011

Z2SAL: a translation-based model checker for Z.
Formal Aspects Comput., 2011

Building a refinement checker for Z
Proceedings of the Proceedings 15th International Refinement Workshop, 2011

Relational Concurrent Refinement: Timed Refinement.
Proceedings of the Formal Techniques for Distributed Systems, 2011

Verifying Linearisability with Potential Linearisation Points.
Proceedings of the FM 2011: Formal Methods, 2011

2010
Model transformations across views.
Sci. Comput. Program., 2010

Incompleteness of relational simulations in the blocking paradigm.
Sci. Comput. Program., 2010

Editorial.
Formal Aspects Comput., 2010

Model-Checking Erlang - A Comparison between EtomCRL2 and McErlang.
Proceedings of the Testing, 2010

Increasing Functional Coverage by Inductive Testing: A Case Study.
Proceedings of the Testing Software and Systems, 2010

2009
Relational concurrent refinement part II: Internal operations and outputs.
Formal Aspects Comput., 2009

Relational Concurrent Refinement: Automata.
Proceedings of the 14th BCS-FACS Refinement Workshop, 2009

Preface.
Proceedings of the 14th BCS-FACS Refinement Workshop, 2009

Using formal specifications to support testing.
ACM Comput. Surv., 2009

Applying Testability Transformations to Achieve Structural Coverage of Erlang Programs.
Proceedings of the Testing of Software and Communication Systems, 2009

Modelling Divergence in Relational Concurrent Refinement.
Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

Incrementally Discovering Testable Specifications from Program Executions.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Property-Based Testing - The ProTest Project.
Proceedings of the Formal Methods for Components and Objects - 8th International Symposium, 2009

Iterative Refinement of Reverse-Engineered Models by Model-Based Testing.
Proceedings of the FM 2009: Formal Methods, 2009

2008
More Relational Concurrent Refinement: Traces and Partial Relations.
Proceedings of the 13th BAC-FACS Refinement Workshop, 2008

Preface.
Proceedings of the 13th BAC-FACS Refinement Workshop, 2008

Verifying Erlang Telecommunication Systems with the Process Algebra µCRL.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008

Mechanizing a Correctness Proof for a Lock-Free Concurrent Stack.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2008

Z2SAL - Building a Model Checker for Z.
Proceedings of the Abstract State Machines, B and Z, First International Conference, 2008

2007
Using Model Checking to Automatically Find Retrieve Relations.
Proceedings of the BCS-FACS Refinement Workshop, 2007

Preface.
Proceedings of the BCS-FACS Refinement Workshop, 2007

On using data abstractions for model checking refinements.
Acta Informatica, 2007

Proving Linearizability Via Non-atomic Refinement.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007

Verification of timed Erlang/OTP components using the process algebra mucrl.
Proceedings of the 2007 ACM SIGPLAN Workshop on Erlang, Freiburg, Germany, October 5, 2007, 2007

2006
Verifying data refinements using a model checker.
Formal Aspects Comput., 2006

Guest Editorial.
Formal Aspects Comput., 2006

Relational Concurrent Refinement with Internal Operations.
Proceedings of the 11th Refinement Workshop, 2006

Preface.
Proceedings of the 11th Refinement Workshop, 2006

Filtering Retrenchments into Refinements.
Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2006), 2006

Issues in Implementing a Model Checker for Z.
Proceedings of the Formal Methods and Software Engineering, 2006

Model Transformations Incorporating Multiple Views.
Proceedings of the Algebraic Methodology and Software Technology, 2006

2005
Introduction.
Softw. Syst. Model., 2005

Guest Editorial Integrated Formal Methods.
Formal Aspects Comput., 2005

Model Checking Downward Simulations.
Proceedings of the REFINE 2005 Workshop, 2005

Preface.
Proceedings of the REFINE 2005 Workshop, 2005

Non-atomic Refinement in Z and CSP.
Proceedings of the ZB 2005: Formal Specification and Development in Z and B, 2005

Formal Program Development with Approximations.
Proceedings of the ZB 2005: Formal Specification and Development in Z and B, 2005

Verifying fault-tolerant Erlang programs.
Proceedings of the 2005 ACM SIGPLAN Workshop on Erlang, Tallinn, 2005

2004
Development of a verified Erlang program for resource locking.
Int. J. Softw. Tools Technol. Transf., 2004

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

Linear Temporal Logic and Z Refinement.
Proceedings of the Algebraic Methodology and Software Technology, 2004

2003
Model checking stochastic automata.
ACM Trans. Comput. Log., 2003

A Relational Framework for the Integration of Specifications.
Trans. SDPS, 2003

Structural Refinement of Systems Specified in Object-Z and CSP.
Formal Aspects Comput., 2003

Relational Concurrent Refinement.
Formal Aspects Comput., 2003

Using Coupled Simulations in Non-atomic Refinement.
Proceedings of the ZB 2003: Formal Specification and Development in Z and B, 2003

Timed CSP and Object-Z.
Proceedings of the ZB 2003: Formal Specification and Development in Z and B, 2003

Design and Verification of Distributed Multi-media Systems.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 2003

Addressing Computational Viewpoint Design.
Proceedings of the 7th International Enterprise Distributed Object Computing Conference (EDOC 2003), 2003

Recent Advances in Refinement.
Proceedings of the Abstract State Machines, 2003

2002
ODP computational-to-information viewpoint mappings: a translation of CORBA IDL to Z.
IEE Proc. Softw., 2002

A Formal Framework for Viewpoint Consistency.
Formal Methods Syst. Des., 2002

Combining Component Specifications in Object-Z and CSP.
Formal Aspects Comput., 2002

Preface.
Proceedings of the BCS FACS Refinement Workshop 2002, 2002

Unifying concurrent and relational refinement.
Proceedings of the BCS FACS Refinement Workshop 2002, 2002

Using UML to specify QoS constraints in ODP.
Comput. Networks, 2002

Handling Inconsistencies in Z Using Quasi-Classical Logic.
Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

Abstract Specification in Object-Z and CSP.
Proceedings of the Formal Methods and Software Engineering, 2002

A UML Approach to the Design of Open Distributed Systems.
Proceedings of the Formal Methods and Software Engineering, 2002

Interpreting ODP Viewpoint Specification: Observations from a Case Study.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems V, 2002

Verifying Erlang Code: A Resource Locker Case-Study.
Proceedings of the FME 2002: Formal Methods, 2002

2001
Specification, Refinement and Verification of Concurrent Systems-An Integration of Object-Z and CSP.
Formal Methods Syst. Des., 2001

Analysis of a Multimedia Stream using Stochastic Process Algebra.
Comput. J., 2001

Author Obliged to Submit Paper before 4 July: Policies in an Enterprise Specification.
Proceedings of the Policies for Distributed Systems and Networks, 2001

2000
Guest Editors' Introduction: Formal Methods for Object Oriented Distributed Systems.
IEEE Trans. Software Eng., 2000

Editorial: special issue on specification-based testing.
Softw. Test. Verification Reliab., 2000

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

A single complete refinement rule for Z.
J. Log. Comput., 2000

Teaching Communication Protocols.
Comput. Sci. Educ., 2000

Stochastic Model Checking for Multimedia
CoRR, 2000

Viewpoint consistency in ODP.
Comput. Networks, 2000

Guards, Preconditions, and Refinement in Z.
Proceedings of the ZB 2000: Formal Specification and Development in Z and B, First International Conference of B and Z Users, York, UK, August 29, 2000

Liberating Data Refinement.
Proceedings of the Mathematics of Program Construction, 5th International Conference, 2000

Structural Refinement in Object-Z/CSP.
Proceedings of the Integrated Formal Methods, Second International Conference, 2000

Specification and Analysis of Automata-Based Designs.
Proceedings of the Integrated Formal Methods, Second International Conference, 2000

A Case Study in Partial Specification: Consistency and Refinement for Object-Z.
Proceedings of the 3rd IEEE International Conference on Formal Engineering Methods, 2000

Refinement of objects and operations in Object-Z.
Proceedings of the Formal Methods for Open Object-Based Distributed Systems IV, 2000

1999
Testing Refinements of State-based Formal Specifications.
Softw. Test. Verification Reliab., 1999

Strategies for Consistency Checking Based on Unification.
Sci. Comput. Program., 1999

Constructive Consistency Checking for Partial Specification in Z.
Sci. Comput. Program., 1999

Calculating upward and downward simulations of state-based specifications.
Inf. Softw. Technol., 1999

Stochastic Specification and Verification.
Proceedings of the 3rd Irish Workshop on Formal Methods, Galway, Ireland, July 1999, 1999

Specifying Component and Context Specification Using Promotion.
Proceedings of the Integrated Formal Methods, 1999

A Junction between State Based and Behavioural Specification (Invited Talk).
Proceedings of the Formal Methods for Open Object-Based Distributed Systems, 1999

Non-atomic Refinement in Z.
Proceedings of the FM'99 - Formal Methods, 1999

Formalising ODP enterprise policies.
Proceedings of the Third International Enterprise Distributed Object Computing Conference, 1999

1998
Constraint-oriented style for object-oriented formal specification.
IEE Proc. Softw., 1998

Specifying and Refining Internal Operations in Z.
Formal Aspects Comput., 1998

Testing Refinements by Refining Tests.
Proceedings of the ZUM '98: The Z Formal Specification Notation, 1998

Consistency of Partial Process Specifications.
Proceedings of the Algebraic Methodology and Software Technology, 1998

1997
Weak Refinement in Z.
Proceedings of the ZUM '97: The Z Formal Specification Notation, 1997

Formal Specification and Testing of a Management Architecture.
Proceedings of the Integrated Network Management V, 1997

Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP.
Proceedings of the First IEEE International Conference on Formal Engineering Methods, 1997

Disjunction of LOTOS Specifications.
Proceedings of the Formal Description Techniques and Protocol Specification, 1997

Viewpoint Consistency in Z and LOTOS: A Case Study.
Proceedings of the FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, 1997

Extending LOTOS with Time: A True Concurrency Perspective.
Proceedings of the Transformation-Based Reactive Systems Development, 1997

1996
Cross-viewpoint consistency in open distributed processing.
Softw. Eng. J., 1996

Issues in multiparadigm viewpoint specification.
Proceedings of the Joint Proceedings of the Second International Software Architecture Workshop (ISAW-2) and International Workshop on Multiple Perspectives in Software Development (Viewpoints '96) on SIGSOFT '96 workshops, 1996

Comparing LOTOS and Z Refinement Relations.
Proceedings of the Formal Description Techniques IX: Theory, 1996

Consistency and Refinement for Partial Specification in Z.
Proceedings of the FME '96: Industrial Benefit and Advances in Formal Methods, 1996

1995
Viewpoints and Objects.
Proceedings of the ZUM '95: The Z Formal Specification Notation, 1995

Modelling distributed systems using Z.
Proceedings of the 1995 ACM symposium on applied computing, 1995

Composition of LOTOS specifications.
Proceedings of the Protocol Specification, 1995

A True Concurrency Semantics for Quality of Service Specification and Validation.
Proceedings of the International Conference on Multimedia Networking, 1995

Formal description techniques for object management.
Proceedings of the Integrated Network Management IV, 1995

1994
Modelling Garbage Collection Algorithms Using CCS and Temporal Logic (Abstract).
Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, 1994

Consistency and Conformance in ODP (Abstract).
Proceedings of the Thirteenth Annual ACM Symposium on Principles of Distributed Computing, 1994

1974
Meeting of the Association for Symbolic Logic: Orleans, France, 1972.
J. Symb. Log., 1974

1968
Meeting of the Association for Symbolic Logic Leeds 1967.
J. Symb. Log., 1968


  Loading...