Skip navigation
Skip navigation

Automated Theorem Proving for Assertions in Separation Logic with All Connectives

Hou, Zhe; Gore, Rajeev; Tiu, Alwen

Description

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
URI: http://hdl.handle.net/1885/103775
Source: Beagle - A Hierarchic Superposition Theorem Prover
DOI: 10.1007/978-3-319-21401-6_34

Download

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:  20 July 2017/ Responsible Officer:  University Librarian/ Page Contact:  Library Systems & Web Coordinator