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. It will deliver a new framework for verifying state-of-the-art memory managers, reusable for a wide range of managed programming languages, target hardware, policies, and algorithms. 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 also the nation's capability to safeguard and defend these assets by the necessary human resources.