DoC Researchers Advances Assurance in Dafny Compiler with Award-Winning Research

Prof Donaldson and his research team have achieved a significant breakthrough in enhancing the reliability of the Dafny programming language

In a collaboration with Amazon, Professor Alastair Donaldson and his research team at Imperial's Department of Computing have achieved a significant breakthrough in enhancing the reliability of the Dafny programming language. Dafny, known for its robust support of formal verification, is widely utilized by tech giants like Amazon and VMWare for developing high-assurance software.

The research project, funded in part by two prestigious Amazon Research Awards and supported by the IRIS EPSRC Programme Grant, focuses on fortifying the Dafny compiler against potential vulnerabilities that could compromise the correctness of formally verified programs. Despite the language's strengths in mathematical verification techniques, the team identified a critical area for improvement: compiler bugs.

"Formally verified programs in Dafny can only be as reliable as the compiler itself," explains Professor Donaldson. "Our research addresses this challenge by leveraging automated randomised testing to systematically detect and rectify flaws within the Dafny compiler."

The culmination of their efforts was recently presented at the International Conference on Software Testing, Verification and Validation (ICST), where their paper, featured in the Industry Track, earned the prestigious Best Paper Award. This recognition underscores the importance of their findings in advancing the field of software reliability and formal methods.

"By automating the detection of compiler bugs, so that they can be fixed before they affect end users, we aim to further enhance the trustworthiness of Dafny-based software systems," adds Professor Donaldson. "Our collaboration with Amazon has been a satisfying demonstration of the real-world impact that software testing research can have."

For more information on this research and its implications for the future of high-assurance software development, you can read the full paper here.