Thesis Details

Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata

Bachelor's Thesis Student: Kmenta Martin Academic Year: 2021/2022 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
Czech title
Rozvoj nástroje ASMA pro analýzu programů s řetězci pomocí symbolických automatů
Language
English
Abstract

In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.

Keywords

regular model checking, RMC, abstract regular model checking, ARMC, finite automata, transducers, symbolic finite automata, AutomataDotNet, ASMA, VeriFIT, reverse concatenation

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade C
Date
13 June 2022
Reviewer
Lengál Ondřej, Ing., Ph.D.
Committee
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áš, 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
Citation
KMENTA, Martin. Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata. Brno, 2022. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2022-06-13. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/25149/
BibTeX 
@bachelorsthesis{FITBT25149,
    author = "Martin Kmenta",
    type = "Bachelor's thesis",
    title = "Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2022,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/25149/"
}

Theses

Back to top