Department of Informatics

TU München - Fakultät für Informatik
Chair IV: Software & Systems Engineering

TUM
 
PDF-Datei  A Separation Logic Framework for HOL

Technical Report

Author:Thomas Tuerk
Month:jun
Note:http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-799.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 data-content. 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

(c) 1999-2006 - Lehrstuhl Software & Systems Engineering
Sitemap |  Contact