Přístupnostní navigace
E-application
Search Search Close
Master's Thesis
Author of thesis: Ing. Ondřej Koumar
Acad. year: 2025/2026
Supervisor: doc. Mgr. Lukáš Holík, Ph.D.
Reviewer: Mgr. Juraj Síč
Input validation using regular expressions is a critical component of web application security. However, modern regular expression engines support advanced features, such as backreferences and lookaround assertions, that exceed the expressive power of classical regular languages, rendering traditional analysis based on formal models ineffective. This thesis proposes a structural decomposition approach to address the language membership problem for ECMAScript regular expressions. We introduce the Regex Constraint Graph (RCG), a formal model that transforms complex regex features into a system of string equations and constraints suitable for a Satisfiability Modulo Theories (SMT) solver. The proposed model was implemented as a native C++ module for the Z3-Noodler SMT solver. Evaluation on a large dataset of real-world instances confirmed the correctness of the translation. In a direct comparison with the Black Ostrich solver, Z3-Noodler achieved a significantly lower median evaluation time. Although static quantifier unrolling poses a limitation for large state spaces, the results confirm that integrating structural regex constraints directly into an SMT solver provides a robust and efficient verification tool.
Z3-Noodler, SMT solving, graphs, formal verification, string constraints, ECMAScript, regular expressions, membership problem
Date of defence
22.06.2026
Result of the defence
Defended (thesis was successfully defended)
Grading
A
Process of defence
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm A.
Topics for thesis defence
Language of thesis
English
Faculty
Fakulta informačních technologií
Department
Department of Intelligent Systems
Study programme
Information Technology and Artificial Intelligence (MITAI)
Specialization
Mathematical Methods (NMAT)
Composition of Committee
doc. Mgr. Adam Rogalewicz, Ph.D. (předseda) doc. RNDr. Milan Češka, Ph.D. (místopředseda) Ing. Martin Hrubý, Ph.D. (člen) Ing. Aleš Smrčka, Ph.D. (člen) Dr. Ing. Petr Peringer (člen) Ing. Jaroslav Rozman, Ph.D. (člen)
Supervisor’s reportdoc. Mgr. Lukáš Holík, Ph.D.
Výsledek je skvělý, metoda pro analýzu rozšířených regulárních výrazů ve string constraint solvingu, která je elegantní a překonává state of the art oblasti zejména svou efektivitou. I samotný kód implementace je na výjimečně dobré úrovni a je poměrně rozsáhlý.
Náročné téma, kombinace komplikovaných metod string solvingu a zpracování rozšířených regulárních výrazů, náročný výzkumný úkol. Obtížné je také proniknout do nástroje Z3-Noodler.
Dokončeno včas, konzultováno, text konzultován částečně.
Práce povede téměř jistě k publikaci, zároveň je zásadní pro další praktické aplikace string constraint solvingu.
Výborná, student nejprve nastudoval množství náročné základní literatury, automatové metody string solvingu a zpracování rozšířených regulárních výrazů, samostatně pak studoval nad rámec zadané literatury.
Student byl velmi aktivní a samostatný. Podle doktora Havleny, který studenta vedl technicky, student potřeboval jen velmi málo iniciálních informací a dalo se s ním diskutovat jako s kolegou, sám přicházel s nápady.
Grade proposed by supervisor: A
Reviewer’s reportMgr. Juraj Síč
Aj keď má práca niektoré nedostatky, vzhľadom na kvalitný realizačný výstup a náročnosť práce ju hodnotím známkou A.
Evaluation level: student se odůvodněně odchýlil od zadání s drobnými výhradami
Zadanie vyžadovalo navrhnúť kombináciu metód použitých v nástroji Z3-Noodler s metódami na spracovanie rozšírených regulárnych výrazov v nástroji Black Ostrich a ich implementáciu (body 2 a 3 zadania). Namiesto toho študent navrhol úplne novú metódu na spracovanie rozšírených regulárnych výrazov, ktorú následne implementoval do nástroja Z3-Noodler. V tomto nevidím zásadný problém, keďže navrhnutá metóda dosahuje porovnateľné výsledky s nástrojom Black Ostrich. V práci mi však chýba zdôvodnenie, prečo sa študent nepokúsil o kombináciu metód z nástroja Black Ostrich s nástrojom Z3-Noodler, ako bolo pôvodne uvedené v zadaní.
Evaluation level: je v obvyklém rozmezí
Práca má logickú štruktúru a jednotlivé časti na seba vhodne nadväzujú. Text je vo všeobecnosti zrozumiteľný, avšak niektoré definície neboli formulované dostatočne jasne. Problematické boli najmä definície uvedené v sekcii „Two-way Alternating Automata“. Rovnako definícia 4.1 „Regex Constraint Graph“ nebola podľa môjho názoru dostatočne zrozumiteľná a zaslúžila by si podrobnejšie vysvetlenie.
Práca je napísaná solídnou angličtinou. Až na niekoľko miest, kde sa opakovali už uvedené informácie, som si nevšimol závažnejšie jazykové ani typografické chyby.
V práci sú využité a vhodne citované relevantné vedecké články. Prevzaté časti sú riadne odlíšené od vlastných výsledkov.
Študent implementoval navrhnutú metódu do nástroja Z3-Noodler, otestoval jej korektnosť porovnaním s nástrojmi na vyhľadávanie pomocou regulárnych výrazov na vhodne zvolených benchmarkoch a porovnal ju s nástrojom Black Ostrich. Implementácia je kvalitná a vhodne okomentovaná. Experimentálne vyhodnotenie ukazuje, že navrhnutá metóda je korektná a na benchmarkoch, ktoré dokážu vyriešiť ako Z3-Noodler, tak aj Black Ostrich, je rýchlejšia.
Spracovanie rozšírených regulárnych výrazov predstavuje významné rozšírenie možností nástroja Z3-Noodler a robí ho výrazne silnejším a praktickejším pre reálne použitie.
Evaluation level: obtížnější zadání
Grade proposed by reviewer: A
Responsibility: Mgr. et Mgr. Hana Odstrčilová