Interpolation Support for Yaga SMT Solver
| Název práce v češtině: | Podpora interpolace v SMT řešiči Yaga |
|---|---|
| Název v anglickém jazyce: | Interpolation Support for Yaga SMT Solver |
| Klíčová slova: | Satisfiability modulo theories|Craigova interpolace|Yaga |
| Klíčová slova anglicky: | Satisfiability modulo theories|Craig interpolation|Yaga |
| Akademický rok vypsání: | 2024/2025 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ú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í: | 17.04.2025 |
| Datum zadání: | 22.04.2025 |
| Datum potvrzení stud. oddělením: | 23.04.2025 |
| Datum a čas obhajoby: | 10.02.2026 10:00 |
| Datum odevzdání elektronické podoby: | 08.01.2026 |
| Datum odevzdání tištěné podoby: | 08.01.2026 |
| Datum proběhlé obhajoby: | 10.02.2026 |
| Oponenti: | RNDr. Petr Kučera, Ph.D. |
| Zásady pro vypracování |
| In software verification, SMT solvers are often used as back-end tools for deciding about program correctness. Their functionality is no longer limited just to deciding the satisfiability of the input formula, but it is typically required to produce models, unsatisfiability cores, or
interpolants further improving convergence of the verification process. The goal of the thesis is to extend the MCSat-based Yaga SMT solver [1] with interpolation functionality, in particular to produce "model interpolants" [2,3]. The resulting implementation should be evaluated on a number of benchmarks, preferably from a public benchmark set. |
| Seznam odborné literatury |
| [1] Yaga: MC-Sat SMT solver – https://github.com/d3sformal/yaga
[2] Dejan Jovanovic, Bruno Dutertre (2021): Interpolation and Model Checking for Nonlinear Arithmetic. [3] Dejan Jovanovic, Clark Barrett, Leonardo de Moura (2013): The design and implementation of the model constructing satisfiability calculus |