Thesis Details

Překladač grafu toků dat do logiky bitových vektorů

Bachelor's Thesis Student: Sušovský Tomáš Academic Year: 2015/2016 Supervisor: Smrčka Aleš, Ing., Ph.D.
English title
A Bit-Vector Compiler for Data-Flow Graphs
Language
Czech
Abstract

The principal goal of this bachelor thesis is to design and implement a tool for compiling data-flow graph models to SMT-LIB format. This thesis builds on the research project HADES developed by VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The solution uses compiler for generating object model from original graph. Object model can be converted to a SMT-LIB format description including assertions of the desired system properties. Loop unrolling method (with user defined boundary for unrollment) is used for verification of system properties depending on changes in state of model. Capabilities of the developed tool are demonstrated on set of data-flow graphs models. Models cover usage of all elements defined in VAM language (input format) and their combinations. Result of this thesis presents new ways of processing data-flow graphs in VAM format and their verification.

Keywords

Formal verification, SMT, data-flow graphs, VAM, compilers

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade C
Date
15 June 2016
Reviewer
Lengál Ondřej, Ing., Ph.D.
Committee
Meduna Alexander, prof. RNDr., CSc. (DIFS FIT BUT), předseda
Burget Lukáš, doc. Ing., Ph.D. (DCGM FIT BUT), člen
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Jaroš Jiří, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Křivka Zbyněk, Ing., Ph.D. (DIFS FIT BUT), člen
Citation
SUŠOVSKÝ, Tomáš. Překladač grafu toků dat do logiky bitových vektorů. Brno, 2016. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2016-06-15. Supervised by Smrčka Aleš. Available from: https://www.fit.vut.cz/study/thesis/18543/
BibTeX 
@bachelorsthesis{FITBT18543,
    author = "Tom\'{a}\v{s} Su\v{s}ovsk\'{y}",
    type = "Bachelor's thesis",
    title = "P\v{r}eklada\v{c} grafu tok\r{u} dat do logiky bitov\'{y}ch vektor\r{u}",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2016,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/18543/"
}

Theses

Back to top