Algoritmus PD-KIND v řešiči Golem
| Thesis title in Czech: | Algoritmus PD-KIND v řešiči Golem |
|---|---|
| Thesis title in English: | The PD-KIND algorithm in the Golem SMT solver |
| Academic year of topic announcement: | 2023/2024 |
| Thesis type: | Bachelor's thesis |
| Thesis language: | |
| Department: | Department of Distributed and Dependable Systems (32-KDSS) |
| Supervisor: | doc. RNDr. Jan Kofroň, Ph.D. |
| Author: | hidden - assigned and confirmed by the Study Dept. |
| Date of registration: | 06.02.2024 |
| Date of assignment: | 11.03.2024 |
| Confirmed by Study dept. on: | 09.04.2024 |
| Advisors: | Mgr. Martin Blicha, Ph.D. |
| Guidelines |
| Golem [1] je řešič Hornových klauzulí, který se využívá pro verifikaci programů pomocí efektivní metody, kterou je překlad do Hornových klauzulí a následně jejich vyhodnocení. Obsahuje několik algoritmů, které využívá k řešení těchto klauzulí, a tedy jejich verifikaci. K nim dokáže poskytnout i svědka jako certifikát validity. Algoritmus PD-Kind (Property-directed k-induction) [4] využívá myšlenky separace ověřování dosažitelnosti od indukčního uvažování v algoritmu IC3 [5] a integruje do ní K-indukci. K-indukce je silnější než normální indukce a pomocí ní má tato metoda potenciál vytvářet přesnější (logicky silnější) invarianty.
Cílem této práce je navrhnout způsob, jak algoritmus PD-KIND integrovat do řešiče Golem, a po té algoritmus v tomto nástroji implementovat. Funkčnost řešení bude demonstrována na sadě dostupných benchmarků. |
| References |
| [1] Golem – Řešič Hornových klauzulí https://github.com/usi-verification-and-security/golem
[2] OpenSMT – SMT řešič https://github.com/usi-verification-and-security/opensmt/ [3] SMT-LIB 2.6 – https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf [4] D. Jovanović and B. Dutertre. Property-directed k-induction, Formal Methods in Computer-Aided Design (FMCAD), Mountain View, CA, USA, 2016, pp. 85-92, DOI: 10.1109/FMCAD.2016.7886665. [5] Lange, T., Neuhäußer, M.R., Noll, T. et al. IC3 software model checking. Int J Softw Tools Technol Transfer 22, 135–161 (2020). https://doi.org/10.1007/s10009-019-00547-x |