Programming languages and compilers researchers have attacked the problem of preventing software flaws from many angles, including type systems and other static analyses. However, to ensure that no bugs are introduced into the deployed system, some form of verification must be applied at all levels, from the source program and its specification, to the final assembly code running on the hardware. Applying formal verification techniques of this kind on the large scale are beyond our current technology, but much progress has been made since the problem was first articulated in the 1960's. Building a "verifying compiler" (one that proves the generated program is correct with respect to a formal specification) has been proposed by Tony Hoare as a Grand Challenge problem for Computer Science, and there is much active work in the area.

This course will survey the historic and current approaches to verifying compilation, focusing on the programming language and compiler aspects of the problem, but also touching on related subjects such as theorem proving and software model checking. The course material will primarily focus on the research literature, with papers presented both by the instructor and class participants. The reading selection will range from classics, such as Tony Hoare's 1969 paper "An Axiomatic Basis for Computer Programming" to more recent work such as Morrisett et al.'s "From System F to Typed Assembly Language".

Grades will be based on class participation, the presentation of papers in class, and (possibly) a course project.