An Executable Semantics for CompCert C
No abstract available.
DOI 10.1007/978-3-642-35308-6_8
Related papers
- Verified peephole optimizations for CompCert PLDI 2016
- CompCert: A Journey through the Landscape of Mechanized Semantics for Verified Compilation (Keynote) CPP 2023
- An Iris Instance for Verifying CompCert C Programs POPL 2024
- Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler POPL 2023
- Formal Verification of an SSA-Based Middle-End for CompCert TOPLAS 2014
- A formally verified compiler for Lustre PLDI 2017
- A certified framework for compiling and executing garbage-collected languages ICFP 2010
- First Steps towards the Certification of an ARM Simulator Using Compcert CPP 2011