CompCert

Reference 1

CompCert: A realistic, verified compiler.

By verified, we mean a compiler that is accompanied by a machine-checked proof of a semantic preservation property: the generated machine code behaves as prescribed by the semantics of the source program.

By realistic, we mean a compiler that could realistically be used in the context of production of critical software.

Background

The first compiler proof in 19672, for the compilation of arithmetic expressions down to stack machine code; and mechanically verified in 19723.

A survey of compiler verification 4.

  1. Formal verification of a realistic compiler. by Xavier Leroy. 2008. ↩
  2. Correctness of a compiler for arithmetical expressions. J. McCarthy and J. Painter. Mathematical Aspects of Computer Science. 1967. ↩
  3. Proving Compiler correctness in a mechanized logic. By R. Milner and R. Weyhrauch. 1972. ↩
  4. Compiler verification: a bibliography. M. A. Dave. SIGSOFT Softw. Eng. 2003. ↩
Created Oct 5, 2019 // Last Updated May 10, 2021

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?