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]

dc.contributor.authorHou, Zhe
dc.date.accessioned2019-02-18T01:31:05Z
dc.date.available2019-02-18T01:31:05Z
dc.date.copyright2015
dc.identifier.otherb3788150
dc.identifier.urihttp://hdl.handle.net/1885/155766
dc.description.abstractSeparation 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 memory model. Finally, we look at separation logic with Reynolds's heap model semantics. We first try to capture BI logics using nested sequents, our design has a special structure of interleaving additive and multiplicative nested sequents. We discover that this nested structure causes much complication when considering the rules for transferring information between nested sequents. Then we change the angle to solve this problem by using labelled sequents. We present a labelled sequent calculus LS_BBI for BBI, the calculus is simple, sound, complete, and enjoys cut-elimination. We show that all the structural rules in LS_BBI can be localised around applications of certain logical rules, based on which we demonstrate a free variable calculus that deals with the structural rules lazily in a constraint system. We propose a heuristic method to quickly solve certain constraints, and show some experimental results to confirm that our approach is feasible for proof search. Based on LS_BBI, we develop a modular proof theory for various PASLs using cut-free labelled sequent calculi. We first extend LS BBI to handle Calcagno et al.'s original logic of separation algebras by adding rules for partial-determinism and cancellativity. We prove the completeness of our calculus via an intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other PASLs by adding rules for other properties in separation theory. We present a theorem prover based on our labelled calculi for these logics. For concrete heap semantics, we consider Reynolds's SL with all logical connectives but without arbitrary predicates. This logic is not recursively enumerable but is very useful in practice. We give a sound labelled sequent calculus LS_SL for this logic. We illustrate the subtle deficiencies of some existing proof calculi for SL, and show that our rules repair these problems. We extend LS SL with rules for linked lists and binary trees, giving a sound, complete and terminating proof system for a popular fragment called symbolic heaps. Our prover shows comparable results with Smallfoot on valid formulae and on formulae extracted from program verification examples, but it is not competitive on large invalid formulae. However, our prover handles the largest fragment of logical connectives in SL.
dc.format.extentxvii, 270 leaves.
dc.language.isoen_AU
dc.titleLabelled sequent calculi and automated reasoning for assertions in separation logic
dc.typeThesis (PhD)
dcterms.valid2015
local.description.notesThesis (Ph.D)--Australian National University, 2015
local.type.degreeDoctor of Philosophy (PhD)
dc.date.issued2015
local.contributor.affiliationThe Australian National University. Research School of Computer Science
local.identifier.doi10.25911/5c6e715417a6d
dc.date.updated2019-01-10T01:38:13Z
local.mintdoimint
CollectionsOpen Access Theses

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