Verified concurrent memory management on modern processors

这个项目旨在正式验证并发和现代处理器的弱有序内存存在的自动内存管理器。将开发一个用于验证内存管理器的新框架，该框架可用于广泛的托管编程语言、目标硬件、策略和算法。预期的技术成果包括改进的技术，以确保构建关键软件基础设施的基础的可靠性。这将显著增强公共和私人网络资产的安全性，并在交通、通信、能源和国防等一系列关键基础设施中提供更强大、更值得信赖的应用程序。

This project aims to formally verify automatic memory managers in the presence of concurrency and the weakly ordered memory of modern processors. A new framework for verifying memory managers, reusable for a wide range of managed programming languages, target hardware, policies, and algorithms will be developed. Expected technical outcomes include improved techniques to ensure trustworthiness of the foundations on which critical software infrastructures are built. This will significantly enhance the security of public and private cyber assets, and deliver applications that are more robust and trustworthy, across a range of critical infrastructure such as transportation, communication, energy and defence.