<html><body><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000"><div>Qinxiang Cao will present his FPO "Separation-Logic-Based Program Verification in Coq" on <span data-mce-style="font-size: 12pt;" style="font-size: 12pt;">Wednesday, 8/8/2018 at 9am in CS 302. </span></div><div><span data-mce-style="font-size: 12pt;" style="font-size: 12pt;"><br data-mce-bogus="1"></span></div><div><span data-mce-style="font-size: 12pt;" style=""><div>The members of his committee are as follows: </div><div>Adviser: Andrew Appel; Examiners: Lennart Beringer and Arti Gupta; Readers: Lars Birkedal (Aarhus University) and Zachary Kincaid</div></span></div><div><div><br data-mce-bogus="1"></div><div></div><div>Everyone is invited to attend his talk. The talk abstract follow below.</div></div><div><br></div><div><span data-mce-style="font-size: 12pt;" style=""><div>In our interconnected world, software bugs can seriously compromise our safety and</div><div>security. To provide adequate safety or protection, security-critical kernels (of large</div><div>systems) must be functionally correct.</div><div>To ensure functional correctness of C programs, we can use Hoare logic and its</div><div>extensions such as separation logic. But such correctness proofs are large and complex</div><div>enough that we cannot trust them unless they are machine-checked.</div><div>This dissertation shows how we can construct mechanized proofs of program correctness</div><div>using separation logic. I answer three questions: How shall we specify our</div><div>programs? How shall we prove our programs correct w.r.t. their speci cations? How</div><div>shall we mechanize such correctness proofs?</div><div>I present practical techniques for separation-logic-based program veri cation and</div><div>demonstrate them on several examples. I introduce VST-Floyd, a tool for users</div><div>to build formal C program correctness proofs in Coq using separation logic. VSTFloyd</div><div>is built based on Veri able C, a proved sound separation logic; I show how to</div><div>reformulate its rules to make them practical for use in veri cation. Finally, I introduce</div><div>a unifying semantics in separation logic so that research results of one separation logic</div><div>can be generalized to all separation logics. Thus the techniques used in VST-Floyd</div><div>can be used in other separation logics in the future.</div><div><br></div></span></div><div><span data-mce-style="font-size: 12pt;" style="font-size: 12pt;"></span><br>
<p></p><br></div></div></body></html>