Qinxiang Cao will present his FPO "Separation-Logic-Based Program Verification in Coq" on Wednesday, 8/8/2018 at 9am in CS 302. 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 Everyone is invited to attend his talk. The talk abstract follow below. 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.