Deciding Boolean Separation Logic via Small Models

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Deciding Boolean Separation Logic via Small Models

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Deciding Boolean Separation Logic via Small Models

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

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

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

ISBN

978-3-031-57245-6

ISSN

—

e-ISSN

—

Počet stran výsledku

19

Strana od-do

188-206

Název nakladatele

Springer Nature Switzerland AG

Místo vydání

Cham

Místo konání akce

Centre for Security, Reliability and Trust (SnT)

Datum konání akce

6. 4. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001284177100011