Deciding Boolean Separation Logic via Small Models (Technical Report)
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911818175217664 |
|---|---|
| author | Dacík, Tomáš Rogalewicz, Adam Vojnar, Tomáš Zuleger, Florian |
| author_facet | Dacík, Tomáš Rogalewicz, Adam Vojnar, Tomáš Zuleger, Florian |
| contents | We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. Our method is based on a model-based translation to SMT for which we introduce several optimisations$\unicode{x2013}$the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. Through a series of experiments, we show that, on the frequently used symbolic heap fragment, our decision procedure is competitive with other existing approaches, and it can outperform them outside the symbolic heap fragment. Moreover, our decision procedure can also handle some formulae for which no decision procedure has been implemented so far. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_18999 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Deciding Boolean Separation Logic via Small Models (Technical Report) Dacík, Tomáš Rogalewicz, Adam Vojnar, Tomáš Zuleger, Florian Logic in Computer Science We present a novel decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. Our method is based on a model-based translation to SMT for which we introduce several optimisations$\unicode{x2013}$the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. Through a series of experiments, we show that, on the frequently used symbolic heap fragment, our decision procedure is competitive with other existing approaches, and it can outperform them outside the symbolic heap fragment. Moreover, our decision procedure can also handle some formulae for which no decision procedure has been implemented so far. |
| title | Deciding Boolean Separation Logic via Small Models (Technical Report) |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2403.18999 |