Toward automated compiler verification
Raymond J. Toal · 1993
This research examines the Compiler Correctness Problem in the context of operational semantics and higher-order logic, and investigates an approach to automating the verification of compiler specifications. The work aims at simplifying the task of proving translation correctness for compiler designers, who are usually neither logicians nor semanticists. This dissertation makes three important contributions. The first is a formalization of the compiler specification correctness problem in an operational semantic setting that is shown to be close to an intuitive notion of a semantics-preserving translation. Formal statements in higher-order logic, adequate to express translation correctness for a class of optimizing compilers, are motivated and justified. The second is a solution to the problem of relating the operational semantics of the source and target languages of a translation. We show how to mechanize the derivation of an inductive characterization of compiled code, reducing the compiler correctness problem to a semantic equivalence problem. The third is the introduction of a methodology for proving compiler specification correctness, together with the implementation of mechanized procedures that automate much of the verification effort. Provided that certain behavioral assertions describing properties of compiled code are supplied, our method simplifies proof goals in a manner that mirrors the execution of source and target language programs. Our work, then, provides a means of constructing partially automated proofs of compiler specification correctness, taking advantage of the simplicity of operational semantics and the expressiveness of higher-order logic.