|
|
Komprese bitových map pomocí Grayova kódu
Škorvaga, David ; Dvořák, Tomáš (vedoucí práce) ; Gregor, Petr (oponent)
Práce se zabývá kompresí bitmapových indexů. Ke zmenšení bitmapových indexů se často používají specializované algoritmy, které hledají dlouhé řetězce stejných bitů. Řádky indexu je pak výhodné vhodně přerozdělit, aby algoritmus poskytoval co nejlepší kompresní poměr. Nalezení optimálního přerozdělení je sice NP-těžký problém, existují však účinné heuristiky, které setřídí index v polynomiálním čase. V poslední době se objevily experimentální studie, které místo klasického lexikografického třídění využívají třídění podle Grayova kódu. V této práci nahrazujeme klasický Grayův kód novou konstrukcí, která generuje komprimovaný Grayův kód. Konstrukci podrobně popisujeme a na reálných i náhodně generovaných datech zkoumáme, zda je při kompresi algoritmem WAH tento kód účinnější než klasický.
|
|
|
Analysis of a File System Using the Verifying C Compiler
Škorvaga, David ; Kofroň, Jan (vedoucí práce) ; Bednárek, David (oponent)
Název práce: Analýza souborového systému pomocí Verifying C Compiler Autor: Bc. David Škorvaga Katedra: Katedra distribuovaných a spolehlivých systémů Vedoucí diplomové práce: RNDr. Jan Kofroň, Ph.D. Abstrakt: Formální verifikace je jeden ze způsobů, jak zlepšit spolehlivost soft- warových systémů. Jeden z přístupů formální verifikace se zaměřuje na dokazo- vaní správnosti anotovaného zdrojového kódu v široce používaném programovacím jazyce. Verifier C Compiler (VCC) je verifikátor pro concurrent C, který přijímá anotovaný kód v jazyce C a automaticky ověřuje jeho správnost s ohledem na tuto anotaci. Už se objevily úspěšné pokusy o ověření některých kritických systémů, včetně jádra operačního systému. Další důležitou součástí operačního systému je jeho systém souborů. V diplomové práci jsme si vybrali souborový systém FatFs, odlehčenou implementaci souborového systému FAT, nezávislou na zařízení. V této práci vytvoříme specifikaci jeho části pomocí anotace VCC a úspěšně ověříme jeho korektnost. Klíčová slova: Formal Verification, File System, VCC
|
|
|
Komprese bitových map pomocí Grayova kódu
Škorvaga, David ; Dvořák, Tomáš (vedoucí práce) ; Gregor, Petr (oponent)
Práce se zabývá kompresí bitmapových indexů. Ke zmenšení bitmapových indexů se často používají specializované algoritmy, které hledají dlouhé řetězce stejných bitů. Řádky indexu je pak výhodné vhodně přerozdělit, aby algoritmus poskytoval co nejlepší kompresní poměr. Nalezení optimálního přerozdělení je sice NP-těžký problém, existují však účinné heuristiky, které setřídí index v polynomiálním čase. V poslední době se objevily experimentální studie, které místo klasického lexikografického třídění využívají třídění podle Grayova kódu. V této práci nahrazujeme klasický Grayův kód novou konstrukcí, která generuje komprimovaný Grayův kód. Konstrukci podrobně popisujeme a na reálných i náhodně generovaných datech zkoumáme, zda je při kompresi algoritmem WAH tento kód účinnější než klasický.
|
host ::
RSS.