[talks] Qinxiang Cao will present his FPO "Separation-Logic-Based Program Verification in Coq" on Wednesday, 8/8/2018 at 9am in CS 302.

[Nicki Gotsis]

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. 





-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.cs.princeton.edu/pipermail/talks/attachments/20180801/cc0485fb/attachment.html>