Design and verification of correct, efficient and secure concurrent systems (2019-2023)

Todays software must be correct and secure, but it must also be fast: written to take advantage of modern multi-core architectures. Complex interactions between concurrent processes are needed to achieve efficiency, but can easily compromise correctness and security. For software deployed on millions of devices, or that is used to control critical infrastructure, the consequences can be devastating. Traditional development methods cannot cope with the complexity and scale of such software applications. The project aims to provide methods for the design and verification of correct, secure and efficient concurrent software that are scalable and mechanised. They are expected to reduce the prevalence of failures in efficient, modern software.