Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…)
summary
Adds a per-run Isabelle certificate generator to an existing Viper→Boogie translation, proving that whenever the generated Boogie program has no failing executions the original Viper program also has none. The method uses forward-simulation proofs, modularising the large semantic gap (heap, permissions, expression failure) and handling optimized, context-dependent encodings. Implementation alters the translator with roughly a few hundred lines plus boilerplate and produces certificates for 72 benchmarks, all of which Isabelle successfully checks.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:23Frontend soundness in translations
- 2:50Key contributions
- 4:15Frontend translation challenges
- 7:30Non-local reasoning in methods
- 9:15Certificate generation
- 13:10Certifying translation evaluation
- 14:12Conclusion & Q&A
related talks
59mCompiler-assisted Translation Validation
01h 06mVerifying a compiler through equational means
01h 02mLanguage Design meets Verifying Compilers
19mFormally Verifying Optimizations with Block Simulations
29mTowards Formally Verified Just-In-Time Compilation
50mCompCert: a journey through the landscape of mechanized semantics for verified co...
01h 01mMulti-Modal Verification of Distributed Systems in Lean
19mAn Iris Instance for Verifying CompCert C Programs