2024/03/27 by Tomáš Dacík, Adam Rogalewicz, Dacík, Tomáš +5
Biochemistry, Genetics and Molecular Biology · Computer Science · #DNA and Biological Computing #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Machine Learning and Algorithms #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2403.18999
openalex publication_date 2024/03/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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\unicodex2013the 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.