Showing 1–1 of 1 results for author: Boulmé, S

The Trusted Computing Base of the CompCert Verified Compiler

Authors: David Monniaux, Sylvain Boulmé

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 som… ▽ More 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. △ Less

Submitted 10 October, 2022; v1 submitted 25 January, 2022; originally announced January 2022.

Journal ref: Programming Languages and Systems (ESOP 2022), Apr 2022, Munich, Germany. pp.204-233