[Pl-seminar] 12/4: Andrew Appel, Program Logics for Certified Compilers
stamourv at ccs.neu.edu
Wed Nov 27 10:36:50 EST 2013
NUPRL Seminar presents
11:45 - 1:30
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.
More information about the pl-seminar