Tutorial on Separation Logic Seminars/Workshops

Abstract

June 25: An Introduction to Separation Logic
Abstract: The separation logic is an extension of Hoare logic that permits reasoning about pointers. A notable difference of the logic from other reasoning formalisms for pointers is that assertions are extended with spatial conjunction and implication in the logic;intuitively, a spatial conjunction P*Q says that the current heap can be split into two so that P holds for the one and Q for the other, and a spatial implication P-*Q says that whenever a new heap satisfying P is added to the current heap, the combined old and new heap makes Q true. These spatial connectives permit simple proof rules for pointer manipulations, such as deallocation of a heap cell. In this talk, I will explain spatial connectives and proof rules using the connectives. I will mainly focus on how the logic works by giving example proofs, instead of giving theoretical reasons about why the logic works.

June 26: Frame Rule and Local Reasoning
Abstract: When a programmer writes a single procedure in a big program, it is a common practice that he concentrates only on those memory cells that a procedure accesses. Local reasoning is a style of formal reasoning which mimics such a practice: when a procedure in a program is verified, only accessed memory cells are considered. The separation logic has a proof rule, called the Frame Rule, which permits deriving invariants on memory cell not accessed by a procedure easily; consequently, one can do the local reasoning with the rule. This talk is about the Frame Rule, and its subtle soundness result. I will also show that the Frame Rule permits "local specification", that is, specification that only mentions the memory cells that a procedure touches.

June 27: Towards a Mechanized Reasoning
Abstract: Automatic program verifications had been considered as an pure academic issue until recent verification tools, such as SLAM, ESC, Bandera and Polyspace C/Ada verifier, demonstrated its feasibility. These tools were built using Hoare logic, model checking, abstract interpretation, program analysis or theorem proving; and some of them, such as ESC, SLAM and Polyspace C/Ada verifier, have been used to verify the programs in the product line. In this talk, I will explain the approach used in ESC. ESC generates verification conditions from a given annotated program, and uses a theorem prover to check whether the conditions hold or not. I will also give a demonstration on a prototype verification tool, SAW, which uses the same approach as in ESC but with Separation logic instead of Morris style extension of Hoare logic for pointers. Finally, I will comment on some ideas about how to avoid the annotation burden, especially for writing loop invariants.