Professor John Derrick
DPhil
School of Computer Science
Acting Vice-President and Head of Faculty of Science
Professor of Computer Science
Member of the Foundations of Computation and Testing research groups
![Prof. John Derrick profile photo](http://cdn.sheffield.ac.uk/sites/default/files/styles/profile_square_lg_1x/public/2020-09/JD%202.jpg?h=68a695a2&itok=6ttr5RVq)
![Profile picture of Prof. John Derrick profile photo](http://cdn.sheffield.ac.uk/sites/default/files/styles/profile_modal/public/2020-09/JD%202.jpg?h=68a695a2&itok=e9StLokG)
+44 114 222 1849
Full contact details
School of Computer Science
Regent Court (DCS)
211 Portobello
Sheffield
S1 4DP
- Profile
-
John graduated with a degree in Mathematics from the University of Nottingham, before taking his DPhil in Oxford. From 1990 to 2005 he worked at the University of Kent at Canterbury, moving to Sheffield in 2005.
He was Head of Department between 2009 and 2015. In 2015 he was appointed to the post of Deputy PVC for Research and Innovation. Since 2017 he has been Vice President and Head of the Faculty of Science.
- Research interests
-
Specification, refinement and testing using formal methods:
- Refinement in state-based systems.
- Integrated formal methods.
- Viewpoint specification using formal methods.
- Model checking Erlang code.
- Testing of formal specifications.
- Process algebraic refinement.
- Frameworks for distributed systems: architectural semantics, specification templates, object orientation, interfaces.
- Publications
-
Books
- Refinement. Springer International Publishing.
- Formal techniques for networked and distributed systems-- FORTE 2007. Springer-Verlag New York Inc.
- Integrated formal methods. Springer.
- Refinement in Z and Object-Z. Springer London.
- Preface. Elsevier.
Edited books
Journal articles
- Verifying correctness of persistent concurrent data structures: a sound and complete method. Formal Aspects of Computing.
- Modelling concurrent objects running on the TSO and ARMv8 memory models. Science of Computer Programming. View this article in WRRO
- Mechanized proofs of opacity: a comparison of two techniques. Formal Aspects of Computing, 30(5), 597-625. View this article in WRRO
- Inferring extended finite state machine models from software executions. Empirical Software Engineering, 21(3), 811-853. View this article in WRRO
- Interval-based data refinement: A uniform approach to true concurrency in discrete and real-time systems. Science of Computer Programming, 111, 214-247. View this article in WRRO
- Verifying Linearisability. ACM Computing Surveys, 48(2), 1-43.
- A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Transactions on Computational Logic, 15(4), 1-37. View this article in WRRO
- Using coarse-grained abstractions to verify linearizability on TSO architectures. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8855. View this article in WRRO
- Reasoning algebraically about refinement on TSO architectures. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8687, 151-168. View this article in WRRO
- Editorial. Formal Aspects of Computing, 1-1.
- Quiescent consistency: Defining and verifying relaxed linearizability. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8442 LNCS, 200-214.
- Deriving real-time action systems with multiple time bands using algebraic reasoning. Science of Computer Programming.
- How to prove algorithms linearisable. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7358 LNCS, 243-259.
- Relational concurrent refinement part III: traces, partial relations and automata. Formal Aspects of Computing, 1-26.
- Preface to iFM & ABZ 2012. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7316 LNCS.
- Relational concurrent refinement: Timed refinement. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6722 LNCS, 121-137.
- Verifying linearisability with potential linearisation points. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6664 LNCS, 323-337.
- Selected papers of the Refinement Workshop Turku (2008). Science of Computer Programming, 76(9), 737-738.
- Mechanically verified proof obligations for linearizability. ACM Transactions on Programming Languages and Systems, 33(1).
- Estimating the feasibility of transition paths in extended finite state machines. AUTOMAT SOFTW ENG, 17(1), 33-56.
- Incompleteness of relational simulations in the blocking paradigm. SCI COMPUT PROGRAM, 75(12), 1262-1269. View this article in WRRO
- Model transformations across views. SCI COMPUT PROGRAM, 75(3), 192-210.
- Model-checking Erlang - A comparison between EtomCRL2 and McErlang. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6303 LNCS, 23-38.
- Incrementally discovering testable specifications from program executions. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6286 LNCS, 272-289.
- Property-based testing - The ProTest project. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6286 LNCS, 250-271.
- Editorial. FORM ASP COMPUT, 22(1), 1-1.
- Editorial. FORM ASP COMPUT, 21(1-2), 1-1.
- Relational Concurrent Refinement: Automata. Electronic Notes in Theoretical Computer Science, 259(C), 21-34.
- Formal Aspects of Computing: Editorial. Formal Aspects of Computing, 21(1-2), 1.
- Using Formal Specifications to Support Testing. ACM COMPUT SURV, 41(2). View this article in WRRO
- More Relational Concurrent Refinement: Traces and Partial Relations. Electronic Notes in Theoretical Computer Science, 214(C), 255-276.
- Using Model Checking to Automatically Find Retrieve Relations. Electronic Notes in Theoretical Computer Science, 201(C), 155-175.
- On using data abstractions for model checking refinements. ACTA INFORM, 44(1), 41-71.
- Relational Concurrent Refinement with Internal Operations. Electronic Notes in Theoretical Computer Science, 187, 35-53.
- Filtering retrenchments into refinements. Proceedings - 4th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006, 60-69.
- View this article in WRRO
- Introduction. Software and Systems Modeling, 4(3), 234-235.
- Model checking downward simulations. Electronic Notes in Theoretical Computer Science, 137(2), 205-224.
- Verifying fault-tolerant Erlang programs. Erlang'05 - Proceedings of the ACM SIGPLAN 2005 Erlang Workshop, 26-34.
- Structural refinement of systems specified in object-Z and CSP. Formal Aspects of Computing, 15(1), 1-27.
- Relational Concurrent Refinement. Formal Aspects of Computing, 15(2-3), 182-214.
- Model Checking Stochastic Automata. ACM Transactions on Computational Logic, 4(4), 452-492.
- Unifying concurrent and relational refinement. Electronic Notes in Theoretical Computer Science, 70(3), 94-131.
- Electronics Notes in Theoretical Computer Science: Preface. Electronic Notes in Theoretical Computer Science, 70(3), 331-332.
- Combining component specifications in object-Z and CSP. Formal Aspects of Computing, 13(2), 111-127.
- Testing refinements of state-based formal specifications. Software Testing Verification and Reliability, 9(1), 27-50.
- Constraint-oriented style for object-oriented formal specification. IEE Proceedings: Software, 145(2-3), 61-69.
- Specifying and Refining Internal Operations in Z. Formal Aspects of Computing, 10(2), 125-159.
- Modularising Verification Of Durable Opacity. Logical Methods in Computer Science, Volume 18, Issue 3.
- Proceedings 18th Refinement Workshop. Electronic Proceedings in Theoretical Computer Science, 282.
- Proceedings 17th International Workshop on Refinement. Electronic Proceedings in Theoretical Computer Science, 209.
- Data refinement for true concurrency. Electronic Proceedings in Theoretical Computer Science, 115, 15-35.
- Proceedings 16th International Refinement Workshop. Electronic Proceedings in Theoretical Computer Science, 115.
- From ODP viewpoint consistency to Integrated Formal Methods. Computer Standards and Interfaces.
- Proceedings 15th International Refinement Workshop. Electronic Proceedings in Theoretical Computer Science, 55.
Chapters
- A Fully Verified Persistency Library, Lecture Notes in Computer Science (pp. 26-47). Springer Nature Switzerland
- Understanding, Explaining, and Deriving Refinement, From Astrophysics to Unconventional Computation (pp. 195-206). Springer International Publishing
- Verifying Correctness of Persistent Concurrent Data Structures, Lecture Notes in Computer Science (pp. 179-195). Springer International Publishing
- Incorporating Data into EFSM Inference, Software Engineering and Formal Methods (pp. 257-272). Springer International Publishing
- Formalising Extended Finite State Machine Transition Merging, Formal Methods and Software Engineering (pp. 373-387). Springer International Publishing
- A Proof Method for Linearizability on TSO Architectures, NASA Monographs in Systems and Software Engineering (pp. 61-91). Springer International Publishing
- Testing Refinements by Refining Tests, ZUM ’98: The Z Formal Specification Notation (pp. 265-283). Springer Berlin Heidelberg
- Supporting ODP - Translating LOTOS to Z, IFIP Advances in Information and Communication Technology (pp. 399-406). Springer US
- Viewpoint consistency in ODP, a general interpretation, IFIP Advances in Information and Communication Technology (pp. 189-204). Springer US
- On Behavioural Subtyping in LOTOS, IFIP Advances in Information and Communication Technology (pp. 335-351). Springer US
- The specification and testing of conformance in ODP systems, Testing of Communicating Systems (pp. 93-114). Springer US
- Some Results on Cross Viewpoint Consistency Checking, Open Distributed Processing (pp. 399-412). Springer US
- Maintaining Cross Viewpoint Consistency using Z, Open Distributed Processing (pp. 413-424). Springer US
Conference proceedings papers
- Reverse-engineering EFSMs with data dependencies. Testing Software and Systems (pp 37-54). London, UK (virtual), 10 November 2021 - 11 November 2021. View this article in WRRO
- Brief announcement: On strong observational refinement and forward simulation. 35th International Symposium on Distributed Computing (DISC 2021), Vol. 209 (pp 55:1-55:4). Freiburg, Germany, 4 October 2021 - 8 October 2021.
- Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory (pp 39-58)
- Verifying C11 programs operationally. Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming (pp 355-365)
- Brief announcement: Generalising concurrent correctness to weak memory. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 121
- Observational Models for Linearizability Checking on Weak Memory Models. 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE) (pp 100-107), 29 August 2018 - 31 August 2018.
- Making linearizability compositional for partially ordered executions. Integrated Formal Methods, Vol. 11023 LNCS (pp 110-129), 5 September 2018 - 7 September 2018. View this article in WRRO
- An observational approach to defining linearizability on weak memory models. Lecture Notes in Computer Science (pp 108-123), 19 June 2017 - 22 June 2017. View this article in WRRO
- Proving opacity of a pessimistic STM. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 70 (pp 35.1-35.17), 13 December 2016 - 16 December 2016. View this article in WRRO
- Linearizability and Causality. Software Engineering and Formal Methods. SEFM 2016. Lecture Notes in Computer Science, Vol. 9763 (pp 45-60) View this article in WRRO
- Invariant generation for linearizability proofs. Proceedings of the 31st Annual ACM Symposium on Applied Computing - SAC '16, 4 April 2016 - 8 April 2016. View this article in WRRO
- Choreography-Based Analysis of Distributed Message Passing Programs. 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), 17 February 2016 - 19 February 2016.
- mu2: A Refactoring-Based Mutation Testing Framework for Erlang (pp 178-193)
- Smother: an MC/DC analysis tool for Erlang. Proceedings of the 14th ACM SIGPLAN Workshop on Erlang - Erlang 2015, 4 September 2015 - 4 September 2015.
- Defining correctness conditions for concurrent objects in multicore architectures. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 37 (pp 470-494)
- A Framework for Correctness Criteria on Weak Memory Models (pp 178-194)
- Verifying Opacity of a Transactional Mutex Lock (pp 161-177)
- Admit Your Weakness: Verifying Correctness on TSO Architectures (pp 364-383)
- Experiences using Z2SAL. Proceedings - ICACSIS 2014: 2014 International Conference on Advanced Computer Science and Information Systems (pp 225-231). Jakarta, Indonesia, 18 October 2014 - 19 October 2014. View this article in WRRO
- Synapse: Automatic behaviour inference and implementation comparison for Erlang. Proceedings of the Thirteenth ACM SIGPLAN workshop on Erlang (pp 73-74), 5 September 2014 - 5 September 2014.
- Quiescent Consistency: Defining and Verifying Relaxed Linearizability (pp 200-214)
- Verifying linearizability on TSO architectures. Integrated Formal Methods. IFM: International Conference on Integrated Formal Methods, Vol. 8739 (pp 341-356) View this article in WRRO
- Simplifying proofs of linearisability using layers of abstraction. Electronic Communications of the EASST, Vol. 66
- Inferring Extended Finite State Machine models from software executions. 2013 20th Working Conference on Reverse Engineering (WCRE), 14 October 2013 - 17 October 2013.
- A high-level semantics for program execution under total store order memory. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 8049 LNCS (pp 177-194)
- Automatic inference of erlang module behaviour. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7940 LNCS (pp 253-267)
- Using behaviour inference to optimise regression test sets. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7641 LNCS (pp 184-199)
- Relational concurrent refinement part II: Internal operations and outputs. FORMAL ASPECTS OF COMPUTING, Vol. 21(1-2) (pp 65-102)
- View this article in WRRO
- Verifying data refinements using a model checker. FORMAL ASPECTS OF COMPUTING, Vol. 18(3) (pp 264-287)
- Formalising ODP enterprise policies. Proceedings Third International Enterprise Distributed Object Computing. Conference (Cat. No.99EX366), 30 September 1999 - 30 September 1999.
- IO-refinement in Z. Electronic Workshops in Computing
- Coupling Schemas: Data Refinement and View(point) Composition. Electronic Workshops in Computing
- Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP.. ICFEM (pp 293-303)
- Issues in multiparadigm viewpoint specification. 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 -, 16 October 1996 - 18 October 1996.
- , Vol. 209
- , Vol. 115
- Testing and conformance within distributed systems. Proceedings of 1994 1st International Conference on Software Testing, Reliability and Quality Assurance (STRQA'94)
Reports
Posters
Other
Preprints
- Building a refinement checker for Z, Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011..
- .
- Refinement. Springer International Publishing.
- Research group
-
If you are interested in doing a PhD with Prof. John Derrick then please take a look at the available research topics.
- Grants
-
Research Grants
- Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT), EPSRC, 07/2023 - 11/2026, £422,585, as PI
- Verifiably Correct Transactional Memory, EPSRC, 10/2018 - 08/2022, £397,680, as PI
- Verifiably correct concurrency abstractions, EPSRC, 03/2018 - 02/2020, £17,123, as PI
- Verifying concurrent algorithms on Weak Memory Models, EPSRC, 05/2015 - 11/2018, £389,207, as PI
- PROWESS: Property-based Testing for Web Services, EC FP7, 10/2012 - 10/2015, £405,800, as PI
- Verifying Concurrent Lock-free Algorithms, EPSRC, 04/2012 - 10/2015, £378,907, as PI
- Decision Support Tool, BAE Systems Plc, 07/2011 - 12/2011, £51,895, as PI
- Higher-order Refinement Techniques for model Driven Architecture, EPSRC, 07/2009 - 10/2012, £318,522, as PI
- ProTest: Property based testing, EC FP7, 05/2008 - 12/2011, £277,503, as PI
- Bridging the Gap between Mathematics, ICT and Engineering Research at Sheffield, EPSRC, 01/2007 - 12/2009, £350,842, as Co-PI
- Formally-based tool support for Erlang development, EPSRC, 10/2005 - 03/2009, £225,425, as PI
- Unifying Theories of Refinement, The leverhulme Trust, 10/2005 - 09/2007, £21,994, as PI
- Network: RefineNet, EPSRC, 01/2005 - 06/2007, £52,979, as PI
- Professional activities and memberships
-
- Chair of the BCS FACS sub-group on refinement
- Running (with Eerke Boiten) the series of International Refinement Workshops
- Programme Committee member for conferences such as IFM, ABZ, MBT, AVOCS, ICTSS, MoDeVVA
- Conference Chair for ABZ/iFM 2012, FORTE/PSTV 2007, iFM 2004, FMOODS 1997
- Until recently I was the Vice-chair of IFIP Working Group 6.1 (Architectures and Protocols for Distributed Systems)
- Guest Editor of numerous journal editions (SCP, FACS, SoSyM, IEEE Trans. on Soft. Eng., STVR etc.)
- Recent books include 2nd edition of Refinement in Z and Object-Z: Foundations and Advanced Applications (with Eerke Boiten)