Podpora neinterpretovaných funkcí v SMT řešiči Yaga
| Název práce v češtině: | Podpora neinterpretovaných funkcí v SMT řešiči Yaga |
|---|---|
| Název v anglickém jazyce: | Support for Uninterpreted Functions in Yaga 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: | Milan Malačka - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 02.04.2024 |
| Datum zadání: | 09.04.2024 |
| Datum potvrzení stud. oddělením: | 09.04.2024 |
| Zásady pro vypracování |
| Yaga [1] is a modern, modular, MC-SAT-based [2] SMT solver developed at Charles University. Currently, it supports Boolean logic and Linear Real Arithmetic, allowing for basic experimenting with the algorithms and solver heuristics. To extend the functionality and applicability of the solver, more logics—realized as plugins in the Yaga tool—are to be implemented.
The goal of this thesis is to design and implement support for uninterpreted functions (UF) into the Yaga SMT solver. This includes extending its front-end to be able to parse the corresponding subset of the SMT-LIB specification [3], designing a plugin in terms of the algorithm and data structures, and connecting it appropriately with the Yaga tool and its current plugins. The result is to be evaluated on a set of benchmarks. |
| Seznam odborné literatury |
| [1] Yaga: https://github.com/d3sformal/yaga
[2] D. Jovanovic, C. Barrett and L. de Moura, "The design and implementation of the model constructing satisfiability calculus," 2013 Formal Methods in Computer-Aided Design, Portland, OR, USA, 2013, pp. 173-180, doi: 10.1109/FMCAD.2013.7027033 [3] SMT-LIB: http://smtlib.cs.uiowa.edu/ |