You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Oxford » Outputs » Detail

Output details

11 - Computer Science and Informatics

University of Oxford

Return to search Previous output Next output

Output 242 of 263 in the submission

Article title

Tractable reasoning in a fragment of separation logic

Type

D - Journal article

DOI

10.1007/978-3-642-23217-6_16

Title of journal

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

Article number

Volume number

6901 LNCS

Issue number

First page of article

235

ISSN of journal

0302-9743

Year of publication

2011

URL

http://link.springer.com/chapter/10.1007/978-3-642-23217-6_16

Number of additional authors

Additional information

<11>

This paper provides a graph-based polynomial-time algorithm for deciding entailments in a key fragment of O'Hearn and Reynolds's Separation Logic (SL). All previously known decision procedures for SL proceeded via inference-rule systems. Achieving polynomial-time was a breakthrough on its own (left open in a 2004 paper of Berdine et al.), but arguably even more important was the graph-theoretic approach, which has since been applied (by us and others) to various more powerful extensions of SL, and used in applications. We subsequently published a tool paper at CAV 2013 on this work, and are actively continuing research in this area.

Interdisciplinary

Cross-referral requested

Research group

None

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract