The members of his committee are as follows: 

Adviser: Andrew Appel; Examiners: Lennart Beringer  and Arti Gupta; Readers: Lars Birkedal  (Aarhus University) and Zachary Kincaid

In our interconnected world, software bugs can seriously compromise our safety and

security. To provide adequate safety or protection, security-critical kernels (of large

systems) must be functionally correct.

To ensure functional correctness of C programs, we can use Hoare logic and its

extensions such as separation logic. But such correctness proofs are large and complex

enough that we cannot trust them unless they are machine-checked.

This dissertation shows how we can construct mechanized proofs of program correctness

using separation logic. I answer three questions: How shall we specify our

programs? How shall we prove our programs correct w.r.t. their specications? How

shall we mechanize such correctness proofs?

I present practical techniques for separation-logic-based program verication and

demonstrate them on several examples. I introduce VST-Floyd, a tool for users

to build formal C program correctness proofs in Coq using separation logic. VSTFloyd

is built based on Veriable C, a proved sound separation logic; I show how to

reformulate its rules to make them practical for use in verication. Finally, I introduce

a unifying semantics in separation logic so that research results of one separation logic

can be generalized to all separation logics. Thus the techniques used in VST-Floyd

can be used in other separation logics in the future.