[talks] Qinxiang Cao will present his Pre FPO, "Separation-logic-based program verification in Coq" on Thursday, December 14th, 2017 at 8am in CS 402.
ngotsis at CS.Princeton.EDU
Mon Nov 27 19:21:52 EST 2017
Qinxiang Cao will present his Pre FPO, "Separation-logic-based program verification in Coq" on Thursday, December 14th, 2017 at 8am in CS 402.
The members of his committee are as follows:
Andrew W. Appel (advisor), Lars Birkedal (Aarhus University), Zachary Kincaid (reader), Aarti Gupta (non-reader) and Lennart Beringer (non-reader).
Everyone is welcome to join. Talk title and abstract follow below.
"Separation-logic-based program verification in Coq"
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’ correctness w.r.t. their specifications? How shall we mechanize such correctness proofs?
In this dissertation, I present practical techniques for separation-logic-based program verification 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. VST-Floyd is built based on Verifiable C, a proved sound separation logic; I show how to reformulate its rules to make them practical for use in verification. 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.
More information about the talks