Thesis Details

Verifikace programů s ukazateli založená na detekci vzorů

Bachelor's Thesis Student: Kubíček Jan Academic Year: 2006/2007 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
English title
Verification of Programs with Pointers Based on Pattern Detection
Language
Czech
Abstract

This paper presents our results in study of verifiaction of infinite state space systems. We deal more concretely with abstract model checking. As main part of study we learned about pattern-based verification. This method is supposed to verify programs with dynamic memory structures like lists. Those structures are presented as directed graph. Pattern-based verifiaction abstracts any number of nodes by replacing them with summarized node. This way we achieve bounded  presentation of unbounded memory structure. Afterwards, verification is very effective due to low number of possible memory configurations. In our own work we deal with making model of a program for a tool that implements pattern-based verification. This model isconstructed from a subset of the C language. The main contribution of work is making the verification of simple programs written in C language completely self-acting by automation of constructing input model. In this paper wepresent the grammar of created subset of the C language and implementation details of translation.

Keywords

system, verification, formal verification, pattern based verification, dynamic memory structure, pattern, sumarization, materialization, model, overaproximation, non-determinism, C language

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade B
Date
12 June 2007
Reviewer
Erlebach Pavel, Ing.
Committee
Meduna Alexander, prof. RNDr., CSc. (DIFS FIT BUT), předseda
Herout Pavel, doc. Ing., Ph.D. (WBU in Pilsen), člen
Lukáš Roman, Ing., Ph.D. (DIFS FIT BUT), člen
Růžička Richard, doc. Ing., Ph.D., MBA (DCSY FIT BUT), člen
Strnadel Josef, Ing., Ph.D. (DCSY FIT BUT), člen
Zbořil František, doc. Ing., Ph.D. (DITS FIT BUT), člen
Citation
KUBÍČEK, Jan. Verifikace programů s ukazateli založená na detekci vzorů. Brno, 2007. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2007-06-12. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/5406/
BibTeX 
@bachelorsthesis{FITBT5406,
    author = "Jan Kub\'{i}\v{c}ek",
    type = "Bachelor's thesis",
    title = "Verifikace program\r{u} s ukazateli zalo\v{z}en\'{a} na detekci vzor\r{u}",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2007,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/5406/"
}

Theses

Back to top