Original title: Podpora interpolace v SMT řešiči Yaga
Translated title: Interpolation Support for Yaga SMT Solver
Authors: Hurtišová, Viktória ; Kofroň, Jan (advisor) ; Kučera, Petr (referee)
Document type: Master’s theses
Year: 2026
Language: eng
Abstract: [eng] [cze]
We extend the Yaga SMT solver with support for Craig interpolation. Yaga is an SMT solver based on the Model-Constructing Satisfiability Calculus, which integrates theory reasoning directly into the search process. While Yaga already supports satisfi- ability checking for quantifier-free linear real arithmetic and uninterpreted functions, it currently lacks interpolation capabilities required by modern verification workflows. In this thesis, we implement model-based interpolation in Yaga, following an interpolation- modulo-models approach that does not rely on clausal proofs. The implementation in- cludes modifications to Yaga's parsing, control flow, as well as its core components. We evaluate the implementation on SMT-LIB benchmarks, where we validate the correctness of generated interpolants and compare performance with existing SMT solvers. Tato práce rozšiřuje SMT řešič Yaga o podporu Craigovy interpolace. Yaga je SMT řešič založený na kalkulu Model-Constructing Satisfiability, který integruje uvažování v teoriích přímo do prohledávacího procesu. Zatímco Yaga podporuje rozhodování o spl- nitelnosti v bezkvantifikátorové lineární reálné aritmetice a neinterpretovaných funkcích, v současnosti postrádá interpolační funkcionalitu nezbytnou pro moderní verifikační po- stupy. V rámci této práce v řešiči Yaga implementujeme modelově řízenou interpolaci, která není založená na klauzálních důkazech, ale na přístupu interpolace-modulo-model. Implementace zahrnuje úpravy parsování, řídicí logiky i základních komponent řešiče Yaga. Navržené řešení je vyhodnoceno na benchmarcích SMT-LIB, kde ověřujeme správ- nost generovaných interpolantů a porovnáváme výkon s existujícími SMT řešiči.
Keywords: Satisfiability modulo theories|Craig interpolation|Yaga; Satisfiability modulo theories|Craigova interpolace|Yaga

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/207049

Permalink: http://www.nusl.cz/ntk/nusl-696914


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Master’s theses