Thesis Details

Nástoj pro abstraktní regulární stromový model checking

Bachelor's Thesis Student: Mráz Patrik Academic Year: 2016/2017 Supervisor: Hruška Martin, Ing.
English title
Tool for Abstract Regular Tree Model Checking
Language
Czech
Abstract

Formal verification deals with proving the correctness of the system according to the given specifications. Its need is driven by an increasing number of computers and a increase in the complexity of the systems being developed. The aim of this work is to implement the formal verification tool abstract regular tree model checking (ARTMC) over the VATA library. To achieve this goal, it was necessary to extend the VATA library on the finite tree transducers, abstractions of tree automata and integrate them together with the ARTMC into the VATA library.

Keywords

abstract regular tree model checking, ARTMC, tree automata, tree transducer, abstraction, VATA

Department
Degree Programme
Information Technology
Files
Status
defended, grade D
Date
16 June 2017
Reviewer
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Hanáček Petr, doc. Dr. Ing. (DITS FIT BUT), člen
Kořenek Jan, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Veselý Vladimír, Ing., Ph.D. (DIFS FIT BUT), člen
Citation
MRÁZ, Patrik. Nástoj pro abstraktní regulární stromový model checking. Brno, 2017. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2017-06-16. Supervised by Hruška Martin. Available from: https://www.fit.vut.cz/study/thesis/19056/
BibTeX
@bachelorsthesis{FITBT19056,
    author = "Patrik Mr\'{a}z",
    type = "Bachelor's thesis",
    title = "N\'{a}stoj pro abstraktn\'{i} regul\'{a}rn\'{i} stromov\'{y} model checking",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2017,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/19056/"
}
Back to top