|
|
Plugins for Getting Information about the System for BusyBox
Poláček, Marek ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
In this thesis, we discuss implementation of tools for getting information from the system. We examine file systems sysfs and procfs in the Linux operating system. Furthermore, we discourse how to write small programs in the C language. Eventually, we take a look at implementation of tools like iostat, mpstat and powertop. These tools were implemented in a minimalistic form suitable for Busybox within this thesis.
|
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.
|
|
|
Prefix Restriction of Regulated Grammar Systems
Konečný, Filip ; Lukáš, Roman (referee) ; Meduna, Alexandr (advisor)
This thesis studies grammar systems whose components use sequences of productions whose left-hand sides are formed by nonterminal strings, not just single nonterminals. It introduces three restrictions on the derivations in these grammar systems. The first restriction requires that all rewritten symbols occur within the first l symbols of the first continuous block of nonterminals in the sentential form during every derivation step. The second restriction defines derivations over sentential forms containing no more than m continuous blocks of nonterminals. The third restriction extends the second in the way that each sequence of nonterminals must be of length h or less. As its main result, the thesis demonstrates that two of these restrictions decrease the generative power of grammar systems.
|
|
|
An Efficient Finite Tree Automata Library
Lengál, Ondřej ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
Numerous computer systems use dynamic control and data structures of unbounded size. These data structures have often the character of trees or they can be encoded as trees with some additional pointers. This is exploited by some currently intensively studied techniques of formal verification that represent an infinite number of states using a finite tree automaton. However, currently there is no tree automata library implementation that would provide an efficient and flexible support for such methods. Thus the aim of this Mas- ter's Thesis is to provide such a library. The present paper first describes the theoretical background of finite tree automata and regular tree languages. Then it surveys the cur- rent implementations of tree automata libraries and studies various verification techniques, outlining requirements for the library. Representation of a finite tree automaton and algo- rithms that perform standard language operations on this representation are proposed in the next part, which is followed by description of library implementation. Through a series of experiments it is shown that the library can compete with other available tree automata libraries, in certain areas being even significantly superior to them.
|
|
|
Hodnocení vybraného elektrického vlhkoměru při měření vlhkosti dřeva smrku v průběhu procesu navlhání
Konečný, Filip
The content of this bachelor's thesis deals with the measurement of the moisture content of spruce wood (Picea abies (L.) Karst.) in the wetting process. Spruce wood was added to zero moisture (w = 0%) and then stored in an air-conditioned room. Wood moisture was measured using an Orion 950 dielectric hygrometer. The moisture values measured on this hygrometer were subsequently compared with the actual moisture found, which was determined using the gravimetric method. The interface of the selected hygrometer enables the setting of the wood density value as well, thus allowing the comparison of the wood moisture with the actual density and with the table density given in the tables from the wood hygrometer manufacturer. The measured spruce wood samples were divided into two groups of 15 pieces each, namely samples without defects or with only minimal defects, and samples with larger defects, especially with resin streaks or knots. Most accurately, the hygrometer measured with the actual density of the samples for both groups. There was always a very significant difference of values when the table density was set.
|
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.
|
|
|
Plugins for Getting Information about the System for BusyBox
Poláček, Marek ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
In this thesis, we discuss implementation of tools for getting information from the system. We examine file systems sysfs and procfs in the Linux operating system. Furthermore, we discourse how to write small programs in the C language. Eventually, we take a look at implementation of tools like iostat, mpstat and powertop. These tools were implemented in a minimalistic form suitable for Busybox within this thesis.
|
|
|
An Efficient Finite Tree Automata Library
Lengál, Ondřej ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
Numerous computer systems use dynamic control and data structures of unbounded size. These data structures have often the character of trees or they can be encoded as trees with some additional pointers. This is exploited by some currently intensively studied techniques of formal verification that represent an infinite number of states using a finite tree automaton. However, currently there is no tree automata library implementation that would provide an efficient and flexible support for such methods. Thus the aim of this Mas- ter's Thesis is to provide such a library. The present paper first describes the theoretical background of finite tree automata and regular tree languages. Then it surveys the cur- rent implementations of tree automata libraries and studies various verification techniques, outlining requirements for the library. Representation of a finite tree automaton and algo- rithms that perform standard language operations on this representation are proposed in the next part, which is followed by description of library implementation. Through a series of experiments it is shown that the library can compete with other available tree automata libraries, in certain areas being even significantly superior to them.
|
|
|
Prefix Restriction of Regulated Grammar Systems
Konečný, Filip ; Lukáš, Roman (referee) ; Meduna, Alexandr (advisor)
This thesis studies grammar systems whose components use sequences of productions whose left-hand sides are formed by nonterminal strings, not just single nonterminals. It introduces three restrictions on the derivations in these grammar systems. The first restriction requires that all rewritten symbols occur within the first l symbols of the first continuous block of nonterminals in the sentential form during every derivation step. The second restriction defines derivations over sentential forms containing no more than m continuous blocks of nonterminals. The third restriction extends the second in the way that each sequence of nonterminals must be of length h or less. As its main result, the thesis demonstrates that two of these restrictions decrease the generative power of grammar systems.
|
guest ::
RSS feed.