Deciding Boolean Separation Logic via Small Models

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F24%3APU150716" target="_blank" >RIV/00216305:26230/24:PU150716 - isvavai.cz</a>

Result on the web

<a href="https://link.springer.com/chapter/10.1007/978-3-031-57246-3_11" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-57246-3_11</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-57246-3_11" target="_blank" >10.1007/978-3-031-57246-3_11</a>

Result language

angličtina

Original language name

Deciding Boolean Separation Logic via Small Models

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

Result was created during the realization of more than one project. More information in the Projects tab.

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Tools and Algorithms for the Construction and Analysis of Systems (TACAS)

ISBN

978-3-031-57245-6

ISSN

—

e-ISSN

—

Number of pages

19

Pages from-to

188-206

Publisher name

Springer Nature Switzerland AG

Place of publication

Cham

Event location

Centre for Security, Reliability and Trust (SnT)

Event date

Apr 6, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001284177100011