Název: Délky v řešení řetězcových omezení
Překlad názvu: Length Constraints in String Solving
Autoři: Hranička, Jan ; Lengál, Ondřej (oponent) ; Havlena, Vojtěch (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]
Řešení řetězcových omezení je v dnešní době základním kamenem formální verifikace s širokým vědeckým i obchodním uplatněním. Přínosem této práce je návrh nové rozhodovací procedury s cílem rozšířit jeden z předních string solverů: Z3-Noodler. Tato rozhodovací procedura je založena na symbolickém zarovnání řetězcových proměnných v rovnicích pomocí generování omezení na jejich délky. Experimenty na standartních benchmarcích ukázaly, že integrace této procedury s nástrojem Z3-Noodler vede ke snížení timeoutů o 32 a na určitých testech snižuje celkovou dobu běhu nástroje více než padesátkrát. Díky těmto přínosům je možné očekávat přidání této procedury do zmíněného nástroje. String solving is currently a fundamental part of formal verification with numerous scientific and business applications. In this thesis, a new decision procedure is proposed with the intend to extend a state-of-the-art string solver Z3-Noodler. This decision procedure is based on symbolically aligning string variables in word equations by generating constraints on their lengths. When experimenting with this procedure on standardized benchmarks, its integration with Z3-Noodler resulted in the reduction of 32 timeouts and in some instances more than 50x time improvement. These benefits make it possible for this decision procedure to be included in a future release of the mentioned solver.
Klíčová slova: length constraints; SMT solver; string solving; Z3; délková omezení; SMT solver; Z3; ř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/246592

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


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