HackerPapers

arXiv:2201.10280cs.LO

The Trusted Computing Base of the CompCert Verified Compiler

David Monniaux, Sylvain Boulmé

HN submission. Found in a submission link or body. Submitters do not count as commenters in the main ranking; a submission is not an endorsement.

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.

arXiv comments
Journal reference
Programming Languages and Systems (ESOP 2022), Apr 2022, Munich, Germany. pp.204-233
DOI
doi:10.1007/978-3-030-99336-8_8
Subjects
cs.LOLogic in Computer Science cs.PLProgramming Languages

On Hacker News

No comments linking this paper were found in the collected sources. Found in 1 HN submission from Feb 2022 to Feb 2022. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments0 threads

No comments linking this paper were found in the collected sources. Open submission discussions.

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.