|
|
Knihovna pro profilování datových struktur programů C/C++
Pavela, Jiří ; Rogalewicz, Adam (oponent) ; Fiedor, Tomáš (vedoucí práce)
Výkonnostní chyby mohou do velké míry negativně ovlivnit kvalitu vyvíjeného systému a v některých kritických odvětvích způsobit nevratné škody. K nalezení těchto chyb je obvykle využita profilace v současnosti jedna z nejvíce rozšířených technik výkonnostní analýzy. Přestože existují rozšířené profilovací nástroje, tak většina z nich postrádá srozumitelný grafický výstup a schopnost detailnějšího studia složitostí algoritmů. Tato práce představuje nový profilovací nástroj zaměřený právě na automatizovaný odhad složitostí algoritmů a operací nad dynamickými datovými strukturami. Principem navrženého řešení je sběr statistických dat z běhu programu a následné provedení regresní analýzy s cílem nalézt model, který nejvhodněji reprezentuje složitost algoritmu. Výsledný prototyp byl podroben sérii experimentů, které vyhodnocují přesnost produkovaných výsledků, demonstrují praktická využití nástroje a názorně představují jeho grafický výstup.
|
|
|
Existující útoky na SSL/TLS
Lysoněk, Milan ; Smrčka, Aleš (oponent) ; Fiedor, Tomáš (vedoucí práce)
SSL/TLS je moderní kryptografický protokol, který zabezpečuje komunikaci mezi klientem a serverem. Avšak na tento protokol existují útoky, které mohou ohrozit komunikaci buď odposloucháváním nebo jejím narušením. Obrana proti těmto útokům a testování zranitelností protokolů je ale značně náročný proces. Tato práce popisuje zranitelnosti SSL/TLS protokolu a implementuje vybrané útoky v tlsfuzzeru --- nástroj pro testování SSL/TLS implementací. Výsledná implementace útoků je demonstrována na třech SSL/TLS implementacích.
|
|
|
Automatická tvorba testovacích případů z datových toků
Kraut, Daniel ; Fiedor, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá automatickou tvorbou testovacích případů na úrovni jednotkového testování, pro zdrojové texty v jazyce C. K dosažení automatizace jsou použity metody přístupu k software jako k datovým tokům proměnných. Je zde nastíněn náhled na průběh tvorby testů a funkci CSP solverů, které jsou nezbytnou částí pro rozhodnutelnost těhto problémů. Statická analýza kódu je umožněna knihovnou LibTooling v projektu překladačového front-endu Clang. Jsou uvedeny výstupy z aplikace, jimiž jsou automaticky vytvořené vstupní hodnoty pro testovací případy.
|
|
|
Synthesizing Non-Termination Proofs from Templates
Martiček, Štefan ; Fiedor, Tomáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
One of the properties that are most difficult to verify in the area of formal analysis is liveness. Proving non-termination of programs also belongs to the methods that verify this property. Our work describes the design and implementation of two algorithms checking non-termination. We inspire ourselves by already existing approaches, such as recurrence sets and over-approximation of loops with the use of invariants in the form of recurrence relations. The main challenge for us was an adaptation of these algorithms to the SSA (single static assignment) representation used in 2LS and the overall integration in our framework. We were able to unify the mentioned approaches into analysis of non-termination, which achieves the best results in comparison to the other tools that were compared at the SV-COMP 2017 competition.
|
|
|
Firefox OS Application for Learning Languages
Chudík, Jakub ; Fiedor, Tomáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis deals with creating a language learning application specifically for the Friefox OS operating system for mobile, handheld devices. Because of its nature, the application's user interface attempts to cater specifically to the ergonomic needs of applications for handheld devices. It applies several concepts of gamification to improve the language learning process, the results of which are presented and evaluated. The application also brings its own unique features to make it stand out among existing state of art language learning applications.
|
|
|
Integrace IBM SoftLayer do prostředí ManageIQ
Coufal, Tomáš ; Fiedor, Tomáš (oponent) ; Rogalewicz, Adam (vedoucí práce)
Cloudová řešení získávají na popularitě, spolu s tím však roste jejich složitost. Pro jejich efektivní správu a řízení existují různá řešení. Projekt ManageIQ je jedním z těchto nástrojů. Tato bakalářská práce se zabývá integrací nového poskytovatele cloudové infrastruktury, IBM SoftLayeru, do prostředí správce cloudových řešení ManageIQ. Na tomto příkladě je vysvětleno, jaká rozhraní je třeba použít pro správu poskytovatelů, jak pracovat s cloudovými API a jaké výzvy je třeba řešit při integraci nového poskytovatele. Výsledkem práce je funkční prostředí umožnující snadnou práci v IBM SoftLayeru skrze ManageIQ. To uživateli zprostředkovává sledování a úpravy dostupných zařízení či vytváření a spouštění nových součástí infrastruktury.
|
|
|
Nástroj pro správu Active Directory
Radimák, Samuel ; Křena, Bohuslav (oponent) ; Fiedor, Tomáš (vedoucí práce)
Jedným z kľúčových faktorov v oblasti informačných technológií sú ľudia. Ľudia v zamestnaní často používajú rôzne zdroje, ktoré im daná firma ponúka, pričom tieto zdroje je možné nájsť v rôznych tvaroch a veľkostiach - počítače, tlačiarne, telefóny, e-maily, softvér atď. Avšak každá správna firma potrebuje korektne nastaviť politiku správy daných zdrojov. Adresárové služby sú dlhodobo známym konceptom a dnes sú už široko používaným štandardom firiem po celom svete, kde pomáhajú v efektívnom riadení a zoskupovaní dostupných zdrojov firmy. Táto práca je zameraná na adresárové služby Microsoft Active Directory. Ponúka hlavné koncepty a základy technológie Active Directory. V práci sú predstavené logické a fyzické komponenty Active Directory. Active Directory je pôvodná technológia spoločnosti Microsoft, avšak časom sa začali objavovať systémy podporujúce Active Directory na linuxových operačných systémoch. Táto práca sa zaoberá rozdielmi medzi Active Directory v operačných systémoch Windows Server a ďalších operačných systémov založených na Linuxe. Najdôležitejšie riešenie zo všetkých alternatív k Microsoft, Samba4, bol rozšírený o podporu Active Directory a úspešne kopíruje originálnu funkcionalitu. Stáva sa tým legitímnou alternatívou k použitiu Windows Server, s ktorým má v súčasnej dobe porovnateľnú funkcionalitu. V práci sa nachádza rozbor danej funkcionality a opísané sú aj obmedzujúce faktory daných systémov. Ako ďalšia alternatíva k predchádzajúcim riešeniam je poskytnutý aj popis systému Zentyal, ktorý je komerčnou implementáciou systému Samba4 a preto disponuje podobnými vlastnosťami ako Samba4. Hlavným cieľom tejto práce je skutočná správa objektov v Active Directory, preto sú v práci predstavené existujúce aplikácie umožňujúce správu týchto objektov. Sám Microsoft ponúka balík základných nástrojov pre správu, ktoré sú porovnané s výberom pokročilejších komerčných nástrojov. Zobrazený je aj zoznam výhod a nevýhod každej z daných aplikácií. Na základe popisu funkcionality existujúcich aplikácií pre správu domény sú identifikované niektoré chýbajúce vlastnosti takýchto aplikácií. Podľa týchto vlastností je predstavený nový koncept aplikácie, ktorý je porovnaný s existujúcimi riešeniami a ukazuje benefity tohto konceptu. Tento návrh je následne implementovaný, pričom nová aplikácia podporuje správu používateľov a skupín a takisto ponúka rozšírenia ako úpravu profilových fotiek a prispôsobenie procesu vytvárania objektov. Na základe výsledkov testovania aplikácie sú predstavené možnosti budúceho rozširovania tohto projektu o nové vlastnosti.
|
|
|
Překladač jazyka C v prostředí Python
Fiedor, Tomáš ; Bidlo, Michal (oponent) ; Vašíček, Zdeněk (vedoucí práce)
V současné době neexistuje žádné výrazné propojení problematiky tvorby překladačů a návrhu procesorů a jejich instrukčních sad ve výuce. Cílem této práce je vytvořit snadno rozšiřitelný modulární překladač, který bude umožňovat experimentovat s instrukční sadou použitého cílového procesoru. Překladač implementuje několik optimalizačních technik, jejichž vliv je v práci diskutován. Jednou z pokročilejších použitých technik je kontextové generování cílového kódu, které vykazuje mnohem lepší metriky výsledného kódu v porovnání s prostým slepým generování.
|
|
|
A Decision Procedure for the WSkS Logic
Fiedor, Tomáš ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Various types of logics are often used as a means for formal specification of systems. The weak monadic second-order logic of k successors (WSkS) is one of these logics with quite high expressivity, yet still decidable. Although the complexity of checking satisfiability of a WSkS formula is not even in the ELEMENTARY class, there are approaches to this problem based on deterministic tree automata that perform well in practice, like the MONA tool that efficiently solves the class of practical formulae, but fails for some others. This work extends the class of practically solvable formulae with the use of recently developed techniques for efficient manipulation of non-deterministic automata (such as the antichains algorithm for testing universality) and designs a new decision procedure using non-deterministic automata. The procedure is implemented and is compared with the MONA tool and for some cases yield better results than MONA.
|
|
| |
host ::
RSS.