
A Separation Logic Framework for HOL
Technical Report
Author:  Thomas Tuerk 
Month:  jun 
Note:  http://www.cl.cam.ac.uk/techreports/UCAMCLTR799.pdf 
Publisher:  University of Cambridge, Computer Laboratory 
Year:  2011 
Abstract:  Separation logic is an extension of Hoare logic due to O'Hearn and Reynolds. It was
designed for reasoning about mutable data structures. Because separation logic supports
local reasoning, it scales better than classical Hoare logic and can easily be used to reason
about concurrency. There are automated separation logic tools as well as several formalisations
in interactive theorem provers. Typically, the automated separation logic tools
are able to reason about shallow properties of large programs. They usually consider just
the shape of datastructures, not their datacontent. The formalisations inside theorem
provers can be used to prove interesting, deep properties. However, they typically lack
automation. Another shortcomming is that there are a lot of slightly different separation
logics. For each programming language and each interesting property a new kind of
separation logic seems to be invented.
In this thesis, a general framework for separation logic is developed inside the HOL4
theorem prover. This framework is based on Abstract Separation Logic, an abstract,
high level variant of separation logic. Abstract Separation Logic is a general separation
logic such that many other separation logics can be based on it. This framework is
instantiatiated in a first step to support a stack with read and write permissions following
ideas of Parkinson, Bornat and Calcagno. Finally, the framework is further instantiated
to build a separation logic tool called Holfoot. It is similar to the tool Smallfoot, but
extends it from reasoning about shape properties to fully functional specifications.
To my knowledge this work presents the first formalisation of Abstract Separation Logic
inside a theorem prover. By building Holfoot on top of this formalisation, I could demonstrate
that Abstract Separation Logic can be used as a basis for realistic separation logic
tools. Moreover, this work demonstrates that it is feasable to implement such separation
logic tools inside a theorem prover. Holfoot is highly automated. It can verify Smallfoot
examples automatically inside HOL4. Moreover, Holfoot can use the full power of
HOL4. This allows Holfoot to verify fully functional specifications. Simple fully functional
specifications can be handled automatically using HOL4's tools and libraries or
external SMT solvers. More complicated ones can be handled using interactive proofs
inside HOL4. In contrast, most other separation logic tools can reason just about the
shape of data structures. Others reason only about data properties that can be solved
using SMT solvers. 
 
BibTeX 


