Skip navigation
Skip navigation

Labelled sequent calculi and automated reasoning for assertions in separation logic

Hou, Zhe

Description

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)
URI: http://hdl.handle.net/1885/155766
DOI: 10.25911/5c6e715417a6d

Download

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:  19 May 2020/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator