Professor John Derrick

DPhil

Department of Computer Science

Acting Vice-President and Head of Faculty of Science

Professor of Computer Science

Member of the Verification and Testing research groups

j.derrick@sheffield.ac.uk
+44 114 222 1849
+44 114 222 9762 (PA: Sophie Jacob)

Full contact details

Professor John Derrick
Department 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.

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

Edited books

  • Bowman H & Derrick J (Ed.) (2001) Formal Methods for Distributed Processing: A Survey of Object-Oriented Approaches. Cambridge Univ Press. RIS download Bibtex download

Journal articles

Chapters

Conference proceedings papers

  • Bila E, Doherty S, Dongol B, Derrick J, Schellhorn G & Wehrheim H (2020) Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory (pp 39-58) RIS download Bibtex download
  • Doherty S, Dongol B, Wehrheim H & Derrick J (2019) Verifying C11 programs operationally. Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming (pp 355-365) RIS download Bibtex download
  • Doherty S, Dongol B, Wehrheim H & Derrick J (2018) Brief announcement: Generalising concurrent correctness to weak memory. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 121 RIS download Bibtex download
  • Winter K, Smith G & Derrick J (2018) 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. RIS download Bibtex download
  • Doherty S, Dongol B, Wehrheim H & Derrick J (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 RIS download Bibtex download
  • Derrick J & Smith G (2017) 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 RIS download Bibtex download
  • Doherty S, Dongol B, Derrick J, Schellhorn G & Wehrheim H (2017) 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 RIS download Bibtex download
  • Doherty S & Derrick J (2016) 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 RIS download Bibtex download
  • Smith G & Derrick J (2016) 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 RIS download Bibtex download
  • Taylor R, Tuosto E, Walkinshaw N & Derrick J (2016) 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. RIS download Bibtex download
  • Taylor R & Derrick J (2015) mu2: A Refactoring-Based Mutation Testing Framework for Erlang (pp 178-193) RIS download Bibtex download
  • Taylor R & Derrick J (2015) 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. RIS download Bibtex download
  • Dongol B, Derrick J, Groves L & Smith G (2015) Defining correctness conditions for concurrent objects in multicore architectures. Leibniz International Proceedings in Informatics, LIPIcs, Vol. 37 (pp 470-494) RIS download Bibtex download
  • Derrick J & Smith G (2015) A Framework for Correctness Criteria on Weak Memory Models (pp 178-194) RIS download Bibtex download
  • Derrick J, Dongol B, Schellhorn G, Travkin O & Wehrheim H (2015) Verifying Opacity of a Transactional Mutex Lock (pp 161-177) RIS download Bibtex download
  • Smith G, Derrick J & Dongol B (2015) Admit Your Weakness: Verifying Correctness on TSO Architectures (pp 364-383) RIS download Bibtex download
  • Siregar MU, Derrick J, North SD & Simons AJH (2014) 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 RIS download Bibtex download
  • Lamela Seijas P, Thompson S, Taylor R, Bogdanov K & Derrick J (2014) 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. RIS download Bibtex download
  • Derrick J, Dongol B, Schellhorn G, Tofan B, Travkin O & Wehrheim H (2014) Quiescent Consistency: Defining and Verifying Relaxed Linearizability (pp 200-214) RIS download Bibtex download
  • Derrick J, Smith G & Dongol B (2014) 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 RIS download Bibtex download
  • Dongol B & Derrick J (2013) Simplifying proofs of linearisability using layers of abstraction. Electronic Communications of the EASST, Vol. 66 RIS download Bibtex download
  • Walkinshaw N, Taylor R & Derrick J (2013) Inferring Extended Finite State Machine models from software executions. 2013 20th Working Conference on Reverse Engineering (WCRE), 14 October 2013 - 17 October 2013. RIS download Bibtex download
  • Taylor R, Bogdanov K & Derrick J (2013) 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) RIS download Bibtex download
  • Dongol B, Travkin O, Derrick J & Wehrheim H (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) RIS download Bibtex download
  • Taylor R, Hall M, Bogdanov K & Derrick J (2012) 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) RIS download Bibtex download
  • (2012) Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012. Proceedings. IFM, Vol. 7321 RIS download Bibtex download
  • (2011) Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.. Refine@FM, Vol. 55 RIS download Bibtex download
  • Derrick J, North S & Simons AJH (2011) Building a refinement checker for Z. Refine@FM, Vol. 55 (pp 37-52) RIS download Bibtex download
  • Walkinshaw N, Bogdanov K, Derrick J & Paris J (2010) Increasing Functional Coverage by Inductive Testing: A Case Study.. ICTSS, Vol. 6435 (pp 126-141) RIS download Bibtex download
  • Boiten E, Derrick J & Schellhorn G (2009) Relational concurrent refinement part II: Internal operations and outputs. FORMAL ASPECTS OF COMPUTING, Vol. 21(1-2) (pp 65-102) RIS download Bibtex download
  • Walkinshaw N, Derrick J & Guo Q (2009) Iterative Refinement of Reverse-Engineered Models by Model-Based Testing.. FM, Vol. 5850 (pp 305-320) RIS download Bibtex download
  • Boitlen E & Derrick J (2009) Modelling Divergence in Relational Concurrent Refinement. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 5423 (pp 183-199) RIS download Bibtex download
  • Guo Q, Derrick J & Walkinshaw N (2009) Applying Testability Transformations to Achieve Structural Coverage of Erlang Programs. TESTING OF SOFTWARE AND COMMUNICATION SYSTEMS, PROCEEDINGS, Vol. 5826 (pp 81-96) RIS download Bibtex download
  • Derrick J, Schellhorn G & Wehrheim H (2008) Mechanizing a correctness proof for a lock-free concurrent stack. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, Vol. 5051 (pp 78-95) RIS download Bibtex download
  • Derrick J, North S & Simons AJH (2008) Z2SAL-Building a Model Checker for Z. ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, Vol. 5238 (pp 280-293) View this article in WRRO RIS download Bibtex download
  • Guo Q, Derrick J & Hoch C (2008) Verifying Erlang telecommunication systems with the process algebra mu CRL. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2008, Vol. 5048 (pp 201-217) RIS download Bibtex download
  • (2007) Formal Techniques for Networked and Distributed Systems - FORTE 2007, 27th IFIP WG 6.1 International Conference, Tallinn, Estonia, June 27-29, 2007, Proceedings. FORTE, Vol. 4574 RIS download Bibtex download
  • Guo Q & Derrick J (2007) Verification of Timed Erlang/OTP Components Using the Process Algebra mu CRL. ERLANG'07: PROCEEDINGS OF THE 2007 SIGPLAN ERLANG WORKSHOP (pp 55-64) RIS download Bibtex download
  • Derrick J, Schellhorn G & Wehrheim H (2007) Proving linearizability via non-atomic refinement. Integrated Formal Methods, Proceedings, Vol. 4591 (pp 195-214) RIS download Bibtex download
  • Smith G & Derrick J (2006) Verifying data refinements using a model checker. FORMAL ASPECTS OF COMPUTING, Vol. 18(3) (pp 264-287) RIS download Bibtex download
  • Derrick J, North S & Simons T (2006) Issues in implementing a model checker for Z. Formal Methods and Software Engineering, Proceedings, Vol. 4260 (pp 678-696) RIS download Bibtex download
  • Derrick J & Wehrheim H (2006) Model transformations incorporating multiple views. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 111-126) RIS download Bibtex download
  • Derrick J & Wehrheim H (2005) Non-atomic refinement in Z and CSP. ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, Vol. 3455 (pp 24-44) RIS download Bibtex download
  • Boiten EA & Derrick J (2005) Formal program development with approximations. ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, Vol. 3455 (pp 374-392) RIS download Bibtex download
  • (2004) Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings. IFM, Vol. 2999 RIS download Bibtex download
  • Derrick J & Smith G (2004) Linear temporal logic and Z refinement. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, Vol. 3116 (pp 117-131) RIS download Bibtex download
  • Derrick J (2003) Timed CSP and Object-Z. ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, Vol. 2651 (pp 300-318) RIS download Bibtex download
  • Derrick J & Boiten E (2003) Recent advances in refinement. ABSTRACT STATE MACHINES 2003: ADVANCES IN THEORY AND PRACTICE, PROCEEDINGS, Vol. 2589 (pp 33-56) RIS download Bibtex download
  • Akehurst DH, Derrick J & Waters AG (2003) Addressing computational viewpoint design. SEVENTH IEEE INTERNATIONAL ENTERPRISE DISTRIBUTED OBJECT COMPUTING CONFERENCE, PROCEEDINGS (pp 147-158) RIS download Bibtex download
  • Derrick J & Wehrheim H (2003) Using coupled simulations in non-atomic refinement. ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, Vol. 2651 (pp 127-147) RIS download Bibtex download
  • Akehurst D, Derrick J & Waters AG (2003) Design and verification of distributed multi-media systems. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, Vol. 2884 (pp 276-292) RIS download Bibtex download
  • Miarka R, Derrick J & Boiten EA (2002) Handling Inconsistencies in Z Using Quasi-Classical Logic.. ZB, Vol. 2272 (pp 204-225) RIS download Bibtex download
  • Arts T, Earle CB & Derrick J (2002) Verifying Erlang Code: A Resource Locker Case-Study.. FME, Vol. 2391 (pp 184-203) RIS download Bibtex download
  • Taylor C, Boiten EA & Derrick J (2002) Interpreting ODP Viewpoint Specification: Observations from a Case Study.. FMOODS, Vol. 209 (pp 61-76) RIS download Bibtex download
  • Smith G & Derrick J (2002) Abstract Specification in Object-Z and CSP.. ICFEM, Vol. 2495 (pp 108-119) RIS download Bibtex download
  • Bordbar B, Derrick J & Waters G (2002) A UML approach to the design of open distributed systems. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Vol. 2495 (pp 561-572) RIS download Bibtex download
  • Cole J, Derrick J, Milosevic Z & Raymond K (2001) Author obliged to submit paper before 4 July: Policies in an enterprise specification. POLICIES FOR DISTRIBUTED SYSTEMS AND NETWORKS, PROCEEDINGS, Vol. 1995 (pp 1-17) RIS download Bibtex download
  • Miarka R, Boiten EA & Derrick J (2000) Guards, Preconditions, and Refinement in Z.. ZB, Vol. 1878 (pp 286-303) RIS download Bibtex download
  • Taylor C, Derrick J & Boiten E (2000) A case study in partial specification: Consistency and refinement for object-Z. ICFEM 2000: THIRD INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS (pp 177-185) RIS download Bibtex download
  • Boiten E & Derrick J (2000) Liberating data refinement. MATHEMATICS OF PROGRAM CONSTRUCTION, Vol. 1837 (pp 144-166) RIS download Bibtex download
  • Derrick J & Boiten E (2000) Refinement of objects and operations in Object-Z. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS IV, Vol. 49 (pp 257-277) RIS download Bibtex download
  • Bryans J, Blair L, Bowman H & Derrick J (2000) Specification and analysis of automata-based designs. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 1945 (pp 176-193) RIS download Bibtex download
  • Derrick J & Smith G (2000) Structural refinement in Object-Z/CSP. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 1945 (pp 194-213) RIS download Bibtex download
  • Steen MWA & Derrick J (1999) Formalising ODP enterprise policies. Proceedings Third International Enterprise Distributed Object Computing. Conference (Cat. No.99EX366), 30 September 1999 - 30 September 1999. RIS download Bibtex download
  • Bowman H & Derrick J (1999) A Junction between State Based and Behavioural Specification (Invited Talk).. FMOODS, Vol. 139 (pp 213-239) RIS download Bibtex download
  • Derrick J & Boiten EA (1999) Specifying Component and Context Specification Using Promotion.. IFM (pp 293-312) RIS download Bibtex download
  • Bryans JW & Derrick J (1999) Stochastic Specification and Verification.. IWFM RIS download Bibtex download
  • Steen M, Derrick J, Boiten E & Bowman H (1999) Consistency of partial process specifications. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, Vol. 1548 (pp 248-262) RIS download Bibtex download
  • Derrick J & Boiten E (1999) Non-atomic refinement in Z. FM'99-FORMAL METHODS, VOL II, Vol. 1709 (pp 1477-1496) RIS download Bibtex download
  • Derrick J & Boiten E (1998) Testing refinements by refining tests. ZUM '98: THE Z FORMAL SPECIFICATION NOTATION, Vol. 1493 (pp 265-283) RIS download Bibtex download
  • Steen M, Bowman H, Derrick J & Boiten EA (1997) Disjunction of LOTOS Specifications.. FORTE, Vol. 107 (pp 177-192) RIS download Bibtex download
  • Boiten EA, Bowman H, Derrick J & Steen M (1997) Viewpoint Consistency in Z and LOTOS: A Case Study.. FME, Vol. 1313 (pp 644-664) RIS download Bibtex download
  • Derrick J, Boiten EA, Bowman H & Steen M (1997) Weak Refinement in Z.. ZUM, Vol. 1212 (pp 369-388) RIS download Bibtex download
  • Smith G & Derrick J (1997) Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP.. ICFEM (pp 293-303) RIS download Bibtex download
  • Fernandes GPA & Derrick J (1997) Formal specification and testing of a management architecture. INTEGRATED NETWORK MANAGEMENT V (pp 473-484) RIS download Bibtex download
  • Bowman H & Derrick J (1997) Extending LOTOS with time: A true concurrency perspective. TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, Vol. 1231 (pp 383-399) RIS download Bibtex download
  • Boiten E, Bowman H, Derrick J & Steen M (1996) 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. RIS download Bibtex download
  • Boiten EA, Derrick J, Bowman H & Steen M (1996) Consistency and Refinement for Partial Specification in Z.. FME, Vol. 1051 (pp 287-306) RIS download Bibtex download
  • Derrick J, Bowman H, Boiten EA & Steen M (1996) Comparing LOTOS and Z Refinement Relations.. FORTE, Vol. 69 (pp 501-516) RIS download Bibtex download
  • Derrick J, Linington PF & Thompson SJ (1995) Formal description techniques for object management.. Integrated Network Management, Vol. 11 (pp 641-653) RIS download Bibtex download
  • Bowman H, Derrick J & Steen M (1995) Viewpoints and Objects.. ZUM, Vol. 967 (pp 449-468) RIS download Bibtex download
  • Steen M, Bowman H & Derrick J (1995) Composition of LOTOS specifications.. PSTV, Vol. 38 (pp 87-102) RIS download Bibtex download
  • Bowman H & Derrick J (1995) Modelling distributed systems using Z.. SAC (pp 147-151) RIS download Bibtex download
  • Bowman H & Derrick J (1995) A True Concurrency Semantics for Quality of Service Specification and Validation.. MMNET (pp 173-182) RIS download Bibtex download
  • Bowman H, Derrick J & Jones RE (1994) Modelling Garbage Collection Algorithms Using CCS and Temporal Logic (Abstract).. PODC (pp 394-394) RIS download Bibtex download
  • Bowman H & Derrick J (1994) Consistency and Conformance in ODP (Abstract).. PODC (pp 388-388) RIS download Bibtex download
  • () , Vol. 209 RIS download Bibtex download
  • () , Vol. 115 RIS download Bibtex download
  • Bowman H & Derrick J () Testing and conformance within distributed systems. Proceedings of 1994 1st International Conference on Software Testing, Reliability and Quality Assurance (STRQA'94) RIS download Bibtex download

Reports

  • Dongol B & Derrick J () Proving linearisability via coarse-grained abstraction RIS download Bibtex download

Posters

  • Siregar MU & Derrick J Using Abstraction in Model Checking Z Specifications. University of Sheffield Engineering Symposium. RIS download Bibtex download

Other

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

Current grants

Previous grants

  • Verifying concurrent algorithms on Weak Memory Models, EPSRC, 05/2015 to 11/2018, £389,207, as PI
  • PROWESS: Property-based Testing for Web Services, EC FP7, 10/2012 to 10/2015, £405,800, as PI
  • Verifying Concurrent Lock-free Algorithms, EPSRC, 04/2012 to 10/2015, £378,907, as PI
  • Decision Support Tool, BAE Systems Plc, 07/2011 to 12/2011, £51,895, as PI
  • Higher-order Refinement Techniques for model Driven Architecture, EPSRC, 07/2009 to 10/2012, £318,522, as PI
  • ProTest: Property based testing, EC FP7, 05/2008 to 12/2011, £277,503, as PI
  • Bridging the Gaps EPSRC, EPSRC, 01/2007 to 12/2009, £350,842, as Co-PI
  • Formally-based tool support for Erlang development, EPSRC, 10/2005 to 03/2009, £225,425, as PI
  • Unifying Theories of Refinement, The leverhulme Trust, 10/2005 to 09/2007, £21,994, as PI
  • Network: RefineNet, EPSRC, 01/2005 to 06/2007, £52,979, as PI
Professional activities
  • 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)