Publication Details
Deciding Boolean Separation Logic via Small Models
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Zuleger Florian, Dr.
separation logic, arbitrary combinations of separating conjunctions with boolean
conjunctions, disjunctions, and guarded negations, decision procedure,
translation to SMT
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---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.
@inproceedings{BUT187751,
author="Tomáš {Dacík} and Adam {Rogalewicz} and Tomáš {Vojnar} and Florian {Zuleger}",
title="Deciding Boolean Separation Logic via Small Models",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
year="2024",
series="Lecture Notes in Computer Science",
volume="14570",
pages="188--206",
publisher="Springer Nature Switzerland AG",
address="Cham",
doi="10.1007/978-3-031-57246-3\{_}11",
isbn="978-3-031-57245-6",
url="https://link.springer.com/chapter/10.1007/978-3-031-57246-3_11"
}