|
Porting of Prawn Library from Ruby to Python 3
Molhanec, Michal ; Pícka, Marek (advisor) ; Mikoláš, Mikoláš (referee)
This work focuses on automatic translation of code written in Ruby programming language into Python 3. First part investigates principles of computer programming languages translation as is described in the literature. Second part compares elements of these two programming languages and suggests ways how these elements can be translated.
Based on this theory I developed Ruby-to-Python translator. Its working is demonstrated on the translation of the Prawn library for generating PDF files.
|
|
Cooperation of high schools with external contractors in preparing school educational programs
Tulach, David ; Lačev, Alek (advisor) ; Hochel, Matej (referee)
This thesis, Cooperation of high schools with external contractors in preparing school educational programs, deals with the question whether it would be possible and beneficial for high schools to cooperate with companies on the preparation or modification of their educational programs, with the goal of improving the quality of education. After initial contributions from experts who provided negative replies to this question, the view was focused on the root of the issue - what are the historical pillars of public schools and pedagogy, what does science say about learning and teaching, how pedagogy reacts to the crisis of science. After comparing literal sources and results from interview with the experts, in combination with a trace and activity analysis, a theory was established that public education is reaching a point of crisis, has not changed in its essence since its beginning and that the best solution might be the establishment of alternative educational institutions.
|
|
Current environmental threats and their impact in the landscape
Zapletalová, Jana ; Kirchner, Karel
Workshop Current environmental threats and their impact on the landscape was organized in the framework of the Strategy AV21 of the Academy of Sciences, the program Natural threats.\nThe papers were oriented both on natural threats (geological and geomorphological threats - slope deformation, erosion, hydrometeorological extremes floods, droughs, biological invasions) and their evaluation and prediction, and social and legal implications of natural and human activities caused by threats and their impacts on the landscape (e. g. changes in the urban environment, anthropogenic impacts in the mining areas). Important topics were focused on the assessment of natural and environmental threats and their solving in selected emergency and crisis situations using geoinformation technologies. \n
Fulltext: content.csg -  PDF
Plný tet: UGN_0465323 - PDF
|
|
Energy assessment of building
Žůrek, Petr ; Horák, Petr (referee) ; Hirš, Jiří (advisor)
Diplomová práce se zabývá energetickým sektorem v Ruské Federaci se zaměřením na sektor budov a jejich energetickou efektivnost. Je zde vytvořen základní přehled předpi-sů a norem týkajících se sektoru budov a dotační programy vytvořené Ruskou vládou na snížení energetické náročnosti. V praktické části je provedeno energetické hodnocení dané budovy v podmínkách Čr a Ruské Federace. Výpočty energetických bilancí budovy jsou prováděny pro klimatické podmínky daných zemí a v souladu s národními předpisy. Na základě energetických bilancí jsou navrženy opatření na úsporu energie. V závěru je provedeno ekonomické posouzení, s ohledem na rozdílné ceny energií a nákladů na provedení návrhových opat-ření v České republice a Ruské Federaci.
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
Retargetable Analysis of Machine Code
Křoustek, Jakub ; Janoušek, Jan (referee) ; Návrat,, Pavol (referee) ; Kolář, Dušan (advisor)
Analýza softwaru je metodologie, jejímž účelem je analyzovat chování daného programu. Jednotlivé metody této analýzy je možné využít i v dalších oborech, jako je zpětné inženýrství, migrace kódu apod. V této práci se zaměříme na analýzu strojového kódu, na zjištění nedostatků existujících metod a na návrh metod nových, které umožní rychlou a přesnou rekonfigurovatelnou analýzu kódu (tj. budou nezávislé na konkrétní cílové platformě). Zkoumány budou dva typy analýz - dynamická (tj. analýza za běhu aplikace) a statická (tj. analýza aplikace bez jejího spuštění). Přínos této práce v rámci dynamické analýzy je realizován jako rekonfigurovatelný ladicí nástroj a dále jako dva typy tzv. rekonfigurovatelného translátovaného simulátoru. Přínos v rámci statické analýzy spočívá v navržení a implementování rekonfigurovatelného zpětného překladače, který slouží pro transformaci strojového kódu zpět do vysokoúrovňové reprezentace. Všechny tyto nástroje jsou založeny na nových metodách navržených autorem této práce. Na základě experimentálních výsledků a ohlasů od uživatelů je možné usuzovat, že tyto nástroje jsou plně srovnatelné s existujícími (komerčními) nástroji a nezřídka dosahují i lepších výsledků.
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (referee) ; Sekanina, Lukáš (referee) ; Vojnar, Tomáš (advisor)
V disertační práci je nejprve uvedena taxonomie chyb v souběžném zpracování dat a přehled technik pro jejich dynamickou detekci. Následně jsou navrženy nové metriky pro měření synchronizace a souběžného chování programů společně s metodologií jejich odvozování. Tyto techniky se zejména uplatní v testování využívajícím techniky prohledávání prostoru a v saturačním testování. Práce dále představuje novou heuristiku vkládání šumu, jejímž cílem je maximalizace proložení instrukcí pozorovaných během testování. Tato heuristika je porovnána s již existujícími heuristikami na několika testech. Výsledky ukazují, že nová heuristika překonává ty existující v určitých případech. Nakonec práce představuje inovativní aplikaci stochastických optimalizačních algoritmů v procesu testování vícevláknových aplikací. Principem metody je hledání vhodných kombinací parametrů testů a metod vkládání šumu. Tato metoda byla prototypově implementována a otestována na množině testovacích příkladů. Výsledky ukazují, že metoda má potenciál vyznamně vylepšit testování vícevláknových programů.
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.
|
|
Evolutionary Approach to Synthesis and Optimization of Ordinary and Polymorphic Circuits
Gajda, Zbyšek ; Schmidt, Jan (referee) ; Zelinka,, Ivan (referee) ; Sekanina, Lukáš (advisor)
Tato disertační práce se zabývá evolučním návrhem a optimalizací jak běžných, tak polymorfních digitálních obvodů. V práci jsou uvedena a vyhodnocena nová rozšíření kartézského genetického programování (Cartesian Genetic Programming, CGP), která umožňují zkrácení výpočetního času a získávání kompaktnějších obvodů. Další část práce se zaměřuje na nové metody syntézy polymorfních obvodů. Uvedené metody založené na polymorfních binárních rozhodovacích diagramech a polymorfním multiplexovaní rozšiřují běžné reprezentace digitálních obvodů, a to s ohledem na začlenění polymorfních hradel. Z důvodu snížení počtu hradel v obvodech syntetizovaných uvedenými metodami je provedena evoluční optimalizace založená na CGP. Implementované polymorfní obvody, které jsou optimalizovány s využitím CGP, reprezentují nejlepší známá řešení, jestliže je jako cílové kritérium brán počet hradel obvodu.
|
guest ::
