Detail publikace

Deciding Boolean Separation Logic via Small Models

DACÍK Tomáš, ROGALEWICZ Adam, VOJNAR Tomáš a ZULEGER Florian. Deciding Boolean Separation Logic via Small Models. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science, roč. 14570. Cham: Springer Nature Switzerland AG, 2024, s. 188-206. ISBN 978-3-031-57245-6. Dostupné z: https://link.springer.com/chapter/10.1007/978-3-031-57246-3_11
Název česky
Rozhodování boolovské Separační logiky pomocí malých modelů
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Dacík Tomáš, Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Zuleger Florian, Dr. (FORSYTE)
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, CH
DOI
10.1007/978-3-031-57246-3_11
UT WoS
001284177100011
EID Scopus
2-s2.0-85192193859
BibTeX 
@INPROCEEDINGS{FITPUB13138,
   author = "Tom\'{a}\v{s} Dac\'{i}k and Adam Rogalewicz and Tom\'{a}\v{s} Vojnar and Florian Zuleger",
   title = "Deciding Boolean Separation Logic via Small Models",
   pages = "188--206",
   booktitle = "Tools and Algorithms for the Construction and Analysis of Systems (TACAS)",
   series = "Lecture Notes in Computer Science",
   volume = 14570,
   year = 2024,
   location = "Cham, CH",
   publisher = "Springer Nature Switzerland AG",
   ISBN = "978-3-031-57245-6",
   doi = "10.1007/978-3-031-57246-3\_11",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13138"
}
Nahoru