Original title: Rozhodovací procedura založená na automatech
Translated title: An Automata-Based Decision Procedure
Authors: Hečko, Michal ; Češka, Milan (referee) ; Lengál, Ondřej (advisor)
Document type: Bachelor's theses
Year: 2022
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Presburgerova aritmetika (PrA) je rozhodnutelná teorie přirozených čísel prvního řádu, která nachází uplatnění v mnoha oblastech formální verifikace vlastností softwaru. Řešiče SMT nástroje implementující různé algoritmické přístupy k rozhodování, zda má formule řešení hrají ve formální verifikaci klíčovou roli. V této práci dokumentujeme vytvoření nového automatického SMT řešiče pro PrA založeného na konečných automatech přístupu, který v současnosti žádný SMT řešič nepoužívá. Uvádíme přehled výzev a jejich řešení vyplývajících ze složitosti takového nástroje, včetně výsledků z provedených experimentů, které již identifikují problémy, kde tento alternativní přístup překonává nejmodernější řešiče. Uvádíme také identifikované problémy, u nichž výkonnost postupu založeného na automatech naráží na problémy, které představují otevřené možnosti výzkumu. Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
Keywords: Celočíselná lineárna aritmetika; Konečný automat; Presburgerova aritmetika; SMT solver; Finite automaton; Linear integer arithmetic; Presburger arithmetic; SMT solver

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/207325

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


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