Skip navigation
Please use this identifier to cite or link to this item:
Title: Computation Improves Interactive Symbolic Execution
Authors: Dodds, Joey
Advisors: Appel, Andrew W
Contributors: Computer Science Department
Keywords: Coq
Formal Methods
Programming Languages
Symbolic Execution
Subjects: Computer science
Issue Date: 2015
Publisher: Princeton, NJ : Princeton University
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.
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Computer Science

Files in This Item:
File Description SizeFormat 
Dodds_princeton_0181D_11583.pdf548.4 kBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.