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
91Ö±²¥
S1 4DP
School of Computer Science
Regent Court (DCS)
211 Portobello
91Ö±²¥
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 91Ö±²¥ 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
- . Springer International Publishing.
- . Springer-Verlag New York Inc.
- . Springer.
- . Springer London.
- Refinement in Z and Object-Z. Springer Verlag.
- . Elsevier.
Edited books
- Formal Methods for Distributed Processing: A Survey of Object-Oriented Approaches. Cambridge Univ Press.
Journal articles
- Preface to the 21th edition of the Workshop on Model Driven Engineering, Verification and Validation (MoDeVVa 2024). Proceedings: MODELS 2024 - ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems: Companion Proceedings, lxviii-lxix.
- . Formal Aspects of Computing.
- . Science of Computer Programming.
- . Formal Aspects of Computing, 30(5), 597-625.
- . Empirical Software Engineering, 21(3), 811-853.
- . Science of Computer Programming, 111, 214-247.
- . ACM Computing Surveys, 48(2), 1-43.
- . ACM Transactions on Computational Logic, 15(4), 1-37.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8855.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8687, 151-168.
- . Formal Aspects of Computing, 1-1.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 8442 LNCS, 200-214.
- . Science of Computer Programming.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7358 LNCS, 243-259.
- . Formal Aspects of Computing, 1-26.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 7316 LNCS.
- . 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.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6664 LNCS, 323-337.
- . Science of Computer Programming, 76(9), 737-738.
- . ACM Transactions on Programming Languages and Systems, 33(1).
- . AUTOMAT SOFTW ENG, 17(1), 33-56.
- . SCI COMPUT PROGRAM, 75(12), 1262-1269.
- . SCI COMPUT PROGRAM, 75(3), 192-210.
- . 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.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6286 LNCS, 272-289.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 6286 LNCS, 250-271.
- . FORM ASP COMPUT, 22(1), 1-1.
- . FORM ASP COMPUT, 21(1-2), 1-1.
- Preface.. Electron. Notes Theor. Comput. Sci., 259, 1-1.
- . Electronic Notes in Theoretical Computer Science, 259(C), 21-34.
- . Formal Aspects of Computing, 21(1-2), 1.
- Z2SAL: a translation-based model checker for Z. Formal Aspects of Computing, 1-29.
- . ACM COMPUT SURV, 41(2).
- Preface.. Electron. Notes Theor. Comput. Sci., 214, 1-1.
- Preface.. Electron. Notes Theor. Comput. Sci., 201, 1-1.
- . Electronic Notes in Theoretical Computer Science, 214(C), 255-276.
- . Electronic Notes in Theoretical Computer Science, 201(C), 155-175.
- . ACTA INFORM, 44(1), 41-71.
- Preface.. Electron. Notes Theor. Comput. Sci., 187, 1-1.
- . Electronic Notes in Theoretical Computer Science, 187, 35-53.
- Guest Editorial.. Formal Asp. Comput., 18, 1-2.
- . 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.
- . 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.
- . Electronic Notes in Theoretical Computer Science, 137(2), 205-224.
- . 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.
- . Formal Aspects of Computing, 15(1), 1-27.
- . Formal Aspects of Computing, 15(2-3), 182-214.
- . 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.
- . Electronic Notes in Theoretical Computer Science, 70(3), 94-131.
- . Electronic Notes in Theoretical Computer Science, 70(3), 331-332.
- . 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.
- . Software Testing Verification and Reliability, 9(1), 27-50.
- . IEE Proceedings: Software, 145(2-3), 61-69.
- . 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.
- . Logical Methods in Computer Science, Volume 18, Issue 3.
- . Electronic Proceedings in Theoretical Computer Science, 282.
- . Electronic Proceedings in Theoretical Computer Science, 209.
- . Electronic Proceedings in Theoretical Computer Science, 115, 15-35.
- . Electronic Proceedings in Theoretical Computer Science, 115.
- . Computer Standards and Interfaces.
- . Electronic Proceedings in Theoretical Computer Science, 55.
Chapters
- , Lecture Notes in Computer Science (pp. 26-47). Springer Nature Switzerland
- , From Astrophysics to Unconventional Computation (pp. 195-206). Springer International Publishing
- , Lecture Notes in Computer Science (pp. 179-195). Springer International Publishing
- , Software Engineering and Formal Methods (pp. 257-272). Springer International Publishing
- , Formal Methods and Software Engineering (pp. 373-387). Springer International Publishing
- , 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).
- , ZUM ’98: The Z Formal Specification Notation (pp. 265-283). Springer Berlin Heidelberg
- , IFIP Advances in Information and Communication Technology (pp. 399-406). Springer US
- , IFIP Advances in Information and Communication Technology (pp. 189-204). Springer US
- , IFIP Advances in Information and Communication Technology (pp. 335-351). Springer US
- , Testing of Communicating Systems (pp. 93-114). Springer US
- , Open Distributed Processing (pp. 399-412). Springer US
- , Open Distributed Processing (pp. 413-424). Springer US
Conference proceedings papers
- . Testing Software and Systems (pp 37-54). London, UK (virtual), 10 November 2021 - 11 November 2021.
- . 35th International Symposium on Distributed Computing (DISC 2021), Vol. 209 (pp 55:1-55:4). Freiburg, Germany, 4 October 2021 - 8 October 2021.
- (pp 39-58)
- . Proceedings of the 24th Symposium on Principles and Practice of Parallel Programming (pp 355-365)
- . Leibniz International Proceedings in Informatics, LIPIcs, Vol. 121
- . 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE) (pp 100-107), 29 August 2018 - 31 August 2018.
- . Integrated Formal Methods, Vol. 11023 LNCS (pp 110-129), 5 September 2018 - 7 September 2018.
- 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)
- . Lecture Notes in Computer Science (pp 108-123), 19 June 2017 - 22 June 2017.
- . Leibniz International Proceedings in Informatics, LIPIcs, Vol. 70 (pp 35.1-35.17), 13 December 2016 - 16 December 2016.
- . Software Engineering and Formal Methods. SEFM 2016. Lecture Notes in Computer Science, Vol. 9763 (pp 45-60)
- . Proceedings of the 31st Annual ACM Symposium on Applied Computing - SAC '16, 4 April 2016 - 8 April 2016.
- . 2016 24th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP), 17 February 2016 - 19 February 2016.
- (pp 178-193)
- . Proceedings of the 14th ACM SIGPLAN Workshop on Erlang - Erlang 2015, 4 September 2015 - 4 September 2015.
- . Leibniz International Proceedings in Informatics, LIPIcs, Vol. 37 (pp 470-494)
- (pp 178-194)
- (pp 161-177)
- (pp 364-383)
- . Proceedings - ICACSIS 2014: 2014 International Conference on Advanced Computer Science and Information Systems (pp 225-231). Jakarta, Indonesia, 18 October 2014 - 19 October 2014.
- . Proceedings of the Thirteenth ACM SIGPLAN workshop on Erlang (pp 73-74), 5 September 2014 - 5 September 2014.
- (pp 200-214)
- . Integrated Formal Methods. IFM: International Conference on Integrated Formal Methods, Vol. 8739 (pp 341-356)
- . Electronic Communications of the EASST, Vol. 66
- . 2013 20th Working Conference on Reverse Engineering (WCRE), 14 October 2013 - 17 October 2013.
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 8049 LNCS (pp 177-194)
- . Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 7940 LNCS (pp 253-267)
- . 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)
- . 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)
- 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)
- . 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)
- . 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)
- . Electronic Workshops in Computing
- . 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)
- . 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)
- . 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
- . 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 91Ö±²¥ Engineering Symposium.
Other
- .
Preprints
- Proceedings 18th Refinement Workshop, arXiv.
- Data refinement for true concurrency, arXiv.
- Proceedings 16th International Refinement Workshop, arXiv.
- , Proceedings 15th International Refinement Workshop, Refine@FM 2011, Limerick, Ireland, 20th June 2011..
- Proceedings 15th International Refinement Workshop, arXiv.
- .
- . Springer International Publishing.
- Research group
-
If you are interested in doing a PhD with Prof. John Derrick then please take a look at the
- Grants
-
Research Grants
- (COVERT), EPSRC, 07/2023 - 11/2026, £422,585, as PI
- , EPSRC, 10/2018 - 08/2022, £397,680, as PI
- , EPSRC, 03/2018 - 02/2020, £17,123, as PI
- , EPSRC, 05/2015 - 11/2018, £389,207, as PI
- PROWESS: , EC FP7, 10/2012 - 10/2015, £405,800, as PI
- , EPSRC, 04/2012 - 10/2015, £378,907, as PI
- Decision Support Tool, BAE Systems Plc, 07/2011 - 12/2011, £51,895, as PI
- , EPSRC, 07/2009 - 10/2012, £318,522, as PI
- ProTest: , EC FP7, 05/2008 - 12/2011, £277,503, as PI
- Bridging the Gap between Mathematics, ICT and Engineering Research at 91Ö±²¥, 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)