Skip navigation
Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp01qn59q6317
 Title: Verified Separate Compilation for C Authors: Stewart, James Gordon Advisors: Appel, Andrew W Contributors: Computer Science Department Keywords: interactive theorem provingseparate compilationverified 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. URI: http://arks.princeton.edu/ark:/88435/dsp01qn59q6317 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 PDF

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