The Trusted Computing Base of the CompCert Verified Compiler
arXiv:2201.10280 · doi:10.1007/978-3-030-99336-8_8
Abstract
CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code. Yet, there could be loopholes in this approach. We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated. Possible issues range from the modeling of the source and the target languages to some techniques used to call external algorithms from within the compiler.
References in corpus (5)
- A formally verified compiler back-end
- A Static Analyzer for Large Safety-Critical Software
- The pitfalls of verifying floating-point computations
- Implementing and reasoning about hash-consed data structures in Coq
- Simple, Light, Yet Formally Verified, Global Common Subexpression Elimination and Loop-Invariant Code Motion