Symbolic-Heap Separation logic is a popular formalism for automated reasoning about heap-manipulating programs, which allows the user to give customized data structure definitions. In this paper, we give a new decidability proof for the separation logic fragment of Iosif, Rogalewicz and Simacek. We circumvent the reduction to MSO from their proof and provide a direct model-theoretic construction with elementary complexity. We implemented our approach in the Harrsh analyzer and evaluate its effectiveness. In particular, we show that Harrsh can decide the entailment problem for data structure definitions for which no previous decision procedures have been implemented.
CITATION STYLE
Katelaan, J., Matheja, C., & Zuleger, F. (2019). Effective entailment checking for separation logic with inductive definitions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11428 LNCS, pp. 319–336). Springer Verlag. https://doi.org/10.1007/978-3-030-17465-1_18
Mendeley helps you to discover research relevant for your work.