The Logic of Separation Logic: Models and Proofs

Frank S. de Boer; Hans Dieter A. Hiep; Stijn de Gouw

doi:10.1007/978-3-031-43513-3_22

The Logic of Separation Logic: Models and Proofs

Frank S. de Boer, Hans Dieter A. Hiep^*, Stijn de Gouw

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

Abstract

The standard semantics of separation logic is restricted to finite heaps. This restriction already gives rise to a logic which does not satisfy compactness, hence it does not allow for an effective, sound and complete axiomatization. In this paper we therefore study both the general model theory and proof theory of the separation logic of finite and infinite heaps over arbitrary (first-order) models. We show that we can express in the resulting logic finiteness of the models and the existence of both countably infinite and uncountable models. We further show that a sound and complete sequent calculus still can be obtained by restricting the second-order quantification over heaps to first-order definable heaps.

Original language	English
Title of host publication	Automated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publication	32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings
Editors	Revantha Ramanayake, Josef Urban
Publisher	Springer
Pages	407-426
Number of pages	20
ISBN (Electronic)	9783031435133
ISBN (Print)	9783031435126
DOIs	https://doi.org/10.1007/978-3-031-43513-3_22
Publication status	Published - 14 Sept 2023
Event	32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023 - Prague, Czech Republic Duration: 18 Sept 2023 → 21 Sept 2023 https://tableaux2023.tableaux-ar.org/#:~:text=The%2032nd%20International%20Conference,September%2018%2D21%2C%202023.

Publication series

Series	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14278 LNAI
ISSN	0302-9743

Conference

Conference	32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023
Country/Territory	Czech Republic
City	Prague
Period	18/09/23 → 21/09/23
Internet address	https://tableaux2023.tableaux-ar.org/#:~:text=The%2032nd%20International%20Conference,September%2018%2D21%2C%202023.

Access to Document

10.1007/978-3-031-43513-3_22Licence: CC BY

Cite this

de Boer, F. S., Hiep, H. D. A., & de Gouw, S. (2023). The Logic of Separation Logic: Models and Proofs. In R. Ramanayake, & J. Urban (Eds.), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings (pp. 407-426). Springer. https://doi.org/10.1007/978-3-031-43513-3_22

de Boer, Frank S. ; Hiep, Hans Dieter A. ; de Gouw, Stijn. / The Logic of Separation Logic : Models and Proofs. Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. editor / Revantha Ramanayake ; Josef Urban. Springer, 2023. pp. 407-426 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14278 LNAI).

@inproceedings{71506cf88d0742dd9f20216e3acfd2ef,

title = "The Logic of Separation Logic: Models and Proofs",

abstract = "The standard semantics of separation logic is restricted to finite heaps. This restriction already gives rise to a logic which does not satisfy compactness, hence it does not allow for an effective, sound and complete axiomatization. In this paper we therefore study both the general model theory and proof theory of the separation logic of finite and infinite heaps over arbitrary (first-order) models. We show that we can express in the resulting logic finiteness of the models and the existence of both countably infinite and uncountable models. We further show that a sound and complete sequent calculus still can be obtained by restricting the second-order quantification over heaps to first-order definable heaps.",

author = "{de Boer}, {Frank S.} and Hiep, {Hans Dieter A.} and {de Gouw}, Stijn",

note = "Funding Information: The authors thank the anonymous referees for providing many constructive and useful suggestions for improvement. Publisher Copyright: {\textcopyright} 2023, The Author(s).; 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023 ; Conference date: 18-09-2023 Through 21-09-2023",

year = "2023",

month = sep,

day = "14",

doi = "10.1007/978-3-031-43513-3_22",

language = "English",

isbn = "9783031435126",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "407--426",

editor = "Revantha Ramanayake and Josef Urban",

booktitle = "Automated Reasoning with Analytic Tableaux and Related Methods",

url = "https://tableaux2023.tableaux-ar.org/#:~:text=The%2032nd%20International%20Conference,September%2018%2D21%2C%202023.",

}

de Boer, FS, Hiep, HDA & de Gouw, S 2023, The Logic of Separation Logic: Models and Proofs. in R Ramanayake & J Urban (eds), Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14278 LNAI, pp. 407-426, 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023, Prague, Czech Republic, 18/09/23. https://doi.org/10.1007/978-3-031-43513-3_22

The Logic of Separation Logic: Models and Proofs. / de Boer, Frank S.; Hiep, Hans Dieter A.; de Gouw, Stijn.
Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. ed. / Revantha Ramanayake; Josef Urban. Springer, 2023. p. 407-426 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14278 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference Article in proceeding › Academic › peer-review

TY - GEN

T1 - The Logic of Separation Logic

T2 - 32nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2023

AU - de Boer, Frank S.

AU - Hiep, Hans Dieter A.

AU - de Gouw, Stijn

PY - 2023/9/14

Y1 - 2023/9/14

N2 - The standard semantics of separation logic is restricted to finite heaps. This restriction already gives rise to a logic which does not satisfy compactness, hence it does not allow for an effective, sound and complete axiomatization. In this paper we therefore study both the general model theory and proof theory of the separation logic of finite and infinite heaps over arbitrary (first-order) models. We show that we can express in the resulting logic finiteness of the models and the existence of both countably infinite and uncountable models. We further show that a sound and complete sequent calculus still can be obtained by restricting the second-order quantification over heaps to first-order definable heaps.

AB - The standard semantics of separation logic is restricted to finite heaps. This restriction already gives rise to a logic which does not satisfy compactness, hence it does not allow for an effective, sound and complete axiomatization. In this paper we therefore study both the general model theory and proof theory of the separation logic of finite and infinite heaps over arbitrary (first-order) models. We show that we can express in the resulting logic finiteness of the models and the existence of both countably infinite and uncountable models. We further show that a sound and complete sequent calculus still can be obtained by restricting the second-order quantification over heaps to first-order definable heaps.

U2 - 10.1007/978-3-031-43513-3_22

DO - 10.1007/978-3-031-43513-3_22

M3 - Conference Article in proceeding

AN - SCOPUS:85172418206

SN - 9783031435126

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 407

EP - 426

BT - Automated Reasoning with Analytic Tableaux and Related Methods

A2 - Ramanayake, Revantha

A2 - Urban, Josef

PB - Springer

Y2 - 18 September 2023 through 21 September 2023

ER -

de Boer FS, Hiep HDA, de Gouw S. The Logic of Separation Logic: Models and Proofs. In Ramanayake R, Urban J, editors, Automated Reasoning with Analytic Tableaux and Related Methods: 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings. Springer. 2023. p. 407-426. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 14278 LNAI). doi: 10.1007/978-3-031-43513-3_22