|
|
Deciding Logic with Automata
Hečko, Michal ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
The work presented in this thesis focuses on deciding quantified linear integer arithmetic using finite automata. We present a novel implementation of the classical automata-based decision procedure supporting the SMT-LIB input format. Our comprehensive presentation of the developed tool focuses on various aspects and design decisions that play a prominent role in the performance of the implementation. We identify the lack of theory-based reasoning as the primary reason for the overall poor performance of the decision procedure and give a range of cheap heuristics that significantly improve its speed. We also give a~novel top-down reformulation of the procedure that allows to perform theory-based reasoning during the construction of automata. We also compare our tool to the state-of-the-art SMT solvers, showing that our prototype implementation is comparative and even superior to the state of the art.
|
|
|
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.