Skip navigation
Skip navigation

Automated Theorem Proving for Assertions in Separation Logic with All Connectives

Hou, Zhe; Gore, Rajeev; Tiu, Alwen


This paper considers Reynolds’s separation logic 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 for this logic. Using numerous examples, we illustrate the subtle deficiencies of several existing proof calculi for separation logic, and show that our rules repair these deficiencies. We extend the calculus with rules for linked lists and binary trees, giving a sound,...[Show more]

CollectionsANU Research Publications
Date published: 2015
Type: Conference paper
Source: Beagle - A Hierarchic Superposition Theorem Prover
DOI: 10.1007/978-3-319-21401-6_34


File Description SizeFormat Image
01_Hou_Automated_Theorem_Proving_for_2015.pdf925.5 kBAdobe PDF    Request a copy

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