|
Verifikace ukazatelových programů pomocí lesních automatů
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Holík, Lukáš (vedoucí práce)
V této práci je rozvíjena existující metoda pro shape analýzu programů založená na lesních automatech. Dále je také vylepšována implementace této metody, nástroj Forester. Lesní automaty jsou založeny na stromových automatech, jejichž jednoduchou implementaci Forester obsahuje. Prvním přínosem této práce je nahrazení této implementace knihovnou VATA, která obsahuje efektivní algoritmy pro reprezentaci a manipulaci stromových automatů. Verze nástroje Forester používající knihovnu VATA se zúčastnila mezinárodní soutěže SV-COMP 2015. Dále je verifikace založená na lesních automatech v této práci rozšířena o predikátovou abstrakci a analýzu nalezených protipříkladů. Výsledek této analýzy je možné využít následujícími způsoby. Prvním je určení toho, zda je nalezené chyba reálná nebo naopak nepravá. Druhým je pak zjemnění predikátové abstrakce pomocí predikátů odvozených při zpětném běhu. Obě techniky byly také implementovány v nástroji Forester. Na závěr je zhodnoceno zlepšení, které tyto techniky přinesly oproti původní verzi nástroje Forester.
|
|
Information system to support teaching
Vaško, Ľubomír ; Pecinovský, Rudolf (vedoucí práce) ; Šlajchrt, Zbyněk (oponent)
Cílem diplomové práce je návrh a vývoj jednoduchého informačního systému pro podporu výuky. První část práce se věnuje vysvětlení základních pojmů v oblasti e learningu, výběru systémů k analýze a jejich zhodnocení. Na základě práce s vybranými systémy jsou na začátku druhé části práce stanoveny obecné a funkční požadavky na jednoduchý portál pro podporu výuky, který je alternativou k vybraným robustním systémem. Práce se také zabývá popisem použitých technologií a architekturou vyvinutého systému. V závěrečné části práce je návod k instalaci systému a uživatelské příručky, které obsahují kromě popisu funkcí i náhledy obrazovek systému. Praktickým výstupem z práce je modulární webová aplikace, která je uživatelům dostupná prostřednictvím internetového prohlížeče. Vyvinutý systém je rozšiřitelný o nové moduly. Architektura systému umožňuje rozdělit budoucí vývoj mezi vývojářů věnujícím se tvorbě uživatelské prostředí a vývojářů zabývajících se logikou aplikace.
|
|
Aplikace pro podporu práce studijní referentky pro zpracování výstupů z ISIS
Marek, Lukáš ; Benáčanová, Helena (vedoucí práce) ; Sedláčková, Jana (oponent)
Tato bakalářská práce slouží jako popis vývoje aplikace, která usnadňuje práci studijním referentkám a systémovému integrátorovi fakulty na fakultě Informatiky a statistiky. Aplikace je vyvíjena v programovacím jazyce Visual Basic for Application a je nadstavbou k Integrovanému studijnímu informačnímu systému na Vysoké škole ekonomické v Praze. První část práce se věnuje analýze praxe studijních referentek v přijímacím řízení. Práce rovněž popisuje průběh celého přijímacího řízení. V analytické části jsou specifikována zdrojová a výstupní data a následně požadavky na jednotlivé funkcionality aplikace. Druhá část je věnovaná samotnému vývoji aplikace, a to jak z programového hlediska, tak z hlediska uživatelského. Jsou vysvětleny jednotlivé algoritmy a postupy při řešení problémů. V uživatelské části je stručný návod k tomu, jak aplikaci používat.
|
|
Stanovení disociačních konstant a limitních mobilit vybraných amfolytů
Maliňáková, Lucie ; Riesová, Martina (vedoucí práce) ; Beneš, Martin (oponent)
Kapilární zónová elektroforéza je jednoduchá a automatizovaná metoda, která umožňuje stanovit aciditní disociační konstanty a limitní iontové mobility analytů ze stejné série experimentů za malé spotřeby vzorku. Závislost efektivních mobilit 7 vybraných amfolytů na pH pufru byla experimentálně zjištěna v rozsahu pH 1,6 až 6,8. Sada jednoduchých pufrů s konstantní iontovou silou byla navržena pomocí programu PeakMaster. Analyzované amfolyty byly detekovány bezkontaktním vodivostním detektorem. Použitím dynamického potahování kapiláry se minimalizovala interakce analytů se silanolovými skupinami na vnitřní stěně kapiláry. Experimentálně zjištěné hodnoty efektivních mobilit byly proloženy (fitovány) vhodnou funkcí. Získanými parametry byly aktuální mobility a smíšené disociační konstanty odpovídající příslušné iontové síle. Pomocí rozšířeného Debye- Hückelova zákona s lineárním členem a Onsagerova zákona byly tyto hodnoty přepočítány na termodynamické disociační konstanty a limitní iontové mobility amfolytů. Klíčová slova: kapilární zónová elektroforéza, disociační konstanta, limitní mobilita, amfolyty
|
|
Interactive Debugger for MSIM
Martinec, Tomáš ; Děcký, Martin (vedoucí práce) ; Malohlava, Michal (oponent)
Cílem této práce je rozšíření ladících schopností MSIMu pomocí napojení na vývojové prostředí Eclipse. MSIM je simulátor počítače založený na procesoru MIPS a jednoduchém hardwarovém modelu. Je zaměřen převážně na výuku principů operačních systémů. V současné době MSIM umožňuje ladit emulovaný kód díky implementaci síťového rozhraní GNU Debuggeru (GDB) a pomocí několika interních ladících příkazů. Implementace prezentovaná v této práci spojuje MSIM a ladící prostředí Eclipse IDE pomocí GDB rozhraní. Umožňuje tak uživatelsky přívětivé ladění emulovaného kódu na úrovni zdrojových souborů i assembleru. Dále jsou v práci diskutovány pokročilé ladící techniky jako sledování userspace vláken, konstrukce call tree, zpětné krokování a další.
|
|
Ion-Protein Interactions
Heyda, Jan
Název práce: Interakce iontů s proteiny Autor: Mgr. et Mgr. Jan Heyda Katedra: Fyzikální a makromolekulární chemie Vedoucí doktorské práce: Prof. Pavel Jungwirth, DSc., ÚOCHB AV ČR, v.v.i. E-mail vedoucího: pavel.jungwirth@uochb.cas.cz Abstrakt: V předkládané práci byly použity metody molekulové dynamiky v kom- binaci s pokročilými technikami analýzy k získání detailních informací a pro hlubší pochopení interakcí mezi ionty a proteiny v roztocích. Proto byly zkoumány systémy o různém stupni komplexity, počínaje roztoky molekulárních solí s drobnými frag- menty, podobajícími se funkčním skupinám aminokyselin, jako např. N-methylacetamid reprezentující peptidovou vazbu nebo alkylované amonné kationty. Dále se předmětem našeho studia staly jednotlivé kladně nabité aminokyseliny, u nichž byla popsána silná interakce s malým fluoridovým aniontem, jež je však pro větší halogenidy (Cl− , Br− , I− ) výrazně zeslabena. Toto pozorování bylo prohloubeno objevem vysoké citlivosti fluoridu na rozložení náboje na amonné skupině, bočním řetězci lysinu a N-konci glycinu, zatímco jodid zde vykazoval pouze velice nízkou citlivost. Následně bylo prokázáno, že u krátkých kladně nabitých peptidových úseků v polyargininu a dihistidinu...
|
|
Ion - Protein Interaction
Heyda, Jan ; Jungwirth, Pavel (vedoucí práce) ; Hof, Martin (oponent) ; Ettrich, Rüdiger (oponent)
Název práce: Interakce iontů s proteiny Autor: Mgr. et Mgr. Jan Heyda Katedra: Fyzikální a makromolekulární chemie Vedoucí doktorské práce: Prof. Pavel Jungwirth, DSc., ÚOCHB AV ČR, v.v.i. E-mail vedoucího: pavel.jungwirth@uochb.cas.cz Abstrakt: V předkládané práci byly použity metody molekulové dynamiky v kom- binaci s pokročilými technikami analýzy k získání detailních informací a pro hlubší pochopení interakcí mezi ionty a proteiny v roztocích. Proto byly zkoumány systémy o různém stupni komplexity, počínaje roztoky molekulárních solí s drobnými frag- menty, podobajícími se funkčním skupinám aminokyselin, jako např. N-methylacetamid reprezentující peptidovou vazbu nebo alkylované amonné kationty. Dále se předmětem našeho studia staly jednotlivé kladně nabité aminokyseliny, u nichž byla popsána silná interakce s malým fluoridovým aniontem, jež je však pro větší halogenidy (Cl− , Br− , I− ) výrazně zeslabena. Toto pozorování bylo prohloubeno objevem vysoké citlivosti fluoridu na rozložení náboje na amonné skupině, bočním řetězci lysinu a N-konci glycinu, zatímco jodid zde vykazoval pouze velice nízkou citlivost. Následně bylo prokázáno, že u krátkých kladně nabitých peptidových úseků v polyargininu a dihistidinu...
|
|
Experimentální GUHA procedury
Kuchař, Tomáš ; Mrázová, Iveta (oponent) ; Rauch, Jan (vedoucí práce)
Cílem práce je nová implementace šesti GUHA procedur známých ze systému LISpMiner (4ftMiner, SD4ftMiner, CFMiner, SDCFMiner, KLMiner, SDKLMiner) do prostředí systému Ferda Data Miner s ohledem na jejich další výzkum a vývoj. Základní princip GUHA metody je v generování všech možných relevantních otázek specifikovaných uživatelem, ověření každé z nich oproti datům a reportování pouze prostých tvrzení. Typická efektivní realizace GUHA procedury používá vhodné reprezentace dat pomocí bitových řetězců. Byly vytvořeny prostředky pro řešení výše uvedených GUHA procedur. V průběhu prací došlo k rozšíření možností zadání množiny relevantních otázek.
|
|
MPS-based Domain-specific Language for Defining RTSJ Systems
Fechtner, Tomáš ; Malohlava, Michal (vedoucí práce) ; Pech, Václav (oponent)
Real-time Specification of Java (RTSJ) je rozšíření pro jazyk Java, které umožňuje využít tento jazyk pro tvorbu real-time systémů. Nicméně náročnost použití a složitý programovací model RTSJ s její manuální správou paměti vede často k chybám. Pro ulehčení vývoje RTSJ systému by proto bylo přínosné poskytnout rozšíření jazyka Java pomocí konceptu domain-specific language (DSL). Cílem tohoto DSL by bylo umožnit bezpečnější a intuitivnější vývoj. K tomu je však potřeba najít kompromis mezi všestranností tohoto řešení a jeho použitelností pro uživatele. Tyto požadavky však jdou často proti sobě. Jednou z možností pro vytvoření DSL je použít Meta-Programming System (MPS). Tento systém umožňuje vyvíjet nové doménově specifické jazyky a příslušné projekční editory poskytující rozdílné možnosti jak spravovat kód. Tato práce vytvoří DSL a příslušný generátor kódu umožňující vývoj RTSJ systémů, to vše pomocí MPS platformy. Dále pak provede zhodnocení takto vytvořeného DSL pomocí jednoduché studie. Nakonec tato práce posoudí vhodnost MPS jako platformy pro vytváření DSL.
|
|
The Interaction between Bilateral Investment Treaties and EU Law
Hrabčáková, Barbora ; Balaš, Vladimír (vedoucí práce) ; Šturma, Pavel (oponent)
Vzťah bilaterálnych investičných dohôd a práva EÚ V súčastnosti prebieha v rámci Európskej únie záasdná zmena v oblasti regulácie zahraničných investícií spočívajúca v presune (niektorých) kompetencií v danej obalsti z členských štátov na Európsku úniu, a to ako súčasť širiš iniciatívy s konečným cieľom vytvoriť spoločnú európsku investičnú politiku, ktorá, je arguemntované, môže eventuálne nahradiť systém bilaterálnych ivnestičných dohôd uzavretých medzi členskými a tretími štátmi. Od vstupu Lisabonskej zmluvy v účinnosť je Európska únia výlučne kompetentná regulovať priame zahraničné investície vo vzťahu k tretím štátom a to na základe vloženia pojmu "priamych zahraničných investícií" do znenia čl. 207 odst. 1 Zmluvy o fungovaní Euróspekj únie upravujúceho spoločnú obchodnú politiku, v ktorej, v súlade s čl. 3 odst. 1 písm. e), má Európska únie výlučnú právomoc. Aj keď znenie článku vyzerá na prvý pohľad jasne, existuje niekoľko otázok, predovšetkým vo veci rozsahu novej výlučnej kompetencie Európskej únie, ktoré doposiaľ neboli vyriešené. Po prvé, problematika rozsahu foriem zahraničných investícií, ktoré by mali byť regulované Európskou úniou v rámci novej kompetencie, je nejasná. Boli vznesené argumenty, že výlučná kompetencia sa vzťahuje len na priame zahraničné investície, zatiaľ čo iné formy, v...
|
host ::
