Thesis Details

An Automata-Based Decision Procedure

Bachelor's Thesis Student: Hečko Michal Academic Year: 2021/2022 Supervisor: Lengál Ondřej, Ing., Ph.D.
Czech title
Rozhodovací procedura založená na automatech

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

Degree Programme
defended, grade A
13 June 2022
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Martínek Tomáš, 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
HEČKO, Michal. An Automata-Based Decision Procedure. Brno, 2022. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-06-13. Supervised by Lengál Ondřej. Available from:
    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 = ""
Back to top