Detail publikačního výsledku

Deciding Boolean Separation Logic via Small Models

DACÍK, T.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F.

Originální název

Deciding Boolean Separation Logic via Small Models

Anglický název

Deciding Boolean Separation Logic via Small Models

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

separation logic, arbitrary combinations of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations, decision procedure, translation to SMT

Klíčová slova v angličtině

separation logic, arbitrary combinations of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations, decision procedure, translation to SMT

Autoři

DACÍK, T.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F.

Rok RIV

2025

Vydáno

04.04.2024

Nakladatel

Springer Nature Switzerland AG

Místo

Cham

ISBN

978-3-031-57245-6

Kniha

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

Edice

Lecture Notes in Computer Science

Svazek

14570

Strany od

188

Strany do

206

Strany počet

19

URL

https://link.springer.com/chapter/10.1007/978-3-031-57246-3_11

Plný text v Digitální knihovně

http://hdl.handle.net/11012/252866

BibTex

@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"
}

Dokumenty

978-3-031-57246-3_11