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
j.derrick@sheffield.ac.uk
+44 114 222 1849
+44 114 222 1849
+44 114 222 9762
(PA: Sophie Jacob)
Regent Court (DCS)
Full contact details
Professor John Derrick
School of Computer Science
Regent Court (DCS)
211 Portobello
Sheffield
S1 4DP
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.
- Refinement in Z and Object-Z. Springer Verlag.
- Preface. Elsevier.
Edited books
- Formal Methods for Distributed Processing: A Survey of Object-Oriented 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), 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.
- Temporal-logic property preservation under Z refinement. Formal Aspects of Computing, 1-24.
- 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.
- Formally based tool support for model checking Erlang applications. International Journal on Software Tools for Technology Transfer, 1-22.
- 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.
- Preface.. Electron. Notes Theor. Comput. Sci., 259, 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.
- Z2SAL: a translation-based model checker for Z. Formal Aspects of Computing, 1-29.
- Using Formal Specifications to Support Testing. ACM COMPUT SURV, 41(2). View this article in WRRO
- Preface.. Electron. Notes Theor. Comput. Sci., 214, 1-1.
- Preface.. Electron. Notes Theor. Comput. Sci., 201, 1-1.
- 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.
- Preface.. Electron. Notes Theor. Comput. Sci., 187, 1-1.
- Relational Concurrent Refinement with Internal Operations. Electronic Notes in Theoretical Computer Science, 187, 35-53.
- Guest Editorial.. Formal Asp. Comput., 18, 1-2.
- Filtering retrenchments into refinements. Proceedings - 4th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2006, 60-69.
- Editorial. International Journal of Business Performance Management, 8(1), 1-4. View this article in WRRO
- Introduction. Software and Systems Modeling, 4(3), 234-235.
- Guest Editorial Integrated Formal Methods.. Formal Asp. Comput., 17, 389-389.
- Preface.. Electron. Notes Theor. Comput. Sci., 137, 1-3.
- 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.
- Development of a verified Erlang program for resource locking.. Int. J. Softw. Tools Technol. Transf., 5, 205-220.
- Programming Methodology A. McIver and C. Morgan, editors, Springer-Verlag, 2002.. J. Funct. Program., 14, 597-598.
- Relational framework for the integration of specifications. Journal of Integrated Design and Process Science, 7(3), 39-48.
- 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.
- Using UML to specify QoS constraints in ODP. COMPUT NETW, 40(2), 279-304.
- A formal framework for viewpoint consistency. FORM METHOD SYST DES, 21(2), 111-166.
- ODP computational-to-information viewpoint mappings: a translation of CORBA IDL to Z.. IEE Proc. Softw., 149, 57-63.
- 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.
- Specification, refinement and verification of concurrent systems - An integration of Object-Z and CSP. FORM METHOD SYST DES, 18(3), 249-284.
- Analysis of a multimedia stream using stochastic process algebra. COMPUT J, 44(4), 230-245.
- Editorial: Special issue on specification-based testing. SOFTW TEST VERIF BEH, 10(4), 201-202.
- A single complete refinement rule for Z. J LOGIC COMPUT, 10(5), 663-675.
- Viewpoint consistency in ODP. COMPUT NETW, 34(3), 503-537.
- ODP enterprise viewpoint specification. COMP STAND INTER, 22(3), 165-189.
- 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), 577-578.
- Stochastic Model Checking for Multimedia. CoRR, cs.MM/0002004.
- Concurrent and Real-Time Systems: The CSP Approach, Steve Schneider, Wiley, 2000 (Book Review).. Softw. Test. Verification Reliab., 10, 195-195.
- Calculating upward and downward simulations of state-based specifications. INFORM SOFTWARE TECH, 41(13), 917-923.
- Constructive consistency checking for partial specification in Z. SCI COMPUT PROGRAM, 35(1), 29-75.
- Viewpoints and consistency: translating LOTOS to Object-z. COMP STAND INTER, 21(3), 251-272.
- Strategies for consistency checking based on unification. SCI COMPUT PROGRAM, 33(3), 261-298.
- 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.
- Cross-viewpoint consistency in open distributed processing. SOFTWARE ENG J, 11(1), 44-57.
- FDTS FOR ODP. COMP STAND INTER, 17(5-6), 457-479.
- Meeting of the Association for Symbolic Logic: Orleans, France, 1972.. J. Symb. Log., 39, 371-389.
- Meeting of the Association for Symbolic Logic Leeds 1967.. J. Symb. Log., 33, 490-490.
- 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
- Relational concurrent refinement - Partial and total frameworks, From Action Systems to Distributed Systems: The Refinement Approach (pp. 143-154).
- 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
- MoDeVVa 2018 15 th workshop on model-driven engineering, verification and validation. CEUR Workshop Proceedings, Vol. 2245 (pp 553-554)
- Preface. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE(282)
- 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)
- Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 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 126-141)
- Relational concurrent refinement part II: Internal operations and outputs. FORMAL ASPECTS OF COMPUTING, Vol. 21(1-2) (pp 65-102)
- Iterative Refinement of Reverse-Engineered Models by Model-Based Testing.. FM, Vol. 5850 (pp 305-320)
- Modelling Divergence in Relational Concurrent Refinement. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 5423 (pp 183-199)
- Applying Testability Transformations to Achieve Structural Coverage of Erlang Programs. TESTING OF SOFTWARE AND COMMUNICATION SYSTEMS, PROCEEDINGS, Vol. 5826 (pp 81-96)
- Mechanizing a correctness proof for a lock-free concurrent stack. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, Vol. 5051 (pp 78-95)
- Z2SAL-Building a Model Checker for Z. ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, Vol. 5238 (pp 280-293) View this article in WRRO
- Verifying Erlang telecommunication systems with the process algebra mu CRL. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2008, Vol. 5048 (pp 201-217)
- 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
- Verification of Timed Erlang/OTP Components Using the Process Algebra mu CRL. ERLANG'07: PROCEEDINGS OF THE 2007 SIGPLAN ERLANG WORKSHOP (pp 55-64)
- Proving linearizability via non-atomic refinement. Integrated Formal Methods, Proceedings, Vol. 4591 (pp 195-214)
- Verifying data refinements using a model checker. FORMAL ASPECTS OF COMPUTING, Vol. 18(3) (pp 264-287)
- Issues in implementing a model checker for Z. Formal Methods and Software Engineering, Proceedings, Vol. 4260 (pp 678-696)
- Model transformations incorporating multiple views. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, Vol. 4019 (pp 111-126)
- Non-atomic refinement in Z and CSP. ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, Vol. 3455 (pp 24-44)
- Formal program development with approximations. ZB 2005: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, PROCEEDINGS, Vol. 3455 (pp 374-392)
- Integrated Formal Methods, 4th International Conference, IFM 2004, Canterbury, UK, April 4-7, 2004, Proceedings. IFM, Vol. 2999
- Linear temporal logic and Z refinement. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, Vol. 3116 (pp 117-131)
- Recent advances in refinement. ABSTRACT STATE MACHINES 2003: ADVANCES IN THEORY AND PRACTICE, PROCEEDINGS, Vol. 2589 (pp 33-56)
- Using coupled simulations in non-atomic refinement. ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, Vol. 2651 (pp 127-147)
- Timed CSP and Object-Z. ZB 2003: FORMAL SPECIFICATION AND DEVELOPMENT IN Z AND B, Vol. 2651 (pp 300-318)
- Design and verification of distributed multi-media systems. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, Vol. 2884 (pp 276-292)
- Addressing computational viewpoint design. SEVENTH IEEE INTERNATIONAL ENTERPRISE DISTRIBUTED OBJECT COMPUTING CONFERENCE, PROCEEDINGS (pp 147-158)
- Design and Verification of Distributed Multi-media Systems.. FMOODS, Vol. 2884 (pp 176-292)
- Handling Inconsistencies in Z Using Quasi-Classical Logic.. ZB, Vol. 2272 (pp 204-225)
- Verifying Erlang Code: A Resource Locker Case-Study.. FME, Vol. 2391 (pp 184-203)
- Interpreting ODP Viewpoint Specification: Observations from a Case Study.. FMOODS, Vol. 209 (pp 61-76)
- Abstract Specification in Object-Z and CSP.. ICFEM, Vol. 2495 (pp 108-119)
- A UML approach to the design of open distributed systems. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Vol. 2495 (pp 561-572)
- 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)
- Guards, Preconditions, and Refinement in Z.. ZB, Vol. 1878 (pp 286-303)
- Liberating data refinement. MATHEMATICS OF PROGRAM CONSTRUCTION, Vol. 1837 (pp 144-166)
- Refinement of objects and operations in Object-Z. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS IV, Vol. 49 (pp 257-277)
- 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)
- Structural refinement in Object-Z/CSP. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 1945 (pp 194-213)
- Specification and analysis of automata-based designs. INTEGRATED FORMAL METHODS, PROCEEDINGS, Vol. 1945 (pp 176-193)
- Non-atomic refinement in Z. FM'99-FORMAL METHODS, VOL II, Vol. 1709 (pp 1477-1496)
- 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 293-312)
- A Junction between State Based and Behavioural Specification (Invited Talk).. FMOODS, Vol. 139 (pp 213-239)
- Stochastic Specification and Verification.. IWFM
- Consistency of partial process specifications. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, Vol. 1548 (pp 248-262)
- Testing refinements by refining tests. ZUM '98: THE Z FORMAL SPECIFICATION NOTATION, Vol. 1493 (pp 265-283)
- IO-refinement 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 177-192)
- Viewpoint Consistency in Z and LOTOS: A Case Study.. FME, Vol. 1313 (pp 644-664)
- Weak Refinement in Z.. ZUM, Vol. 1212 (pp 369-388)
- Refinement and Verification of Concurrent Systems Specified in Object-Z and CSP.. ICFEM (pp 293-303)
- Extending LOTOS with time: A true concurrency perspective. TRANSFORMATION-BASED REACTIVE SYSTEMS DEVELOPMENT, Vol. 1231 (pp 383-399)
- Formal specification and testing of a management architecture. INTEGRATED NETWORK MANAGEMENT V (pp 473-484)
- 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.
- Consistency and Refinement for Partial Specification in Z.. FME, Vol. 1051 (pp 287-306)
- Comparing LOTOS and Z Refinement Relations.. FORTE, Vol. 69 (pp 501-516)
- Formal description techniques for object management.. Integrated Network Management, Vol. 11 (pp 641-653)
- Composition of LOTOS specifications.. PSTV, Vol. 38 (pp 87-102)
- Viewpoints and Objects.. ZUM, Vol. 967 (pp 449-468)
- Modelling distributed systems using Z.. SAC (pp 147-151)
- A True Concurrency Semantics for Quality of Service Specification and Validation.. MMNET (pp 173-182)
- Modelling Garbage Collection Algorithms Using CCS and Temporal Logic (Abstract).. PODC (pp 394-394)
- Consistency and Conformance in ODP (Abstract).. PODC (pp 388-388)
- , 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
- Proving linearisability via coarse-grained abstraction
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.
- .
- 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
-
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: 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 Gap between Mathematics, ICT and Engineering Research at Sheffield, 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 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)