We develop formal reasoning techniques for concurrent programs, with a particular emphasis on concurrent program logics. Recently, various logics based on separation logic have been developed, by ourselves and others, to provide more modular abstract reasoning about concurrent programs. Our work has tackled a range of problems including data abstraction, abstract atomicity, fault-tolerance and progress. In particular, we have recently developed Concurrent Abstract Predicates, Views, TaDA, CoLoSL, Fault-tolerant Concurrent Separation Logic and Total-TaDA.

We have applied our reasoning to, for example, algorithms for manipulating concurrent B-trees, skip lists from java.util.concurrent, graph algorithms and the POSIX file system. Our goal is to challenge and improve the state-of-the-art in concurrent reasoning, refining our logics to deal with more advanced concurrent programs, developing automated reasoning tools based on these logics, and applying our work to real-world concurrent programs.

Research Support

This research is supported by the EPSRC programme grant EP/K008528/1: REMS: Rigorous Engineering of Mainstream Systems and previously by the EPSRC programme grant EP/H008373/2: Resource Reasoning. We also have substantial collaboration with Thomas Dinsdale-Young, previously a PhD student and RA of Gardner and now an independent research fellow at the University of Aarhus.


Recent Publications

  1. A Perspective on Specifying and Verifying Concurrent Modules

    Journal of Logical and Algebraic Methods in Programming, vol. 98, pp. 1–25

  2. A Concurrent Specification of POSIX File Systems

    32nd European Conference on Object-Oriented Programming (ECOOP 2018).

  3. Algebraic Laws for Weak Consistency

    Proceedings of 28th International Conference on Concurrency Theory, (Concur 2017)

  4. Deciding Secrecy of Security Protocols for an Unbounded Number of Sessions: The Case of Depth-bounded Processes

    Proceedings of 30th IEEE Computer Security Foundations Symposium, (CSF 2017)

  5. Abstraction, Refinement and Concurrent Reasoning

    Ph.D. Thesis, Imperial College London

  6. Reasoning with Time and Data Abstractions

    Ph.D. Thesis, Imperial College London

  7. Caper: Automatic Verification for Fine-grained Concurrency

    Proceedings of the 26th European Symposium on Programming (ESOP’17), pp. 420–447

  8. Abstract Specifications for Concurrent Maps

    Proceedings of the 26th European Symposium on Programming (ESOP’17), pp. 964–990

  9. Reasoning About POSIX File Systems

    Ph.D. Thesis, Imperial College London

  10. Modular Termination Verification for Non-blocking Concurrency

    Proceedings of the 25th European Symposium on Programming (ESOP’16), pp. 176–201