Skip navigation
Please use this identifier to cite or link to this item:
Title: Verified Separate Compilation for C
Authors: Stewart, James Gordon
Advisors: Appel, Andrew W
Contributors: Computer Science Department
Keywords: interactive theorem proving
separate compilation
verified compilers
Subjects: Computer science
Issue Date: 2015
Publisher: Princeton, NJ : Princeton University
Abstract: A separate compiler independently translates a program's components in a way that preserves correctness of the program as a whole. This dissertation develops techniques and tools for verified (mechanically proved) separate compilation of programs in C. Specifying and proving separate compilation for C is made challenging by the coincidence of: compiler optimizations, such as register spilling, that introduce compiler-managed (private) memory regions into function stack frames, and C's stack-allocated addressable local variables, which may \emph{leak} portions of stack frames to other modules when their addresses are passed as arguments to external function calls. The CompCert compiler, as built/proved by Leroy et al. 2006--2015 and upon which this dissertation builds, has proofs of correctness for whole programs, but its simulation relations are too weak to specify or prove separately compiled modules. The main contributions of the dissertation are: (i) language-independent linking, a new operational model of multilanguage module interaction that supports the statement and proof of cross-language contextual equivalence; (ii) structured simulations, a program-equivalence proof method that enables expressive module-local invariants on the state communicated between compilation units at runtime; (iii) the application of the above techniques to Compositional CompCert, a verified separate compiler for C. As additional validation, the dissertation demonstrates the connection of Compositional CompCert to the Verifiable C program logic.
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 
Stewart_princeton_0181D_11274.pdf1.44 MBAdobe PDFView/Download

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