Nikos Gkorogiannis

Title: Reasoning about the program heap

Abstract:
Separation logic (SL) is a recent development aimed at verifying programs that use dynamic allocation/pointers, a known headache for decades.  I will give a high-level overview of what SL is and how it helps with verification.  Then I will present my work on SL covering topics such as: decidability for the satisfiability problem; undecidability for the entailment problem; theorem proving using cyclic proof; inferring recursive specifications from bare code; and, checking invalidity using heuristics.  The talk will be high-level and no prior familiarity with SL will be assumed (but a little bit of logic always helps).