Verified compilation and its trusted boundary
Research context
research method · established · As of 2026-10-10
CompCert's principal semantic-preservation theorem relates accepted C abstract syntax to generated assembly abstract syntax: generated behavior refines permitted source behavior under the theorem's hypotheses.
Key knowledge
CompCert's principal semantic-preservation theorem relates accepted C abstract syntax to generated assembly abstract syntax: generated behavior refines permitted source behavior under the theorem's hypotheses. Its theorem does not make a source program's undefined behavior safe. Parsing/preprocessing, assembly/linking, runtime libraries, hardware and proof-checker trust have separate boundaries; testing a compiler sample is not a proof for every input.
Conditions and scope
- Use the formal language/target models and successful-compilation hypotheses of the exact theorem.
- The published proof and statement were inspected; this entry does not claim a new proof replay or verification of the full deployment chain.
Sources · 2
References
Sources retain their recorded scope. A source link alone does not establish verification of every statement.
Evidence and review
Author checked this English statement, displayed equation where present and stated hypotheses against these source locations: §1.2: permitted behavior preservation; C AST to assembly AST and compilation chain limits; transf_c_program_correct and separate-compilation theorem definitions. The check is bounded to the recorded claims; no complete proof reconstruction, software proof replay or universal literature completeness is claimed.
2026-10-10 · Author source-body/statement/equation/domain check, with graph associations scoped individually. Separate independent content/source/inventory review is required before branch closure.
Entry details
Permanent link to this entry ↗- Record identity
- research-info-compiler-semantic-preservation
- Revision
- research.1
- Structured reference record
- Postgraduate & research reference