Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language

Explore a groundbreaking methodology for enhancing the trustworthiness of automated program verifiers in this 18-minute video presentation from PLDI 2024. Delve into the novel approach of formally validating translations into intermediate verification languages (IVLs) like Boogie or Why3. Learn how researchers from ETH Zurich, Université Grenoble Alpes, and the University of British Columbia developed a technique to automatically generate Isabelle proofs, ensuring that the correctness of IVL programs implies the correctness of input programs. Discover the challenges of bridging the semantic gap between input languages and IVLs, and how modularisation strategies address these complexities. Gain insights into the implementation and evaluation of this methodology using the Viper and Boogie languages, demonstrating its effectiveness in validating translations performed by existing Viper implementations. Understand the implications for achieving end-to-end soundness in program verification tools and the potential impact on software reliability and security.