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.

People

Recent Publications

  1. Caper: Automatic Verification for Fine-grained Concurrency

    Proceedings of the 26th European Symposium on Programming (ESOP)

  2. Abstract Specifications for Concurrent Maps

    Proceedings of the 26th European Symposium on Programming (ESOP)

  3. Modular Termination Verification for Non-blocking Concurrency

    Proceedings of the 25th European Symposium on Programming (ESOP)

  4. Verifying Concurrent Graph Algorithms

    Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings

  5. Fault-tolerant Resource Reasoning

    Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS)

  6. Reasoning about the POSIX File System: Local Update and Global Pathnames

    Proceedings of the 30th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)

  7. Steps in Modular Specifications for Concurrent Modules (Invited Tutorial Paper)

    Proceedings of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS)

  8. CoLoSL: Concurrent Local Subjective Logic

    Proceedings of the 24th European Symposium on Programming (ESOP)

  9. TaDA: A Logic for Time and Data Abstraction

    Proceedings of the 28th European Conference on Object-Oriented Programming (ECOOP)

  10. Local Reasoning for the POSIX File System

    Proceedings of the 23rd European Symposium on Programming (ESOP)