Thesis Details
A Decision Procedure for Strong-Separation Logic
Separation logic (SL) is one of the most successful tools for verification of programs that manipulate dynamically allocated memory. Its expressive power, however, comes at a cost of undecidability when several of its features are combined, especially separating implications. To circumvent this problem, the recently introduced strong-separation logic (SSL) uses a stricter definition of the semantics, making it decidable, while remaining suitable for verification. However, there is currently no implementation of a decision procedure for SSL. In this work, we propose a decision procedure for SSL based on a translation to first-order formulae that can be later solved by a specialised solver. Our experimental results on restricted fragments where SL and SSL coincide show that our approach can effectively solve formulae obtained from verification tools based on SL and also outperform all other existing translation-based decision procedures. Moreover, during our experiments, we found cases of unsoundness of the heuristics implemented in the decision procedure for SL that is a part of the well-known cvc5 SMT solver. Based on our reports, those heuristics has been fixed.
Separation logic, strong-separation logic, decision procedure, SMT
Drábek Vladimír, doc. Ing., CSc. (DCSY FIT BUT), člen
Matoušek Petr, doc. Ing., Ph.D., M.A. (DIFS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
Zbořil František, doc. Ing., Ph.D. (DITS FIT BUT), člen
@mastersthesis{FITMT25151,
author = "Tom\'{a}\v{s} Dac\'{i}k",
type = "Master's thesis",
title = "A Decision Procedure for Strong-Separation Logic",
school = "Brno University of Technology, Faculty of Information Technology",
year = 2022,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/25151/"
}