Paper Info
Title
<Emphasis Type="SmallCaps">CompCertS</Emphasis>: A Memory-Aware Verified C Compiler Using a Pointer as Integer Semantics
Abstract
The CompCert C compiler provides the formal guarantee that the observable behaviour of the compiled code improves on the observable behaviour of the source code. In this paper, we present a formally verified C compiler, CompCertS, which is essentially the CompCert compiler, albeit with a stronger formal guarantee: it gives a semantics to more programs and ensures that the memory consumption is preserved by the compiler. CompCertS is based on an enhanced memory model where, unlike CompCert but like Gcc, the binary representation of pointers can be manipulated much like integers and where, unlike CompCert, allocation may fail if no memory is available. The whole proof of CompCertS is a significant proof-effort and we highlight the crux of the novel proofs of 12 passes of the back-end and a challenging proof of an essential optimising pass of the front-end.
Year
DOI
Venue
2017
10.1007/s10817-018-9496-y
Journal of Automated Reasoning
Keywords
Field
DocType
Verified compilation, Low-level code, Optimisations, Pointer as integer
Pointer (computer programming),Function pointer,Programming language,Escape analysis,Source code,Computer science,Compiler correctness,Parallel computing,Compiled language,Compiler,Memory model
Conference
Volume
Issue
ISSN
10499
2
1573-0670
Citations 
PageRank 
References 
2
0.37
8
Authors
3
Name
Order
Citations
PageRank
Frédéric Besson121316.86
S. Blazy2366.66
Pierre Wilke3102.61