Original title: Automaty v rozhodovacích procedurách a formální verifikaci
Translated title: Automata in Decision Procedures and Formal Verification
Authors: Janků, Petr ; Meyer, Roland (referee) ; Janota, Mikoláš (referee) ; Holík, Lukáš (advisor)
Document type: Doctoral theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
V této práci navrhneme rychlou redukci splnitelnosti formulí v straight-line a acyklickém fragmentu na problém prázdnosti alternujících konečných automatů (AFA), která je ve většině případů polynomiální. Tato redukce v kombinaci s pokročilými algoritmy pro kontrolu modelů, jako je IC3, poskytuje první praktický algoritmus pro řešení omezení nad řetězci zahrnujících konkatenaci, převodníky a regulární omezení. Dále zavedeme nový fragment řetězcových omezení zvaný chain-free a jeho relaxaci zvanou weakly chaninng spolu s rozhodovacími procedurami pro tyto fragmenty. Je důležité zmínit, že tyto nové fragmenty zobecňují jak straight-line fragment, tak acyklickou formu. Navíc představíme metodu pro ověření splnitelnosti omezení nad řetězci, zejména s převodem mezi řetězci a čísly, pomocí parametrických plochých automatů (PFA). Tento postup je doplněn o algoritmus pro převod omezení nad řetězci na lineární formule v polynomiálním čase s prohledávacím prostorem ohraničeným PFA. Na závěr navrhneme vylepšenou Parikhovu abstrakci pro řešení délkových omezení pro straight-line fragment. In this thesis, we propose a fast reduction of the satisfiability of formulae in the straight-line and acyclic fragments to the emptiness problem of alternating finite-state automata (AFA), which is polynomial in most cases. This reduction, in combination with advanced model checking algorithms such as IC3, provides the first practical algorithm for solving string constraints involving concatenation, finite-state transducers and regular constraints. Furthermore, we introduce a new fragment of string constraints called chain-free and its relaxation called weakly chaninng, along with decision procedures for these fragments. It is important to mention that these new fragments generalize both the straight-line fragment and the acyclic form. Additionally, we presented a method for checking the satisfiability of string constraints, in particular with string-to-number conversion, using parametric flat automata (PFA). This procedure is complemented by an algorithm for converting string constraints to linear formulas in polynomial time with a search space bounded by PFA. In conclusion, we propose and integrate an improved Parikh abstraction into the string solver sloth for solving length constraints.
Keywords: Automaty; IC3; Omezení řetězců; Parikhův obraz.; Rozhodovací procedura; Splnitelnost modulo teorií (SMT); Střídavé konečné automaty; Verifikace programů; Řešení řetězců; Alternating finite automata; Automata; Decision procedure; IC3; Parikh image.; Program verification; Satisfiability modulo theories; String constraints; String solving

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

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


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