Skip navigation
Skip navigation

Labelled sequent calculi and automated reasoning for assertions in separation logic

Hou, Zhe


Separation logic (SL) is an extension of Hoare logic to reason about programs with mutable data structures. This thesis studies automated reasoning for the assertional language (i.e., formulae that represent pre- and post-conditions) of separation logic. We start from the core of separation logic called Boolean BI (BBI), then consider various propositional abstract separation logics (PASLs) as extensions of BBI. These logics are "abstract" because they are independent of any particular concrete...[Show more]

CollectionsOpen Access Theses
Date published: 2015
Type: Thesis (PhD)
DOI: 10.25911/5c6e715417a6d


File Description SizeFormat Image
b37881504_H?u_Zh?.pdf492.53 MBAdobe PDFThumbnail

Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.

Updated:  17 November 2022/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator