Podpora neinterpretovaných funkcí v SMT řešiči Yaga
| Thesis title in Czech: | Podpora neinterpretovaných funkcí v SMT řešiči Yaga |
|---|---|
| Thesis title in English: | Support for Uninterpreted Functions in Yaga 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: | Milan Malačka - assigned and confirmed by the Study Dept. |
| Date of registration: | 02.04.2024 |
| Date of assignment: | 09.04.2024 |
| Confirmed by Study dept. on: | 09.04.2024 |
| Guidelines |
| 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. |
| References |
| [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/ |