|
|
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.
|
|
|
The rationalization of Construction price statistics
Zeman, Petr ; Konečný, František (referee) ; Nový, Martin (advisor)
The subject of the thesis "Rationalization of Construction price statistics" is to outline the issue of reporting of construction activities in the Czech Republic and try to be as simple as possible for statistical purposes, if possible. From a theoretical approach for construction work price indices and their stats go over to the practical part calculation of indices. Available data from the Czech Statistical Office on price indices of building work in recent years converted in terms of weights of permanent representatives from the perspective of individual statements. The goal is, to find a satisfying combination of representatives of both methodological procedures and exclude them from the forms for reporting. This should be saved in time statistical survey of individual respondents and abridged interpretation of outputs of the Czech Statistical Office.
|
|
|
Flexible textile-integrated coils for inductive energy transfer
Konečný, František ; Cupal, Miroslav (referee) ; Raida, Zbyněk (advisor)
This work aims to describe the design of flexible textile coils in several variants (different coil dimensions, different designs). The parameters of the designed coils will be verified using simplified simulation models and compared with theoretical calculations. Further, the work deals with the practical design of coils, including the measurement of their basic parameters and determination the efficiency of inductive power transfer.
|
|
|
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.
|
|
|
Flexible textile-integrated coils for inductive energy transfer
Konečný, František ; Cupal, Miroslav (referee) ; Raida, Zbyněk (advisor)
This work aims to describe the design of flexible textile coils in several variants (different coil dimensions, different designs). The parameters of the designed coils will be verified using simplified simulation models and compared with theoretical calculations. Further, the work deals with the practical design of coils, including the measurement of their basic parameters and determination the efficiency of inductive power transfer.
|
|
|
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.
|
guest ::
RSS feed.