What is wrong?

Notice: Before sending an error with the download, please try the direct link first: Structural Separation Logic


You must sign in to do that.

Forgot password?

Structural Separation Logic

Structural Separation Logic

Structural Separation Logic

Score: ---- | 0 votes
| Sending vote
| Voted!

Book Details:

Publisher:Imperial College London
Pages:307 pages
Size:4.21 MB
License:Pending review


This thesis presents structural separation logic, a novel program reasoning approach for software that manipulates both standard heaps and structured data such as lists and trees. Structural separation logic builds upon existing work in both separation logic and context logic. It considers data abstractly, much as it is exposed by library interfaces, ignoring implementation details.

We provide a programming language that works over structural heaps, which are similar to standard heaps but allow data to be stored in an abstract form. We introduce abstract heaps, which extend structural heaps to enable local reasoning about abstract data. Such data can be split up with structural addresses. Structural addresses allow sub-data (e.g. a sub-tree within a tree) to be abstractly allocated, promoting the sub-data to an abstract heap cell. This cell can be analysed in isolation, then re-joined with the original data. We show how the tight footprints this allows can be refined further with promises, which enable abstract heap cells to retain information about the context from which they were allocated. We prove that our approach is sound with respect to a standard Hoare logic.

We study two large examples. Firstly, we present an axiomatic semantics for the Document Object Model in structural separation logic. We demonstrate how structural separation logic allows abstract reasoning about the DOM tree using tighter footprints than were possible in previous work. Secondly, we give a novel presentation of the POSIX file system library. We identify a subset of the large POSIX standard that focuses on the file system, including commands that manipulate both the file heap and the directory structure. Axioms for this system are given using structural separation logic. As file system resources are typically identified by paths, we use promises to give tight footprints to commands, so that that they do not require all the resource needed to explain paths being used. We demonstrate our reasoning using a software installer example.



Loading comments...

Scanning lists...

The book in numbers

global rank

rank in categories

online since


rate score

Nothing yet...


Nothing yet...

Social likes

Nothing yet...



This may take several minutes


Countries segmentation

This may take several minutes

Source Referers

Websites segmentation


This may take several minutes