Dvě vítězství výzkumné skupiny VeriFIT na SMT-COMP 2026

Jak poznat, který softwarový nástroj si nejlépe poradí se složitými logickými a matematickými problémy? Odpověď hledá SMT-COMP, prestižní mezinárodní soutěž, která na jednotlivých typech úloh každoročně poměřuje schopnosti takzvaných SMT solverů (Satisfiability Modulo Theories) – programů využívaných například při automatizovaném dokazování, analýze a formální verifikaci softwaru. Na sadách náročných úloh se testuje nejen to, zda dokážou najít správné řešení, ale také jak rychle a efektivně si s problémem poradí.

SMT solver lze také popsat jako nástroj, který automaticky rozhodne, zda může být pravdivé komplexní logické tvrzení sestavené například z aritmetiky, textu nebo jiných běžných prvků. A pokud pravdivé je, pak najde příklad, který to dokazuje. SMT solvery se využívají například k ověřování, zda bezpečnostně kritický software neobsahuje závažné chyby; dále ke kontrole, že kód nelze obelstít škodlivým vstupem, k důkazu, že optimalizace v překladači nezmění chování programu, resp. k automatickému generování testovacích případů pro daný kód.

V letošním ročníku SMT-COMP zaznamenali výrazný úspěch výzkumníci z FIT VUT. Soutěže se zúčastnily dva nástroje vyvíjené fakultní výzkumnou skupinou VeriFIT: Z3-Noodler a Amaya. Níže uvedené výsledky se týkají hlavní kategorie soutěže Single Query Track.

Z3-Noodler

Z3-Noodler je rozšíření známého SMT solveru Z3 založené na automatech. Nástroj je určen pro uvažování o tzv. řetězcových (textových) omezeních – tedy o omezeních, která se používají například při kontrole, zda webová aplikace bezpečně validuje uživatelský vstup, nebo při uvažování o politikách přístupu ke zdrojům. V konkurenci solverů nasazovaných v průmyslu v oblasti cloudové bezpečnosti vyhrál Z3-Noodler v divizi QF_Strings ve všech hodnocených kategoriích: v celkové výkonnosti, paralelní výkonnosti i výkonnosti na úlohách s kladnou i zápornou odpovědí. Zároveň byl v celkovém čase řešení o více než řád rychlejší než druhý nejlepší solver, OSTRICH. A právě to je rozdíl, na němž v praktických aplikacích záleží. Kromě toho byl Z3-Noodler oceněn za největší jedinečný přínos v dané divizi, protože vyřešil úlohy, které žádný jiný ze zúčastněných solverů nezvládl.

Z3-Noodler vyvíjejí Vojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál, Michal Hečko a Michal Šedý z výzkumné skupiny VeriFIT, a to spolu se studenty Markem Effenbergerem, Janem Hraničkou, Ondřejem Koumarem, Jakubem Ráčkem, Michalem Šebestou a Martinem Vallušem, kteří k nástroji přispěli v rámci svých bakalářských či diplomových prací nebo projektové praxe. Úspěch Z3-Noodleru staví na dlouhodobém výzkumu skupiny v oblasti rozhodovacích procedur pro řetězcová omezení založených na automatech.

Amaya

Amaya je solver pro formule lineární celočíselné aritmetiky s neomezenými kvantifikátory. Například při analýze počítačových systémů mohou takové formule popisovat stav systému (zbývající energii, rychlost, dostupné zdroje, počet čekajících úloh aj.) a pravidla, podle nichž se tyto hodnoty mění. Pak lze zkoumat například to, zda určité požadavky platí pro všechny možné případy běhu systému nebo zda existuje způsob, jak systém řídit a zajistit jejich splnění.

Takové formule nacházejí uplatnění v oblastech jako formální analýza a syntéza softwarových i hardwarových systémů. Amaya je řeší neobvyklým způsobem: Místo algebraických metod používaných většinou existujících solverů využívá techniky teorie automatů. Převádí aritmetické podmínky na popis množin možných stavů a analyzuje jejich vlastnosti pomocí automatů. Jako výzkumný prototyp prozatím Amaya není optimalizována tak, aby ve všech ohledech dosahovala surové rychlosti vyzrálých, důkladně inženýrsky doladěných solverů, jako je právě Z3.

Amaya byla vyhlášena vítězem oficiálního žebříčku SMT-COMP „Largest Contribution Ranking“ – tedy ocenění napříč celou soutěží, nikoli omezeného na jedinou divizi – dle dvou hodnoticích kritérií (sekvenční a paralelní výkonnosti). Toto ocenění získává nástroj, který vyřeší největší podíl úloh, které nedokáže vyřešit žádný jiný solver. Přístup nástroje Amaya založený na automatech mu umožňuje uspět právě v úlohách, kde konvenční algebraické solvery narážejí na své limity. Jde současně o přímý výsledek výzkumu skupiny VeriFIT, jenž se zaměřuje na kombinaci teorie automatů a algebraického uvažování v aritmetice.

Nástroj Amaya vyvíjejí Vojtěch Havlena, Michal Hečko, Lukáš Holík a Ondřej Lengál. Projekt navazuje na článek skupiny z konference CAV'24 „Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic“.

Kompletní výsledky jsou dostupné na oficiální stránce výsledků SMT-COMP 2026.

Blahopřejeme členům výzkumné skupiny VeriFIT k dalším úspěchům na mezinárodním poli.