Tractable reasoning in a fragment of separation logic
In 2004, Berdine, Calcagno and O'Hearn introduced a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. They showed that entailment in this fragment is in coNP, but the precise complexity of this problem has been open since. In this paper, we sh...
| Main Authors: | , , , , |
|---|---|
| Format: | Conference item |
| Published: |
2011
|
| _version_ | 1797056775001735168 |
|---|---|
| author | Cook, B Haase, C Ouaknine, J Parkinson, M Worrell, J |
| author_facet | Cook, B Haase, C Ouaknine, J Parkinson, M Worrell, J |
| author_sort | Cook, B |
| collection | OXFORD |
| description | In 2004, Berdine, Calcagno and O'Hearn introduced a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. They showed that entailment in this fragment is in coNP, but the precise complexity of this problem has been open since. In this paper, we show that the problem can actually be solved in polynomial time. To this end, we represent separation logic formulae as graphs and show that every satisfiable formula is equivalent to one whose graph is in a particular normal form. Entailment between two such formulae then reduces to a graph homomorphism problem. We also discuss natural syntactic extensions that render entailment intractable. © 2011 Springer-Verlag. |
| first_indexed | 2024-03-06T19:27:14Z |
| format | Conference item |
| id | oxford-uuid:1c2da3aa-7f68-42eb-be18-e9647b953e69 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T19:27:14Z |
| publishDate | 2011 |
| record_format | dspace |
| spelling | oxford-uuid:1c2da3aa-7f68-42eb-be18-e9647b953e692022-03-26T11:04:23ZTractable reasoning in a fragment of separation logicConference itemhttp://purl.org/coar/resource_type/c_5794uuid:1c2da3aa-7f68-42eb-be18-e9647b953e69Symplectic Elements at Oxford2011Cook, BHaase, COuaknine, JParkinson, MWorrell, JIn 2004, Berdine, Calcagno and O'Hearn introduced a fragment of separation logic that allows for reasoning about programs with pointers and linked lists. They showed that entailment in this fragment is in coNP, but the precise complexity of this problem has been open since. In this paper, we show that the problem can actually be solved in polynomial time. To this end, we represent separation logic formulae as graphs and show that every satisfiable formula is equivalent to one whose graph is in a particular normal form. Entailment between two such formulae then reduces to a graph homomorphism problem. We also discuss natural syntactic extensions that render entailment intractable. © 2011 Springer-Verlag. |
| spellingShingle | Cook, B Haase, C Ouaknine, J Parkinson, M Worrell, J Tractable reasoning in a fragment of separation logic |
| title | Tractable reasoning in a fragment of separation logic |
| title_full | Tractable reasoning in a fragment of separation logic |
| title_fullStr | Tractable reasoning in a fragment of separation logic |
| title_full_unstemmed | Tractable reasoning in a fragment of separation logic |
| title_short | Tractable reasoning in a fragment of separation logic |
| title_sort | tractable reasoning in a fragment of separation logic |
| work_keys_str_mv | AT cookb tractablereasoninginafragmentofseparationlogic AT haasec tractablereasoninginafragmentofseparationlogic AT ouakninej tractablereasoninginafragmentofseparationlogic AT parkinsonm tractablereasoninginafragmentofseparationlogic AT worrellj tractablereasoninginafragmentofseparationlogic |