Compositional CompCert
Abstract
This paper reports on the development of Compositional CompCert, the first verified separate compiler for C.
DOI 10.1145/2676726.2676985
Related papers
- An abstract stack based approach to verified compositional compilation to machine code POPL 2019
- CompCertM: CompCert with C-assembly linking and lightweight modular verification POPL 2020
- Lightweight verification of separate compilation POPL 2016
- CompCertO: compiling certified open C components PLDI 2021
- A Compositional Semantics for Verified Separate Compilation and Linking CPP 2015
- Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules POPL 2024
- CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks PLDI 2025
- Denotation-based Compositional Compiler Verification TOPLAS 2026