×

On symbolic heaps modulo permission theories. (English) Zbl 1491.68050

Lokam, Satya (ed.) et al., 37th IARCS annual conference on foundations of software technology and theoretical computer science, FSTTCS 2017, IIT Kanpur, India, December 12–14, 2017. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 93, Article 25, 14 p. (2018).
Summary: We address the entailment problem for separation logic with symbolic heaps admitting list predicates 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 entailment 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.
For the entire collection see [Zbl 1388.68010].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68P05 Data structures
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q25 Analysis of algorithms and problem complexity

Software:

SeLoger; CVC4; VeriFast
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In {\it CAV’11}, volume 8606 of {\it LNCS}, pages 171-177. Springer, 2011.
[2] C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. {\it Satisfiability Modulo Theories}, volume 185 of {\it Frontiers in Artificial Intelligence and Applications}, pages 825-885. IOS Press, 2008.
[3] J. Berdine, C. Calcagno, and P. O’Hearn. A decidable fragment of separation logic. In {\it FSTTCS’04}, volume 3328 of {\it LNCS}, pages 97-109. Springer, 2004. · Zbl 1117.03337
[4] R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission accounting in separa tion logic. In {\it POPL’05}, pages 259-270. ACM, 2005. · Zbl 1369.68130
[5] J. Boyland. Checking interference with fractional permissions. In {\it SAS’03}, number 2694 in LNCS, pages 55-72. Springer, 2003. · Zbl 1067.68537
[6] B. Cook, C. Haase, J. Ouaknine, M. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In {\it CONCUR’11}, volume 6901 of {\it LNCS}, pages 235-249, 2011. · Zbl 1300.03017
[7] R. Dockins, A. Hobor, and A.W. Appel. A fresh look at separation algebras and share accounting. In {\it APLAS’09}, volume 5904 of {\it LNCS}, pages 161-177. Springer, 2009.
[8] D. Galmiche, D. Mery, and D. Pym. Resource tableaux (extended abstract). In {\it CSL’02}, volume 2471 of {\it LNCS}, pages 183-199. Springer, 2002. · Zbl 1020.03508
[9] C. Haase, S. Ishtiaq, J. Ouaknine, and M. Parkinson. SeLoger: A tool for graph-based reasoning in separation logic. In {\it CAV’13}, volume 8044 of {\it LNCS}, pages 790-795, 2013.
[10] G. He, S. Qin, C. Luo, and W.N. Chin. Memory Usage Verification Using Hip/Sleek. In {\it ATVA’09}, number 5799 in LNCS, pages 166-181. Springer, 2009.
[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 {\it NFM’11}, volume 6617 of {\it LNCS}, pages 41-55. Springer, 2011.
[12] X. Bach Le, C. Gherghina, and A. Hobor. Decision procedures over sophisticated fractional permissions. In {\it APLAS’12}, pages 368-385, 2012.
[13] J.C. Reynolds. Separation logic: a logic for shared mutable data structures. In {\it LICS’02}, pages 55-74. IEEE, 2002.
[14] Th. Schaefer. The complexity of satisfiability problems. In {\it STOC’78}, pages 216-226, 1978. · Zbl 1282.68143
[15] J. Villard, E. Lozes, and C. Calcagno.Tracking heaps that hop with Heap-Hop.In {\it TACAS’10}, volume 6015 of {\it LNCS}, pages 275-279. Springer, 2010.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.