Output details
11 - Computer Science and Informatics
University of Oxford
Return to search
Output 0 of 0 in the submission
Article title
Tractable reasoning in a fragment of separation logic
Type
D - Journal article
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
Number of additional authors
4
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
7
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-