Foundational Proof-Carrying Code Proof-Carrying Code (PCC) is
a static mechanism that mechanically verifies type safety of
machine-language programs. But the problem in conventional PCC is,
who will verify the verifier (the type checker) itself? The Foundational
Proof-Carrying Code (FPCC) project at Princeton verifies the
soundness of the type checker from the smallest possible set of axioms
--- logic plus machine semantics. One of the challenges in the
verification is that machine code, unlike high-level languages,
contains unstructured control flows (due to arbitrary jumps). A piece
of machine code contains multiple entry points that jump instructions
might jump to, and multiple exit points. Traditional Hoare logics
either verify the partial correctness of programs with only one entry
and one exit, or need the whole program to verify jump instructions,
which is not modular.
In my Ph.D. thesis work, I designed a logic that modularly verifies
properties of program fragments. The logic works directly on program
fragments with multiple entries and multiple exits. It provides
inference rules to combine fragments together and eliminate
intermediate entries and exits. I showed this logic to be both sound
and (relatively) complete with respect to a small-step machine
semantics. In the FPCC project, I used this logic to construct a
soundness proof for a full-fledged Typed Assembly Language (TAL). All
proofs were formally developed in a theorem prover and rigorously
A Compositional Logic for Control Flow. Gang Tan and Andrew W. Appel.
In Seventh International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 06), LNCS 3855, pages 80-94, Springer, January 2006.
Construction of a Semantic Model for
a Typed Assembly Language. Gang Tan, Andrew W. Appel, Kedar Swadi
and Dinghao Wu. In Fifth International Conference on Verification,
Model Checking and Abstract Interpretation (VMCAI 04), LNCS 2937,
pages 30-43, Springer, January 2004.
Last updated: Sep. 2007