Design and verification of correct, efficient and secure concurrent systems

该项目旨在提供设计和验证正确，安全和高效的并发软件的方法，这些软件是可扩展的和机械化的。具有多个处理器的计算机现在已成为标准，并用于广泛的安全、安保和使命关键软件应用，如运输、卫生和基础设施。这些多核架构有可能带来重要的效率提升，但可能会引入使用传统软件开发方法无法管理的复杂且容易出错的行为。该项目将为此类软件的设计和验证提供更好的、可扩展的和机械化的方法，预计将减少高效现代软件的故障率。

This project aims to provide methods for the design and verification of correct, secure and efficient concurrent software that are scalable and mechanised. Computers with multiple processors are now the norm and are used in a wide range of safety, security and mission critical software applications such as transport, health and infrastructure. These multi-core architectures have the potential to lead to important efficiency gains, but can introduce complex and error-prone behaviours that cannot be managed using traditional software development approaches. This project will produce better, scalable and mechanised methods for the design and verification of such software which is expected to reduce the prevalence of failures in efficient, modern software.