Proof Procedures for Separated Heap Abstractions

Опубликовано 7 сентября 2016, 16:22

Separation logic is a program logic geared towards reasoning about programs that mutate heap-allocated data structures. This talk describes ideas arising from joint work with Josh Berdine and Cristiano Calcagno on proof procedure for a sublogic of separation logic that is oriented to lightweight program verification and analysis. The proof theory uses ideas from substructural logic together with induction-free reasoning about inductive definitions of heap structures. Substructural reasoning is used to to infer frame axioms, which describe the portion of a heap that is not altered by a procedure, as well as to discharge verification conditions; more precisely, the leaves of failed proofs can give us candidate frame axioms. Full automation is achieved through the use of special axioms that capture properties that would normally be proven using by induction. I will illustrate the proof method through its use in the Smallfoot static assertion checker, where it is used to prove verification conditions and infer frame axioms, as well as in the Space Invader program analysis, where it is used to accelerate the convergence of fixed-point calculations.