Thesis Details
An Automata-Based Decision Procedure
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.
Presburger arithmetic, SMT solver, Linear integer arithmetic, Finite automaton
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Martínek Tomáš, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Peringer Petr, Dr. Ing. (DITS FIT BUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT), člen
@bachelorsthesis{FITBT24744, author = "Michal He\v{c}ko", type = "Bachelor's thesis", title = "An Automata-Based Decision Procedure", school = "Brno University of Technology, Faculty of Information Technology", year = 2022, location = "Brno, CZ", language = "english", url = "https://www.fit.vut.cz/study/thesis/24744/" }