|
|
Human Interface to Automata Libraries of MONA Tool
Pyšný, Radek ; Šimáček, Jiří (referee) ; Rogalewicz, Adam (advisor)
Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.
|
|
|
A Restriction of Sentetial Forms of of Scattered Context Grammars
Šimáček, Jiří ; Masopust, Tomáš (referee) ; Meduna, Alexandr (advisor)
This work introduces and discusses generalized scattered context grammars that are based upon sequences of productions whose left-hand sides are formed by nonterminal strings, not just single nonterminals. It places two restrictions on the derivations in these grammars. More specifically, let k be a constant. The first restriction requires that rewriting all symbols occurs within the first k symbols of the first continuous block of nonterminals in the sentential form during every derivation step. The other restriction defines the derivations over sentential forms containing no more than k occurrences of nonterminals. As its main result, the thesis demonstrates that both restrictions decrease the generative power of these grammars to the power of context-free grammars.
|
|
|
Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This thesis is concerning about verification of drivers. Principally is focused on model checking tools, from which the Static Driver Verifier is the most important. A driver Ext2Fsd is checked by this program. This driver belongs to group of file system drivers. Control is driven by entered rules, which the driver must not violate. The aim of this thesis was to verify chosen driver by selected tool. The results have covered all three types of verification´s end. There were rules that driver passed, that driver violated and also that driver didn´t accept. The final chapter of work is about another model checking tool Copper. It offers the basic knowledge about this program.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
|
Human Interface to Automata Libraries of MONA Tool
Pyšný, Radek ; Šimáček, Jiří (referee) ; Rogalewicz, Adam (advisor)
Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
|
Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This thesis is concerning about verification of drivers. Principally is focused on model checking tools, from which the Static Driver Verifier is the most important. A driver Ext2Fsd is checked by this program. This driver belongs to group of file system drivers. Control is driven by entered rules, which the driver must not violate. The aim of this thesis was to verify chosen driver by selected tool. The results have covered all three types of verification´s end. There were rules that driver passed, that driver violated and also that driver didn´t accept. The final chapter of work is about another model checking tool Copper. It offers the basic knowledge about this program.
|
|
|
Implementation of an ifplugd Plugin to the BusyBox Project
Kryzhanovskyy, Maksym ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This work deals with porting the ifplugd daemon to BusyBox project. The first part gives introductory information about the BusyBox project, and looks into the structure of the application. The second part deals with the implementation of the ifplugd daemon. As part of this work was carried out partial adjustments in the BusyBox code and ifplugd daemon has been implemented as an applet of the BusyBox package. At the conclusion of this work are discussed the results.
|
|
|
A Restriction of Sentetial Forms of of Scattered Context Grammars
Šimáček, Jiří ; Masopust, Tomáš (referee) ; Meduna, Alexandr (advisor)
This work introduces and discusses generalized scattered context grammars that are based upon sequences of productions whose left-hand sides are formed by nonterminal strings, not just single nonterminals. It places two restrictions on the derivations in these grammars. More specifically, let k be a constant. The first restriction requires that rewriting all symbols occurs within the first k symbols of the first continuous block of nonterminals in the sentential form during every derivation step. The other restriction defines the derivations over sentential forms containing no more than k occurrences of nonterminals. As its main result, the thesis demonstrates that both restrictions decrease the generative power of these grammars to the power of context-free grammars.
|
guest ::
RSS feed.