Advertisement
Published in:
2008 | OriginalPaper | Chapter
Separation Logic Tutorial
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Separation logic is an extension of Hoare’s logic for reasoning about programs that manipulate pointers. It is based on the
separating conjunction
P
∗
Q
, which asserts that
P
and
Q
hold for separate portions of computer memory.
This tutorial on separation logic has three parts.
1
Basics.
Concentrating on highlights from the early work [1,2,3,4].
1
Model Theory.
The model theory of separation logic evolved from the general resource models of bunched logic [5,6,7] and includes an account of program dynamics in terms of their interaction with resource [8,9].
1
Proof Theory
. I will describe those aspects of the proof theory, particularly new entailment questions (frame and anti-frame inference [10,11]), which are important for applications in mechanized program verification.