|
|
Pluginy pro získávání informací o systému pro projekt BusyBox
Poláček, Marek ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se zabývá implementací nástrojů pro získávání informací o operačním systému pro projekt Busybox. Diskutovány jsou souborové systémy sysfs a procfs v operačním systému Linux. Dále se práce zabývá tím, jak vytvářet co nejmenší programy v jazyce C. Také se věnuje struktuře programů iostat, mpstat a powertop. V rámci práce byly vytvořeny minimalistické implementace již existujících nástrojů, zejména z balíku sysstat, který obsahuje například utility iostat a mpstat.
|
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which nonterminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs.
|
|
|
Prefixové omezení řízených gramatických systémů
Konečný, Filip ; Lukáš, Roman (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce studuje gramatické systémy, jejichž komponenty používají pravidla, která mají na levé straně ne jeden neterminál, ale řetězec neterminálů. Práce u těchto gramatických systémů zavádí tři omezení derivace. První vyžaduje, aby k derivaci v každé větné formě došlo v rámci prvních l symbolů v prvním spojitém bloku neterminálů. Druhé omezení definuje derivaci pro větné formy, které obsahují nejvýše m spojitých bloků neterminálů. Třetí omezení rozšiřuje druhé o podmínku, že každý takový blok může být nejvýše délky h. Hlavním výsledkem této práce jsou důkazy o zmenšení generativní síly gramatických systémů u dvou z těchto omezení.
|
|
|
Efektivní knihovna pro práci s konečnými stromovými automaty
Lengál, Ondřej ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Mnoho současných počítačových systémů používá dynamické datové či řídicí struktury předem neomezené velikosti. Tyto datové struktury mají často charakter stromů nebo se dají zakódovat jako stromy s některými dodatečnými ukazateli nad stromovou kostrou. Této skutečnosti využívají některé v současné době intenzivně studované techniky formální verifikace, které reprezentují nekonečně mnoho stavů konečným stromovým automatem. Nicméně v současnosti neexistuje efektivní a flexibilní implementace knihovny pro stromové automaty, která by byla pro tyto techniky vhodná. Cílem této diplomové práce je takovouto knihovnu poskytnout. Předložený text nejdříve popisuje základy teorie konečných stromových automatů a regulárních stromových jazyků. Dále jsou prozkoumány existující implementace knihoven pro stromové automaty a různé verifikační techniky pro systémy se stromovou strukturou. Poté se text zaobírá návrhem reprezentace stromového automatu a algoritmů provádějících standardní jazykové operace nad touto reprezentací, načež následuje popis implementace knihovny. Prostřednictvím provedených experimentů ukazujeme, že knihovna může konkurovat ostatním dostupným knihovnám pro práci se stromovými automaty, přičemž její výkon v určitých oblastech je řádově vyšší.
|
|
|
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
Obsah této bakalářské práce se zabývá měřením vlhkosti dřeva smrku ztepilého (Picea abies (L.) Karst.) v procesu navlhání. Dřevo smrku bylo vysušeno na nulovou vlhkost (w = 0 %), a následně uloženo do klimatizované místnosti. Vlhkost dřeva byla měřena pomocí dielektrického vlhkoměru s označením Orion 950. Hodnoty vlhkosti naměřené na tomto vlhkoměru byla následně porovnávána se skutečně zjištěnou vlhkostí, která byla stanovena pomoci gravimetrické metody. Rozhraní vybraného vlhkoměru umožňuje nastavení i skutečné hodnoty hustoty dřeva, tudíž dovoloval porovnání vlhkosti dřeva se skutečnou hustotou a s nastavenou tabulkovou hustotou dřeva udávanou v tabulkách od výrobce vlhkoměru. Měřené vzorky dřeva smrku byly rozděleny na dvě skupiny po 15 kusech, a to na vzorky bez vad nebo s pouze minimálními vadami, a na vzorky s většími vadami, a to zejména se smolníky nebo suky. Nejpřesněji měřil vlhkoměr při nastavení skutečné hustoty vzorků a to pro obě skupiny. Při nastavení tabulkové hustoty byl vždy velmi významný rozdíl hodnot.
|
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which nonterminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs.
|
|
|
Pluginy pro získávání informací o systému pro projekt BusyBox
Poláček, Marek ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se zabývá implementací nástrojů pro získávání informací o operačním systému pro projekt Busybox. Diskutovány jsou souborové systémy sysfs a procfs v operačním systému Linux. Dále se práce zabývá tím, jak vytvářet co nejmenší programy v jazyce C. Také se věnuje struktuře programů iostat, mpstat a powertop. V rámci práce byly vytvořeny minimalistické implementace již existujících nástrojů, zejména z balíku sysstat, který obsahuje například utility iostat a mpstat.
|
|
|
Efektivní knihovna pro práci s konečnými stromovými automaty
Lengál, Ondřej ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Mnoho současných počítačových systémů používá dynamické datové či řídicí struktury předem neomezené velikosti. Tyto datové struktury mají často charakter stromů nebo se dají zakódovat jako stromy s některými dodatečnými ukazateli nad stromovou kostrou. Této skutečnosti využívají některé v současné době intenzivně studované techniky formální verifikace, které reprezentují nekonečně mnoho stavů konečným stromovým automatem. Nicméně v současnosti neexistuje efektivní a flexibilní implementace knihovny pro stromové automaty, která by byla pro tyto techniky vhodná. Cílem této diplomové práce je takovouto knihovnu poskytnout. Předložený text nejdříve popisuje základy teorie konečných stromových automatů a regulárních stromových jazyků. Dále jsou prozkoumány existující implementace knihoven pro stromové automaty a různé verifikační techniky pro systémy se stromovou strukturou. Poté se text zaobírá návrhem reprezentace stromového automatu a algoritmů provádějících standardní jazykové operace nad touto reprezentací, načež následuje popis implementace knihovny. Prostřednictvím provedených experimentů ukazujeme, že knihovna může konkurovat ostatním dostupným knihovnám pro práci se stromovými automaty, přičemž její výkon v určitých oblastech je řádově vyšší.
|
|
|
Prefixové omezení řízených gramatických systémů
Konečný, Filip ; Lukáš, Roman (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce studuje gramatické systémy, jejichž komponenty používají pravidla, která mají na levé straně ne jeden neterminál, ale řetězec neterminálů. Práce u těchto gramatických systémů zavádí tři omezení derivace. První vyžaduje, aby k derivaci v každé větné formě došlo v rámci prvních l symbolů v prvním spojitém bloku neterminálů. Druhé omezení definuje derivaci pro větné formy, které obsahují nejvýše m spojitých bloků neterminálů. Třetí omezení rozšiřuje druhé o podmínku, že každý takový blok může být nejvýše délky h. Hlavním výsledkem této práce jsou důkazy o zmenšení generativní síly gramatických systémů u dvou z těchto omezení.
|
host ::
RSS.