|
|
Lidské rozhraní k automatovým knihovnám nástroje MONA
Pyšný, Radek ; Šimáček, Jiří (oponent) ; Rogalewicz, Adam (vedoucí práce)
Konečné stromové automaty jsou formalismem používaným v mnoha různých oblastech informatiky, mimo jiné v oblasti formální verifikace. V současné době existuje několik nástrojů pro práci s konečnými stromovými automaty, avšak knihovny nástroje MONA jsou pro tyto účely nejlepší. Právě konečné stromové automaty jsou častým nástrojem pro formální verifikaci počítačových systémů, které pracují s dynamickými datovými strukturami. Způsob, jakým je realizováno zadávání konečných stromových automatů pro knihovny nástroje MONA , je pro člověka značně náročný, protože je nutné funkci přechodu konečného stromového automatu zadat ve formě několika multiterminálních binárních rozhodovacích diagramů. Cílem této diplomové práce je navrhnout a implementovat nástroj pro převod konečných stromových automatů zapsaných výčtem pravidel do interního formátu nástroje MONA .
|
|
|
Omezení větných forem gramatik s rozptýleným kontextem
Šimáček, Jiří ; Masopust, Tomáš (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce zavádí pojem zobecněných gramatik s rozptýleným kontextem, které se od tradičních liší tím, že levé strany pravidel mohou obecně obsahovat řetězec neterminálních symbolů namísto jediného neterminálu. Dále jsou studovány dva typy omezení při větné derivaci v těchto gramatikách. Nechť k je konstanta. První omezení požaduje, aby přepsání všech symbolů nastalo mezi prvními k symboly v prvním souvislém bloku neterminálů ve větné formě v každém derivačním kroku. Druhé omezení definuje derivaci pouze nad větnými formami, které obsahují nejvýše k výskytů neterminálů. Jako hlavní výsledek práce demonstruje, že oba typy omezení snižují vyjadřovací sílu na úroveň bezkontextových gramatik.
|
|
|
Automatická formální verifikace korektnosti programů v nástrojích SDV, Copper a podobných
Kovalič, Peter ; Šimáček, Jiří (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se věnuje verifikaci ovládačů. Používají se při tom model checkery, hlavní z nich je Static Driver Verifier. Pomocí něj se kontroluje zvolený ovládač Ext2Fsd. Patří do skupiny ovládačů souborových systémů. Kontrola probíhá podle zadaných pravidel, které nesmí ovládač porušovat. Cílem práce bylo vybraný ovládač verifikovat pomocí zvoleného nástroje. Ve výsledcích bylo dosaženo stavu, kdy se ve verifikovaném ovládači objevili všechny tři dostupné možnosti výsledku ovládač splňoval některá pravidla, některá odhalily jeho chyby a jiné nebyly aplikovatelné. Na konci této práce se nachází ještě kapitola, věnována dalšímu model checkeru, s názvem Copper, která poskytuje základní poznatky o tomto nástroji.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating
|
|
|
Lidské rozhraní k automatovým knihovnám nástroje MONA
Pyšný, Radek ; Šimáček, Jiří (oponent) ; Rogalewicz, Adam (vedoucí práce)
Konečné stromové automaty jsou formalismem používaným v mnoha různých oblastech informatiky, mimo jiné v oblasti formální verifikace. V současné době existuje několik nástrojů pro práci s konečnými stromovými automaty, avšak knihovny nástroje MONA jsou pro tyto účely nejlepší. Právě konečné stromové automaty jsou častým nástrojem pro formální verifikaci počítačových systémů, které pracují s dynamickými datovými strukturami. Způsob, jakým je realizováno zadávání konečných stromových automatů pro knihovny nástroje MONA , je pro člověka značně náročný, protože je nutné funkci přechodu konečného stromového automatu zadat ve formě několika multiterminálních binárních rozhodovacích diagramů. Cílem této diplomové práce je navrhnout a implementovat nástroj pro převod konečných stromových automatů zapsaných výčtem pravidel do interního formátu nástroje MONA .
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating
|
|
|
Automatická formální verifikace korektnosti programů v nástrojích SDV, Copper a podobných
Kovalič, Peter ; Šimáček, Jiří (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se věnuje verifikaci ovládačů. Používají se při tom model checkery, hlavní z nich je Static Driver Verifier. Pomocí něj se kontroluje zvolený ovládač Ext2Fsd. Patří do skupiny ovládačů souborových systémů. Kontrola probíhá podle zadaných pravidel, které nesmí ovládač porušovat. Cílem práce bylo vybraný ovládač verifikovat pomocí zvoleného nástroje. Ve výsledcích bylo dosaženo stavu, kdy se ve verifikovaném ovládači objevili všechny tři dostupné možnosti výsledku ovládač splňoval některá pravidla, některá odhalily jeho chyby a jiné nebyly aplikovatelné. Na konci této práce se nachází ještě kapitola, věnována dalšímu model checkeru, s názvem Copper, která poskytuje základní poznatky o tomto nástroji.
|
|
|
Implementace pluginů pro ifplugd do projektu BusyBox
Kryzhanovskyy, Maksym ; Šimáček, Jiří (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se zabývá portovanim démona ifplugd do projektu BusyBox. První část textu poskytuje úvodní informace o projektu BusyBox a nahlíží do struktury aplikace. Druhá část textu se zabývá implementaci démona ifplugd. V rámci teto práce byly provedené dílčí úpravy v kódu BusyBox a démon ifplugd implementován v podobě appletu do balíku BusyBox. V závěru této práce jsou diskutované dosažené výsledky.
|
|
|
Omezení větných forem gramatik s rozptýleným kontextem
Šimáček, Jiří ; Masopust, Tomáš (oponent) ; Meduna, Alexandr (vedoucí práce)
Tato práce zavádí pojem zobecněných gramatik s rozptýleným kontextem, které se od tradičních liší tím, že levé strany pravidel mohou obecně obsahovat řetězec neterminálních symbolů namísto jediného neterminálu. Dále jsou studovány dva typy omezení při větné derivaci v těchto gramatikách. Nechť k je konstanta. První omezení požaduje, aby přepsání všech symbolů nastalo mezi prvními k symboly v prvním souvislém bloku neterminálů ve větné formě v každém derivačním kroku. Druhé omezení definuje derivaci pouze nad větnými formami, které obsahují nejvýše k výskytů neterminálů. Jako hlavní výsledek práce demonstruje, že oba typy omezení snižují vyjadřovací sílu na úroveň bezkontextových gramatik.
|
host ::
RSS.