Computation Improves Interactive Symbolic Execution

Abstract

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 40x

performance improvement.