[Pl-seminar] 12/4: Andrew Appel, Program Logics for Certified Compilers

[Vincent St-Amour]

NUPRL Seminar presents

Andrew Appel
Princeton University

11:45 - 1:30
Wednesday, 12/4
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Program Logics for Certified Compilers

  Formal machine-checked program verification now scales all the way up
to correctness proofs of optimizing compilers for industrial-scale
languages such as C.  To take best advantage of compiler-correctness
proofs, we should prove correct the source programs that we feed
into these compilers, and compose the two proofs end-to-end.
This guarantees that the specified observable behavior we prove
at the source level, will actually hold of the machine-language
program that executes.

   We do this by designing a program logic for the source language,
such as Hoare logic but much more expressive to handle the
higher-order features found in real software (pointers, dynamically
allocated data structures, function pointers, objects, recursion).
Our program logic for "Verifiable C" connects to the CompCert verified
C compiler by X. Leroy et al.  We prove the program logic sound with
respect to the operational semantics of the program logic, and connect
this to the compiler-correctness proof that is w.r.t. the same
operational semantics.  Finally we build proof automation tools that
help the user apply the program logic to actual programs.

   I will talk about both the engineering issues and some of the
theoretical issues in building such a system.