Document Open Access Logo

On Symbolic Heaps Modulo Permission Theories

Authors Stéphane Demri, Etienne Lozes, Denis Lugiez

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2017.25.pdf
  • Filesize: 0.64 MB
  • 14 pages

Document Identifiers

Author Details

Stéphane Demri
Etienne Lozes
Denis Lugiez

Cite As Get BibTex

Stéphane Demri, Etienne Lozes, and Denis Lugiez. On Symbolic Heaps Modulo Permission Theories. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 25:1-25:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2017.25

Abstract

We address the entailment problem for separation logic with symbolic heaps admitting list pred- icates and permissions for memory cells that are essential to express ownership of a heap region. In the permission-free case, the entailment problem is known to be in P. Herein, we design new decision procedures for solving the satisfiability and entailment problems that are parameterised by the permission theories. This permits the use of solvers dealing with the permission theory at hand, independently of the shape analysis. We also show that the entailment problem without list predicates is coNP-complete for several permission models, such as counting permissions and binary tree shares but the problem is in P for fractional permissions. Furthermore, when list predicates are added, we prove that the entailment problem is coNP-complete when the entail- ment problem for permission formulae is in coNP, assuming the write permission can be split into as many read permissions as desired. Finally, we show that the entailment problem for any Boolean permission model with infinite width is coNP-complete.

Subject Classification

Keywords
  • separation logic
  • entailment
  • permission
  • reasoning modulo theories

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In CAV'11, volume 8606 of LNCS, pages 171-177. Springer, 2011. Google Scholar
  2. C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability Modulo Theories, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 825-885. IOS Press, 2008. Google Scholar
  3. J. Berdine, C. Calcagno, and P. O'Hearn. A decidable fragment of separation logic. In FSTTCS'04, volume 3328 of LNCS, pages 97-109. Springer, 2004. Google Scholar
  4. R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In POPL'05, pages 259-270. ACM, 2005. Google Scholar
  5. J. Boyland. Checking interference with fractional permissions. In SAS'03, number 2694 in LNCS, pages 55-72. Springer, 2003. Google Scholar
  6. B. Cook, C. Haase, J. Ouaknine, M. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR'11, volume 6901 of LNCS, pages 235-249, 2011. Google Scholar
  7. R. Dockins, A. Hobor, and A.W. Appel. A fresh look at separation algebras and share accounting. In APLAS'09, volume 5904 of LNCS, pages 161-177. Springer, 2009. Google Scholar
  8. D. Galmiche, D. Mery, and D. Pym. Resource tableaux (extended abstract). In CSL'02, volume 2471 of LNCS, pages 183-199. Springer, 2002. Google Scholar
  9. C. Haase, S. Ishtiaq, J. Ouaknine, and M. Parkinson. SeLoger: A tool for graph-based reasoning in separation logic. In CAV'13, volume 8044 of LNCS, pages 790-795, 2013. Google Scholar
  10. G. He, S. Qin, C. Luo, and W.N. Chin. Memory Usage Verification Using Hip/Sleek. In ATVA'09, number 5799 in LNCS, pages 166-181. Springer, 2009. Google Scholar
  11. B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. Verifast: A powerful, sound, predictable, fast verifier for C and Java. In NFM'11, volume 6617 of LNCS, pages 41-55. Springer, 2011. Google Scholar
  12. X. Bach Le, C. Gherghina, and A. Hobor. Decision procedures over sophisticated fractional permissions. In APLAS'12, pages 368-385, 2012. Google Scholar
  13. J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In LICS'02, pages 55-74. IEEE, 2002. Google Scholar
  14. Th. Schaefer. The complexity of satisfiability problems. In STOC'78, pages 216-226, 1978. Google Scholar
  15. J. Villard, E. Lozes, and C. Calcagno. Tracking heaps that hop with Heap-Hop. In TACAS'10, volume 6015 of LNCS, pages 275-279. Springer, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact