Verified Software

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

   • Shale Xiong

   Ph.D. Thesis, Imperial College London

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

   • Shale Xiong
   • Andrea Cerone
   • Azalea Raad
   • Philippa Gardner

   Proceedings of the 34^th European Conference on Object-Oriented Programming (ECOOP 2020)

3. A Perspective on Specifying and Verifying Concurrent Modules

   • Thomas Dinsdale-Young
   • Pedro da Rocha Pinto
   • Philippa Gardner

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

4. A Concurrent Specification of POSIX File Systems

   • Gian Ntzik
   • Pedro da Rocha Pinto
   • Julian Sutherland
   • Philippa Gardner

   Proceedings of the 32^nd European Conference on Object-Oriented Programming (ECOOP 2018).

5. Algebraic Laws for Weak Consistency

   • Andrea Cerone
   • Alexey Gotsman
   • Hongseok Yang

   Proceedings of 28^th 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

   • Emanuele D’Osualdo
   • Luke Ong
   • Alwen Tiu

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

7. Abstraction, Refinement and Concurrent Reasoning

   • Azalea Raad

   Ph.D. Thesis, Imperial College London

8. Reasoning with Time and Data Abstractions

   • Pedro da Rocha Pinto

   Ph.D. Thesis, Imperial College London

9. Caper: Automatic Verification for Fine-grained Concurrency

   • Thomas Dinsdale-Young
   • Pedro da Rocha Pinto
   • Kristoffer Just Andersen
   • Lars Birkedal

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

10. Abstract Specifications for Concurrent Maps

    • Shale Xiong
    • Pedro da Rocha Pinto
    • Gian Ntzik
    • Philippa Gardner

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