Original title: Délky v řešení řetězcových omezení
Translated title: Length Constraints in String Solving
Authors: Hranička, Jan ; Lengál, Ondřej (referee) ; Havlena, Vojtěch (advisor)
Document type: Bachelor's theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [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.
Keywords: délková omezení; SMT solver; Z3; řešení řetězcových omezení; length constraints; SMT solver; string solving; Z3

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: https://hdl.handle.net/11012/246592

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


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses