Detail publikace

Deciding Boolean Separation Logic via Small Models

DACÍK, T.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F. Deciding Boolean Separation Logic via Small Models. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2024. p. 188-206. ISBN: 978-3-031-57245-6.
Název česky
Rozhodování boolovské Separační logiky pomocí malých modelů
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Dacík Tomáš, Ing. (UITS)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Zuleger Florian, Dr.
URL
Klíčová slova

separační logika, libovolná kombinace separačních konjunkcí a booleovských
konjunkcí, disjunkcí a strážených negací, rozhodovací procedura, překlad do SMT

Abstrakt

Představujeme novou rozhodovací proceduru pro fragment separační logiky (SL)
s libovolným vnořováním separačních konjunkcí s logickými konjunkcemi,
disjunkcemi a střeženými negacemi spolu s podporou nejběžnějších variant
spojovaných seznamů. Naše metoda je založena na překladu na základě modelů do
SMT, pro který zavádíme několik optimalizací -- nejdůležitější z nich je založena
na omezení velikosti instancí predikátů v rámci modelů větších formulí, což vede
k mnohem efektivnějšímu překladu formulí SL do SMT. Prostřednictvím řady
experimentů ukazujeme, že na často používaném fragmentu symbolické haldy je náš
rozhodovací postup konkurenceschopný s ostatními existujícími přístupy a může je
překonat i mimo fragment symbolické haldy. Náš rozhodovací postup si navíc poradí
i s některými formulemi, pro které dosud nebyl žádný rozhodovací postup
implementován.

Rok
2024
Strany
188–206
Sborník
Tools and Algorithms for the Construction and Analysis of Systems (TACAS)
Řada
Lecture Notes in Computer Science
Svazek
14570
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'24 (TACAS'24), Centre for Security, Reliability and Trust (SnT), University of Luxembourg., LU
ISBN
978-3-031-57245-6
Vydavatel
Springer Nature Switzerland AG
Místo
Cham
DOI
10.1007/978-3-031-57246-3_11
UT WoS
001284177100011
EID Scopus
2-s2.0-85192193859
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"
}
Nahoru