Published on *Computer Science Department at Princeton University* (http://www.cs.princeton.edu)

As it becomes more prevalent throughout our lives, correct software is more important than it has ever

been before. Verifiable C is an expressive Hoare logic (higher-order impredicative concurrent separation

logic) for proving functional correctness of C programs. The program logic is foundational—it is proved

sound in Coq w.r.t. the operational semantics of CompCert Clight. Users apply the program logic to C

programs using semiautomated tactics in Coq, but these tactics are very slow.

This thesis shows how to make an efficient (yet still foundational) symbolic executor based on this

separation logic by using computational reflection in several different ways. Our execution engine is able to

interact gracefully with the user by reflecting application-specific proof goals back to the user for interactive

proof—necessary in functional correctness proofs where there is almost always domain-specific reasoning

to be done. We use our “mostly sound” type system, computationally efficient finite-map data structures,

and the MirrorCore framework for computationally reflected logics. Measurements show a 40× performance

improvement.