Professor John Derrick
DPhil
School of Computer Science
Acting VicePresident and Head of Faculty of Science
Professor of Computer Science
Member of the Foundations of Computation and Testing research groups
+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 statebased 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. SpringerVerlag New York Inc.
 Integrated formal methods. Springer.
 Refinement in Z and ObjectZ. Springer London.
 Refinement in Z and ObjectZ. Springer Verlag.
 Preface. Elsevier.
Edited books
 Formal Methods for Distributed Processing: A Survey of ObjectOriented Approaches. Cambridge Univ Press.
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), 597625. View this article in WRRO
 Inferring extended finite state machine models from software executions. Empirical Software Engineering, 21(3), 811853. View this article in WRRO
 Intervalbased data refinement: A uniform approach to true concurrency in discrete and realtime systems. Science of Computer Programming, 111, 214247. View this article in WRRO
 Verifying Linearisability. ACM Computing Surveys, 48(2), 143.
 A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures. ACM Transactions on Computational Logic, 15(4), 137. View this article in WRRO
 Using coarsegrained 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, 151168. View this article in WRRO
 Editorial. Formal Aspects of Computing, 11.
 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, 200214.
 Deriving realtime 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, 243259.
 Relational concurrent refinement part III: traces, partial relations and automata. Formal Aspects of Computing, 126.
 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, 121137.
 Temporallogic property preservation under Z refinement. Formal Aspects of Computing, 124.
 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, 323337.
 Selected papers of the Refinement Workshop Turku (2008). Science of Computer Programming, 76(9), 737738.
 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), 3356.
 Incompleteness of relational simulations in the blocking paradigm. SCI COMPUT PROGRAM, 75(12), 12621269. View this article in WRRO
 Model transformations across views. SCI COMPUT PROGRAM, 75(3), 192210.
 Modelchecking 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, 2338.
 Formally based tool support for model checking Erlang applications. International Journal on Software Tools for Technology Transfer, 122.
 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, 272289.
 Propertybased testing  The ProTest project. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6286 LNCS, 250271.
 Editorial. FORM ASP COMPUT, 22(1), 11.
 Editorial. FORM ASP COMPUT, 21(12), 11.
 Preface.. Electron. Notes Theor. Comput. Sci., 259, 11.
 Relational Concurrent Refinement: Automata. Electronic Notes in Theoretical Computer Science, 259(C), 2134.
 Formal Aspects of Computing: Editorial. Formal Aspects of Computing, 21(12), 1.
 Z2SAL: a translationbased model checker for Z. Formal Aspects of Computing, 129.
 Using Formal Specifications to Support Testing. ACM COMPUT SURV, 41(2). View this article in WRRO
 Preface.. Electron. Notes Theor. Comput. Sci., 214, 11.
 Preface.. Electron. Notes Theor. Comput. Sci., 201, 11.
 More Relational Concurrent Refinement: Traces and Partial Relations. Electronic Notes in Theoretical Computer Science, 214(C), 255276.
 Using Model Checking to Automatically Find Retrieve Relations. Electronic Notes in Theoretical Computer Science, 201(C), 155175.
 On using data abstractions for model checking refinements. ACTA INFORM, 44(1), 4171.
 Preface.. Electron. Notes Theor. Comput. Sci., 187, 11.
 Relational Concurrent Refinement with Internal Operations. Electronic Notes in Theoretical Computer Science, 187, 3553.
 Guest Editorial.. Formal Asp. Comput., 18, 12.
 Filtering retrenchments into refinements. Proceedings  4th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006, 6069.
 View this article in WRRO Editorial. International Journal of Business Performance Management, 8(1), 14.
 Introduction. Software and Systems Modeling, 4(3), 234235.
 Guest Editorial Integrated Formal Methods.. Formal Asp. Comput., 17, 389389.
 Preface.. Electron. Notes Theor. Comput. Sci., 137, 13.
 Model checking downward simulations. Electronic Notes in Theoretical Computer Science, 137(2), 205224.
 Verifying faulttolerant Erlang programs. Erlang'05  Proceedings of the ACM SIGPLAN 2005 Erlang Workshop, 2634.
 Development of a verified Erlang program for resource locking.. Int. J. Softw. Tools Technol. Transf., 5, 205220.
 Programming Methodology A. McIver and C. Morgan, editors, SpringerVerlag, 2002.. J. Funct. Program., 14, 597598.
 Relational framework for the integration of specifications. Journal of Integrated Design and Process Science, 7(3), 3948.
 Structural refinement of systems specified in objectZ and CSP. Formal Aspects of Computing, 15(1), 127.
 Relational Concurrent Refinement. Formal Aspects of Computing, 15(23), 182214.
 Model Checking Stochastic Automata. ACM Transactions on Computational Logic, 4(4), 452492.
 Using UML to specify QoS constraints in ODP. COMPUT NETW, 40(2), 279304.
 A formal framework for viewpoint consistency. FORM METHOD SYST DES, 21(2), 111166.
 ODP computationaltoinformation viewpoint mappings: a translation of CORBA IDL to Z.. IEE Proc. Softw., 149, 5763.
 Unifying concurrent and relational refinement. Electronic Notes in Theoretical Computer Science, 70(3), 94131.
 Electronics Notes in Theoretical Computer Science: Preface. Electronic Notes in Theoretical Computer Science, 70(3), 331332.
 Combining component specifications in objectZ and CSP. Formal Aspects of Computing, 13(2), 111127.
 Specification, refinement and verification of concurrent systems  An integration of ObjectZ and CSP. FORM METHOD SYST DES, 18(3), 249284.
 Analysis of a multimedia stream using stochastic process algebra. COMPUT J, 44(4), 230245.
 Editorial: Special issue on specificationbased testing. SOFTW TEST VERIF BEH, 10(4), 201202.
 A single complete refinement rule for Z. J LOGIC COMPUT, 10(5), 663675.
 Viewpoint consistency in ODP. COMPUT NETW, 34(3), 503537.
 ODP enterprise viewpoint specification. COMP STAND INTER, 22(3), 165189.
 Selected papers from the Second IFIP Int'l Conference on Formal Methods for Open Object Based Distributed Systems, 1997. IEEE T SOFTWARE ENG, 26(7), 577578.
 Stochastic Model Checking for Multimedia. CoRR, cs.MM/0002004.
 Concurrent and RealTime Systems: The CSP Approach, Steve Schneider, Wiley, 2000 (Book Review).. Softw. Test. Verification Reliab., 10, 195195.
 Calculating upward and downward simulations of statebased specifications. INFORM SOFTWARE TECH, 41(13), 917923.
 Constructive consistency checking for partial specification in Z. SCI COMPUT PROGRAM, 35(1), 2975.
 Viewpoints and consistency: translating LOTOS to Objectz. COMP STAND INTER, 21(3), 251272.
 Strategies for consistency checking based on unification. SCI COMPUT PROGRAM, 33(3), 261298.
 Testing refinements of statebased formal specifications. Software Testing Verification and Reliability, 9(1), 2750.
 Constraintoriented style for objectoriented formal specification. IEE Proceedings: Software, 145(23), 6169.
 Specifying and Refining Internal Operations in Z. Formal Aspects of Computing, 10(2), 125159.
 Crossviewpoint consistency in open distributed processing. SOFTWARE ENG J, 11(1), 4457.
 FDTS FOR ODP. COMP STAND INTER, 17(56), 457479.
 Meeting of the Association for Symbolic Logic: Orleans, France, 1972.. J. Symb. Log., 39, 371389.
 Meeting of the Association for Symbolic Logic Leeds 1967.. J. Symb. Log., 33, 490490.
 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, 1535.
 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. 2647). Springer Nature Switzerland
 Understanding, Explaining, and Deriving Refinement, From Astrophysics to Unconventional Computation (pp. 195206). Springer International Publishing
 Verifying Correctness of Persistent Concurrent Data Structures, Lecture Notes in Computer Science (pp. 179195). Springer International Publishing
 Incorporating Data into EFSM Inference, Software Engineering and Formal Methods (pp. 257272). Springer International Publishing
 Formalising Extended Finite State Machine Transition Merging, Formal Methods and Software Engineering (pp. 373387). Springer International Publishing
 A Proof Method for Linearizability on TSO Architectures, NASA Monographs in Systems and Software Engineering (pp. 6191). Springer International Publishing
 Relational concurrent refinement  Partial and total frameworks, From Action Systems to Distributed Systems: The Refinement Approach (pp. 143154).
 Testing Refinements by Refining Tests, ZUM ’98: The Z Formal Specification Notation (pp. 265283). Springer Berlin Heidelberg
 Supporting ODP  Translating LOTOS to Z, IFIP Advances in Information and Communication Technology (pp. 399406). Springer US
 Viewpoint consistency in ODP, a general interpretation, IFIP Advances in Information and Communication Technology (pp. 189204). Springer US
 On Behavioural Subtyping in LOTOS, IFIP Advances in Information and Communication Technology (pp. 335351). Springer US
 The specification and testing of conformance in ODP systems, Testing of Communicating Systems (pp. 93114). Springer US
 Some Results on Cross Viewpoint Consistency Checking, Open Distributed Processing (pp. 399412). Springer US
 Maintaining Cross Viewpoint Consistency using Z, Open Distributed Processing (pp. 413424). Springer US
Conference proceedings papers
 Reverseengineering EFSMs with data dependencies. Testing Software and Systems (pp 3754). 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:155:4). Freiburg, Germany, 4 October 2021  8 October 2021.
 Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory (pp 3958)
 Verifying C11 programs operationally. Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming (pp 355365)
 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 100107), 29 August 2018  31 August 2018.
 Making linearizability compositional for partially ordered executions. Integrated Formal Methods, Vol. 11023 LNCS (pp 110129), 5 September 2018  7 September 2018. View this article in WRRO
 MoDeVVa 2018 15 ^{th} workshop on modeldriven engineering, verification and validation. CEUR Workshop Proceedings, Vol. 2245 (pp 553554)
 Preface. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE(282)
 An observational approach to defining linearizability on weak memory models. Lecture Notes in Computer Science (pp 108123), 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.135.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 4560) 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
 ChoreographyBased Analysis of Distributed Message Passing Programs. 2016 24th Euromicro International Conference on Parallel, Distributed, and NetworkBased Processing (PDP), 17 February 2016  19 February 2016.
 mu2: A RefactoringBased Mutation Testing Framework for Erlang (pp 178193)
 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 470494)
 A Framework for Correctness Criteria on Weak Memory Models (pp 178194)
 Verifying Opacity of a Transactional Mutex Lock (pp 161177)
 Admit Your Weakness: Verifying Correctness on TSO Architectures (pp 364383)
 Experiences using Z2SAL. Proceedings  ICACSIS 2014: 2014 International Conference on Advanced Computer Science and Information Systems (pp 225231). 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 7374), 5 September 2014  5 September 2014.
 Quiescent Consistency: Defining and Verifying Relaxed Linearizability (pp 200214)
 Verifying linearizability on TSO architectures. Integrated Formal Methods. IFM: International Conference on Integrated Formal Methods, Vol. 8739 (pp 341356) 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 highlevel 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 177194)
 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 253267)
 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 184199)
 Integrated Formal Methods  9th International Conference, IFM 2012, Pisa, Italy, June 1821, 2012. Proceedings. IFM, Vol. 7321
 Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011.. Refine@FM, Vol. 55
 Increasing Functional Coverage by Inductive Testing: A Case Study.. ICTSS, Vol. 6435 (pp 126141)
 Relational concurrent refinement part II: Internal operations and outputs. FORMAL ASPECTS OF COMPUTING, Vol. 21(12) (pp 65102)
 Iterative Refinement of ReverseEngineered Models by ModelBased Testing.. FM, Vol. 5850 (pp 305320)
 Modelling Divergence in Relational Concurrent Refinement. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 5423 (pp 183199)
 Applying Testability Transformations to Achieve Structural Coverage of Erlang Programs. TESTING OF SOFTWARE AND COMMUNICATION SYSTEMS, PROCEEDINGS, Vol. 5826 (pp 8196)
 Mechanizing a correctness proof for a lockfree concurrent stack. FORMAL METHODS FOR OPEN OBJECTBASED DISTRIBUTED SYSTEMS, PROCEEDINGS, Vol. 5051 (pp 7895)
 View this article in WRRO Z2SALBuilding a Model Checker for Z. ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, Vol. 5238 (pp 280293)
 Verifying Erlang telecommunication systems with the process algebra mu CRL. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS  FORTE 2008, Vol. 5048 (pp 201217)
 Formal Techniques for Networked and Distributed Systems  FORTE 2007, 27th IFIP WG 6.1 International Conference, Tallinn, Estonia, June 2729, 2007, Proceedings. FORTE, Vol. 4574
 Verification of Timed Erlang/OTP Components Using the Process Algebra mu CRL. ERLANG'07: PROCEEDINGS OF THE 2007 SIGPLAN ERLANG WORKSHOP (pp 5564)
 Proving linearizability via nonatomic refinement. Integrated Formal Methods, Proceedings, Vol. 4591 (pp 195214)
 Verifying data refinements using a model checker. FORMAL ASPECTS OF COMPUTING, Vol. 18(3) (pp 264287)
 Issues in implementing a model checker for Z. Formal Methods and Software Engineering, Proceedings, Vol. 4260 (pp 678696)
 Model transformations incorporating multiple views. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 111126)
 Nonatomic refinement in Z and CSP. ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, Vol. 3455 (pp 2444)
 Formal program development with approximations. ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, Vol. 3455 (pp 374392)
 Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 47, 2004, Proceedings. IFM, Vol. 2999
 Linear temporal logic and Z refinement. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, Vol. 3116 (pp 117131)
 Recent advances in refinement. ABSTRACT STATE MACHINES 2003: ADVANCES IN THEORY AND PRACTICE, PROCEEDINGS, Vol. 2589 (pp 3356)
 Using coupled simulations in nonatomic refinement. ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, Vol. 2651 (pp 127147)
 Timed CSP and ObjectZ. ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, Vol. 2651 (pp 300318)
 Design and verification of distributed multimedia systems. FORMAL METHODS FOR OPEN OBJECTBASED DISTRIBUTED SYSTEMS, PROCEEDINGS, Vol. 2884 (pp 276292)
 Addressing computational viewpoint design. SEVENTH IEEE INTERNATIONAL ENTERPRISE DISTRIBUTED OBJECT COMPUTING CONFERENCE, PROCEEDINGS (pp 147158)
 Design and Verification of Distributed Multimedia Systems.. FMOODS, Vol. 2884 (pp 176292)
 Handling Inconsistencies in Z Using QuasiClassical Logic.. ZB, Vol. 2272 (pp 204225)
 Verifying Erlang Code: A Resource Locker CaseStudy.. FME, Vol. 2391 (pp 184203)
 Interpreting ODP Viewpoint Specification: Observations from a Case Study.. FMOODS, Vol. 209 (pp 6176)
 Abstract Specification in ObjectZ and CSP.. ICFEM, Vol. 2495 (pp 108119)
 A UML approach to the design of open distributed systems. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Vol. 2495 (pp 561572)
 Author obliged to submit paper before 4 July: Policies in an enterprise specification. POLICIES FOR DISTRIBUTED SYSTEMS AND NETWORKS, PROCEEDINGS, Vol. 1995 (pp 117)
 Guards, Preconditions, and Refinement in Z.. ZB, Vol. 1878 (pp 286303)
 Liberating data refinement. MATHEMATICS OF PROGRAM CONSTRUCTION, Vol. 1837 (pp 144166)
 Refinement of objects and operations in ObjectZ. FORMAL METHODS FOR OPEN OBJECTBASED DISTRIBUTED SYSTEMS IV, Vol. 49 (pp 257277)
 A case study in partial specification: Consistency and refinement for objectZ. ICFEM 2000: THIRD INTERNATIONAL CONFERENCE ON FORMAL ENGINEERING METHODS, PROCEEDINGS (pp 177185)
 Structural refinement in ObjectZ/CSP. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 1945 (pp 194213)
 Specification and analysis of automatabased designs. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 1945 (pp 176193)
 Nonatomic refinement in Z. FM'99FORMAL METHODS, VOL II, Vol. 1709 (pp 14771496)
 Formalising ODP enterprise policies. Proceedings Third International Enterprise Distributed Object Computing. Conference (Cat. No.99EX366), 30 September 1999  30 September 1999.
 Specifying Component and Context Specification Using Promotion.. IFM (pp 293312)
 A Junction between State Based and Behavioural Specification (Invited Talk).. FMOODS, Vol. 139 (pp 213239)
 Stochastic Specification and Verification.. IWFM
 Consistency of partial process specifications. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, Vol. 1548 (pp 248262)
 Testing refinements by refining tests. ZUM '98: THE Z FORMAL SPECIFICATION NOTATION, Vol. 1493 (pp 265283)
 IOrefinement in Z. Electronic Workshops in Computing
 Coupling Schemas: Data Refinement and View(point) Composition. Electronic Workshops in Computing
 Disjunction of LOTOS Specifications.. FORTE, Vol. 107 (pp 177192)
 Viewpoint Consistency in Z and LOTOS: A Case Study.. FME, Vol. 1313 (pp 644664)
 Weak Refinement in Z.. ZUM, Vol. 1212 (pp 369388)
 Refinement and Verification of Concurrent Systems Specified in ObjectZ and CSP.. ICFEM (pp 293303)
 Extending LOTOS with time: A true concurrency perspective. TRANSFORMATIONBASED REACTIVE SYSTEMS DEVELOPMENT, Vol. 1231 (pp 383399)
 Formal specification and testing of a management architecture. INTEGRATED NETWORK MANAGEMENT V (pp 473484)
 Issues in multiparadigm viewpoint specification. Joint proceedings of the second international software architecture workshop (ISAW2) and international workshop on multiple perspectives in software development (Viewpoints '96) on SIGSOFT '96 workshops , 16 October 1996  18 October 1996.
 Consistency and Refinement for Partial Specification in Z.. FME, Vol. 1051 (pp 287306)
 Comparing LOTOS and Z Refinement Relations.. FORTE, Vol. 69 (pp 501516)
 Formal description techniques for object management.. Integrated Network Management, Vol. 11 (pp 641653)
 Composition of LOTOS specifications.. PSTV, Vol. 38 (pp 87102)
 Viewpoints and Objects.. ZUM, Vol. 967 (pp 449468)
 Modelling distributed systems using Z.. SAC (pp 147151)
 A True Concurrency Semantics for Quality of Service Specification and Validation.. MMNET (pp 173182)
 Modelling Garbage Collection Algorithms Using CCS and Temporal Logic (Abstract).. PODC (pp 394394)
 Consistency and Conformance in ODP (Abstract).. PODC (pp 388388)
 , 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
 Using Abstraction in Model Checking Z Specifications. University of Sheffield Engineering Symposium.
Other
Preprints
 Proceedings 18th Refinement Workshop, arXiv.
 Data refinement for true concurrency, arXiv.
 Proceedings 16th International Refinement Workshop, arXiv.
 Building a refinement checker for Z, Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011..
 Proceedings 15th International Refinement Workshop, arXiv.
 .
 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

Grants
 Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT), EPSRC, 07/2023 to 11/2026, £422,585, as PI
 Verifiably Correct Transactional Memory, EPSRC, 10/2018 to 08/2022, £397,680, as PI
 Verifiably correct concurrency abstractions, EPSRC, 03/2018 to 02/2020, £17,123, as PI
 Verifying concurrent algorithms on Weak Memory Models, EPSRC, 05/2015 to 11/2018, £389,207, as PI
 PROWESS: Propertybased Testing for Web Services, EC FP7, 10/2012 to 10/2015, £405,800, as PI
 Verifying Concurrent Lockfree 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
 Higherorder 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 Gap between Mathematics, ICT and Engineering Research at Sheffield, EPSRC, 01/2007 to 12/2009, £350,842, as CoPI
 Formallybased 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 and memberships

 Chair of the BCS FACS subgroup 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 Vicechair 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 ObjectZ: Foundations and Advanced Applications (with Eerke Boiten)