Název: Řešení řetězcových omezení pomocí Parikhových obrazů
Překlad názvu: String Constraint Solving Through Parikh Images
Autoři: Bartoš, Petr ; Havlena, Vojtěch (oponent) ; Holík, Lukáš (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2024
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng] [cze]
Tato bakalářská práce si klade za cíl implementovat alternativní způsob řešení řetězcových omezení pomocí takzvaného flattening algoritmu, který pomocí Parikhových obrazů a parametrických plochých automatů transformuje řetězcová omezení na lineární vzorce. Takto vyjádřené omezení je možné řešit pomocí výkonných SMT solverů a předchází problémům spjatým s tradičně používanými metodami založených na automatech, jako je například exploze stavového prostoru. Práce popisuje teoretické znalosti potřebné k pochopení algoritmu pro řešení a představuje další state of the art způsoby řešení. Výsledky implementace jsou poté porovnány s ostatnímy solvery na klasických soutěžních benchmarcích. Provedené experimenty ukazují smíšené výsledky – ač navržené řešení nedosahuje podobné rychlosti jako state-of-the-art solvery, přesnost podaproximačního přístupu je relativně příznivá. This bachelor thesis aims to implement an alternative way of solving string constraints using the so-called flattening algorithm. The algorithm makes use of Parikh images and parametric flat automata to effectively convert string constraints to linear arithmetic, which allows for leveraging powerful SMT solvers. Solving constraints as an algebraic problem is supposed to be more efficient than standardly used automata-based techniques, as it avoids common pitfalls, such as state-space exposion. The thesis covers the theoretical knowledge required to understand the flattening algorithm and introduces alternative modern solution strategies. The implementation results are then compared to other solvers using conventional competition benchmarks. The conducted experiments show that while the speed of the implementation compared to other state-of-the-art solvers is worse, the effectiveness of the underapproximation itself is fairly promising, thus yielding mixed results.
Klíčová slova: flat automaton; linear formulae; parametric automaton; Parikh image; SMT solving; string constraints; string solving; strings; lineární vzorce; parametrický automat; Parikhův obraz; plochý automat; SMT výpočty; řetězce; řetězcová omezení; řešení řetězcových omezení

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: https://hdl.handle.net/11012/246956

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-618466


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce