|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
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.
|
|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
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.
|
host ::
RSS.