Original title: Verifikace programů s ukazateli založená na detekci vzorů
Translated title: Verification of Programs with Pointers Based on Pattern Detection
Authors: Kubíček, Jan ; Erlebach, Pavel (referee) ; Vojnar, Tomáš (advisor)
Document type: Bachelor's theses
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace  pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu. 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: C language; dynamic memory structure; formal verification; materialization; model; non-determinism; overaproximation; pattern; pattern based verification; sumarization; system; verification; dynamická paměťová struktura; formální verifikace; jazyk C; materializace; model; nadaproximace; nedeterminismus; sumarizace; systém; verifikace; verifikace na základě paměťových vzorů; vzor

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/56273

Permalink: http://www.nusl.cz/ntk/nusl-239323


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses