We develop compositional reasoning techniques for concurrent programs using modern concurrent separation logics, introducing fundamental concepts in the reasoning: logical abstraction (Concurrent Abstract Predicates), logical atomicity (the TaDA Logic) and logical environment liveness properties (TaDA Live). In addition, we have started to work on weak consistency models for distribution, developing an interleaving operational semantics for client-observational behaviour of atomic transactions (ECOOP’20).

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 Gardner’s UKRI Established Career Fellowship “VeTSpec: Verified Trustworthy Software Specification” and Emanuele D’Osualdo’s Marie-Curie Fellowship “VeSPA: Verification through Security and Progress Abstractions”. It was previously supported by the EPSRC programme grant EP/K008528/1: REMS: Rigorous Engineering of Mainstream Systems and the EPSRC programme grant EP/H008373/2: Resource Reasoning.

People

Recent Publications

  1. Parametric Operational Semantics for Consistency Models

    Ph.D. Thesis, Imperial College London

  2. Data Consistency in Transactional Storage Systems: a Centralised Approach

    34th European Conference on Object-Oriented Programming (ECOOP 2020)

  3. A Perspective on Specifying and Verifying Concurrent Modules

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

  4. A Concurrent Specification of POSIX File Systems

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

  5. Algebraic Laws for Weak Consistency

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

  6. 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)

  7. Abstraction, Refinement and Concurrent Reasoning

    Ph.D. Thesis, Imperial College London

  8. Reasoning with Time and Data Abstractions

    Ph.D. Thesis, Imperial College London

  9. Caper: Automatic Verification for Fine-grained Concurrency

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

  10. Abstract Specifications for Concurrent Maps

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