CompCert compiler

[Google Scholar] [Website] [Wikipedia]

Notes: Coq theorem prover, translation validation, verified compilers
Papers: leroy:cacm:2009

CompCert is an optimizing compiler for a large subset of C that has been formally verified using the Coq theorem prover. Passes in CompCert were either verified as correct for any input or using translation validation.

Translation validation, Verified compilers

  • CertiKOS: An extensible architecture for building certified concurrent OS Kernels [gu:osdi:2016]
  • Formal verification of a realistic compiler [leroy:cacm:2009]
  • CompCertTSO: A verified compiler for relaxed-memory concurrency [sevcik:jacm:2013]
  • überSpark: Enforcing verifiable object abstractions for automated compositional security analysis of a hypervisor [vasudevan:usenix:2016]