[talks] Gordon Stewart: Pre-FPO talk announcement (5/12 at 9:30 in Room 302)

Nicki Gotsis ngotsis at CS.Princeton.EDU
Mon May 5 09:33:56 EDT 2014

Gordon Stewart will present his Pre-FPO on Monday, May 12 at 9:30am in Room 302 in the Computer Science Building.

The members of his committee are: Andrew Appel (advisor); Zhong Shao and David Walker (readers); David August and Sharad Malik (nonreaders). 

Everyone is invited to attend his talk.  The talk title and abstract follow below:

Title: Verified Separate Compilation for C

Verified separate compilation is the process of independently
translating a program's components in a way that preserves correctness
of the program as a whole. In the most general case, a verified
separate compiler supports heterogeneous source programs, in which
some modules are in C or another high-level language while others are
written in a lower-level language like x86 assembly, as is common in
systems software such as operating systems.  A verified separate
compiler in this context is one that preserves the behavior of the
entire source program, comprising the C and x86 modules, when the C
code is compiled to assembly.

Separate compilation has numerous practical benefits. It speeds up
development cycles by enabling re-compilation of just those source
modules that have been edited by the programmer. It enables shared
libraries---separately compiled modules mapped at runtime into the
virtual address spaces of multiple processes.  It promotes modularity
in the large, by enabling programmers to write applications containing
logically distinct translation units, each composed at a different
level of abstraction or even in a different programming language

But perhaps equally important are applications of verified separate
compilers to /modular verification/, the act of reasoning
independently about each module in a program (with respect to
specifications of the other modules) in order to prove whole program
correctness. A modular verification approach means the programmer can
break the task of proving correctness of large programs into smaller,
more manageable steps: First provide specifications of the modules
that form the program, then prove independently of each module that
the module meets its specification. When modules proved correct in
this way are compiled by a semantics-preserving separate compiler, one
gets not only that each module is translated correctly to assembly and
then machine code, but also that the target whole program---linked and
running on the machine---has the same behavior as the source whole
program about which the programmer proved a correctness
specification. The result is an end-to-end system: Whole program
properties proved modularly at the source level are true also of the
whole program that results from separate compilation and linking.

In this thesis, I present techniques that address the verified
separate compilation problem in the context of C-like languages.  My
work extends state-of-the-art verified compilers for C such as
CompCert (http://compcert.inria.fr/)---the correctness proof of which
is currently limited to whole programs---to support verified separate
compilation. Major results of the thesis are the proof of a separate
compilation theorem for C and the novel semantics of inter-language
linking on which the statement of the separate compilation theorem
depends. I also address applications to verified compilation of
coarse-grained concurrent programs, revealing surprising connections
between separate compilation and concurrency in the process. To
validate the separate compilation result, I show that it supports
modular verification of source programs in the Verified Software
Toolchain program logic for C (http://vst.cs.princeton.edu/).

More information about the talks mailing list