Instead of simply producing an executable, a credible compiler also produces a proof that the compiler correctly compiled the program. Goals include increasing trust in the compiler, enabling more aggressive optimizations, and supportng the safe incorporation of code from multiple people and organizations in the compiler.
This research produced the first relational program logic, a logic for proving relationships between two programs. The credible compilation project used relational logic to prove the correctness of the translation between the source and target program. Relational program logics have since been used for a wide variety of tasks in program analysis and verification and software engineering. My research group, for example, has used relational logic to prove relational acceptability properties of approximate programs (see our PLDI 2012 paper for more information).
Presents the formal foundations and architectural design of a credible compiler, or a compiler that, in addition to a transformed program, produces a proof that the transformed program correctly implements the original input program. Typically, the correctness proof will consist of two subproofs: a subproof that the analysis of the input program produced a correct result, and a subproof that establishes a simulation relation between the original and transformed programs. The paper presents two logics, one for each kind of subproof, and shows that the logics are sound.
A novel and important feature of our framework is its simultaneous support for both formal reasoning and sophisticated compiler transformations that deal with the program and the target machine at a very low level. In particular, our logics allow the compiler to prove the correctness of low-level optimizations such as register allocation and instruction scheduling even in the presence of potentially aliased pointers into the memory of the machine.
Presents the formal foundations of a credible compiler, or a compiler that, in addition to a transformed program, produces a proof that the transformed program correctly implements the original input program. Typically, the correctness proof will consist of two subproofs: a subproof that the analysis of the input program produced a correct result, and a subproof that establishes a simulation relation between the original and transformed programs. The paper presents two logics, one for each kind of subproof, and shows that the logics are sound.