Algoritmus PD-KIND v řešiči Golem
| Název práce v češtině: | Algoritmus PD-KIND v řešiči Golem |
|---|---|
| Název v anglickém jazyce: | The PD-KIND algorithm in the Golem SMT solver |
| Akademický rok vypsání: | 2023/2024 |
| Typ práce: | bakalářská práce |
| Jazyk práce: | |
| Ústav: | Katedra distribuovaných a spolehlivých systémů (32-KDSS) |
| Vedoucí / školitel: | doc. RNDr. Jan Kofroň, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 06.02.2024 |
| Datum zadání: | 11.03.2024 |
| Datum potvrzení stud. oddělením: | 09.04.2024 |
| Konzultanti: | Mgr. Martin Blicha, Ph.D. |
| Zásady pro vypracování |
| 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ů. |
| Seznam odborné literatury |
| [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 |