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.