Martin Rinard

Credible Compilation

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).