|
Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (oponent) ; Sekanina, Lukáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
The thesis starts by providing a taxonomy of concurrency-related errors and an overview of their dynamic detection. Then, concurrency coverage metrics which measure how well the synchronisation and concurrency-related behaviour of tested programs has been examined are proposed together with a~methodology for deriving such metrics. The proposed metrics are especially suitable for saturation-based and search-based testing. Next, a novel coverage-based noise injection techniques that maximise the number of interleavings witnessed during testing are proposed. A comparison of various existing noise injection heuristics and the newly proposed heuristics on a set of benchmarks is provided, showing that the proposed techniques win over the existing ones in some cases. Finally, a novel use of stochastic optimisation algorithms in the area of concurrency testing is proposed in the form of their application for finding suitable combinations of values of the many parameters of tests and the noise injection techniques. The approach has been implemented in a prototype way and tested on a set of benchmark programs, showing its potential to significantly improve the testing process.
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which nonterminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs.
|
|
Evolutionary Approach to Synthesis and Optimization of Ordinary and Polymorphic Circuits
Gajda, Zbyšek ; Schmidt, Jan (oponent) ; Zelinka,, Ivan (oponent) ; Sekanina, Lukáš (vedoucí práce)
This thesis deals with the evolutionary design and optimization of ordinary and polymorphic circuits. New extensions of Cartesian Genetic Programming (CGP) that allow reducing of the computational time and obtaining more compact circuits are proposed and evaluated. Second part of the thesis is focused on new methods for synthesis of polymorphic circuits. Proposed methods, based on polymorphic binary decision diagrams and polymorphic multiplexing, extend the ordinary circuit representations with the aim of including polymorphic gates. In order to reduce the number of gates in circuits synthesized using proposed methods, an evolutionary optimization based on CGP is implemented and evaluated. The implementations of polymorphic circuits optimized by CGP represent the best known solutions if the number of gates is considered as the target criterion.
|
|
Využití pracovních činností v procesu sociální integrace dospělých s mentálním postižením.
SVITÁKOVÁ, Iveta
V rámci své bakalářské práce jsem se věnovala využití pracovních činností v procesu sociální integrace dospělých s mentálním postižením, přičemž cílem bylo vytvořit, zrealizovat a vyhodnotit pravidelnou pracovní činnost určenou specifické skupině dospělých s mentálním postižením a zaměřenou primárně na rozvoj sociální integrace. Text práce je strukturován do šesti kapitol. V první z nich jsem se zaměřila na vymezení mentálního postižení, charakteristiku dospělosti jako důležitého vývojového období v životě člověka a na dospělost jedinců s mentálním postižením s cílem nalézt a pojmenovat specifika, která byla třeba při práci s touto cílovou skupinou zohlednit. V následující části jsem se věnovala sociální integraci, jejím determinantům a prostředí, ve kterém se uskutečňuje. Na získané výstupy jsem navázala ve třetí kapitole, v níž jsem se zaměřila na klíčové kompetence, z nichž jsou pro sociální integraci nezbytným podkladem zejména sociální, personální a komunikativní kompetence. Cílený rozvoj těchto kompetencí lze realizovat prostřednictvím edukační činnosti, která však musí respektovat specifika účastníků a dobrovolnost účasti. Oba tyto předpoklady lze naplňovat v rámci zájmového vzdělávání s využitím adekvátních pedagogických metod. Na tyto oblasti jsem proto zacílila svou pozornost v závěru kapitoly. Kapitola čtvrtá je věnována práci a pracovním činnostem, konkrétně vymezení pojmů, jejich charakteristice, významu a roli pracovních činností v životě člověka, respektive člověka s mentálním postižením. Na základě všech získaných teoretických poznatků a s využitím dosavadních zkušeností s cílovou skupinou jsem v páté kapitole navrhnula specifický vzdělávací program založený na pracovních činnostech a zaměřený na rozvoj vybraných klíčových kompetencí. Do vzdělávacího programu se dobrovolně přihlásili čtyři účastníci, přičemž jsem se rozhodla sledovat rozvoj kompetencí jen tří účastníků z důvodu, že jeden účastník docházel velmi nepravidelně. Program byl realizován třikrát týdně, vždy 2,5 hodiny po dobu sedmi měsíců (od října 2015 do května 2016) v prostorách vzdělávacího centra Mo-zai-ka. Na počátku realizace vytvořeného vzdělávacího programu účastníci souhlasili s tím, že budeme dodržovat a rozvíjet správné návyky potřebné pro dobré vzájemné vztahy ve skupině a výsledky pracovní činnosti. Na základě individuálních charakteristik účastníků jsem připravovala pracovní činnosti, které měly přispět také k rozvoji sociálních a personálních a komunikativních kompetencí. Ty jsem průběžně sledovala a zaznamenávala. Během realizace programu jsem kladla důraz na opakování, trpělivé jednání s účastníky a vytvoření přátelské atmosféry. Po ukončení vzdělávacího programu jsem rozvoj kompetencí u tří vybraných účastníků vyhodnotila. Na základě toho jsem dospěla k závěru, že k největší změně došlo v komunikativních kompetencích. Posun jsem zaznamenala i v sociálních a personálních kompetencích, zde se však výsledky u jednotlivých účastníků značně lišily. Přesto se domnívám, že cíl práce byl splněn. Uvedené výsledky ukazují, že vzdělávání ve volném čase založené na pracovních činnostech může vést k rozvoji sociálních, personálních a komunikativních kompetencí, které jsou pro dospělé s mentálním postižením nezbytné v procesu sociální integrace. Tato bakalářská práce může být zajímavým zdrojem inspirace pro realizaci obdobných programů zacílených na sociální integraci osob s mentálním postižením.
|
|
Reflexe díla Františka Bakuleho ve vztahu k dnešní speciálně pedagogické praxi
BALÍKOVÁ, Tereza
František Bakule byl významným českým pedagogem první poloviny 20. století, prvním ředitelem Jedličkova ústavu v Praze, zakladatelem tzv. Bakulova ústavu a jedním z mála českých představitelů alternativního pojetí výchovy a vzdělávání uznávaných v zahraničí. Jeho odkaz však v současné době není naší odbornou veřejností v rámci hlavního vzdělávacího proudu ani speciálních škol dále systematicky rozvíjen a prakticky uplatňován, na rozdíl od řady zahraničních alternativních pedagogických směrů, které jsou zde úspěšně aplikovány. Cílem této bakalářské práce je proto analyzovat dílo Františka Bakuleho prizmatem současného školního edukačního prostředí s důrazem na vzdělávání žáků se zdravotním postižením. První kapitola je věnována nástinu životní cesty Františka Bakuleho, zejména se zaměřením na významné mezníky, které ovlivnily utváření jeho osobnosti, jeho myšlenky, inspiraci a motivaci a které se projevily v jeho pedagogické činnosti a následně v jeho vlastním uceleném konceptu výchovy a vzdělávání. Konkrétně je zde zmíněno jeho rodinné zázemí a dále je prostor věnován zejména jeho učitelským zkušenostem až po působení v Jedličkově ústavu a etapu života spojenou s jeho vlastním ústavem. Druhá část bakalářské práce je již zaměřena výhradně na Bakuleho specifický edukační koncept. Nejprve jsou zde vymezeny jeho principy a následně uvedeny originální učební osnovy a návrh ideálního prostředí třídy. Text dále obsahuje detailní popis výuky několika předmětů, které byly těžištěm Bakuleho konceptu, a to jmenovitě pracovních činností, hudební výchovy a výtvarné výchovy. Původní didaktické postupy jsou analyzovány s využitím současné terminologie. Vzhledem k vymezenému cíli bylo třeba ve třetí kapitole analyzovat současné pojetí vzdělávání ve výše zmíněných, podle Bakuleho stěžejních oblastech. Text je koncipován tak, aby bylo možné následně reflektovat dílo Františka Bakuleho z pohledu dnešní pedagogické, respektive speciálně pedagogické praxe, nalézt styčné body či odlišnosti a odhalit nevyužitý inspirační potenciál. Tomu je pak věnována čtvrtá, závěrečná kapitola. Na základě analýzy a následné reflexe bylo ve výsledku konstatováno, že ačkoli se Bakulem formulované vzdělávací cíle významně neodlišují od současného pojetí zakotveného v příslušných rámcových vzdělávacích programech, k jejich dosažení se v současné době užívá odlišných postupů a metod. A to přestože sám Bakule své postupy, které lze velmi zjednodušeně charakterizovat mottem "neučit žáky o životě a práci, ale životem a prací", s úspěchem ověřil v praxi a že mu v řadě případů daly za pravdu pozdější výsledky psychologických výzkumů, čímž poskytly jeho didaktickému odkazu teoretickou oporu. Z výše uvedeného je zřejmé, že odkaz díla Františka Bakuleho nebyl naší odbornou pedagogickou veřejností dostatečně doceněn a vytěžen. Na druhou stranu je třeba konstatovat, že jeho širšímu uplatnění stojí v cestě roztříštěnost, v níž se nám dochoval.
|
|
Užití nových technologií při výuce matematiky na základních a středních školách
BUMBÁLEK, Roman
S moderními informačními technologiemi se setkáváme každý den. Slouží k pomoci v práci, k zábavě, ale mají také velký potenciál pro využití ve vzdělávání. Tato práce se zabývá jejich vhodnou aplikací do výuky matematiky, na tematiku goniometrických funkcí. Cílem je vytvořit konstrukce, které by potenciál moderních technologií co nejlépe využily. Pro řešení problematiky byl vybrán program GeoGebra pro možnost tvorby dynamických konstrukcí a pro další nesporné výhody, zmíněné dále v práci. K vytvořeným konstrukcím jsou přidány podrobné návody, jak je lze sestrojit. Práce je také doplněna řešenými úlohami a pracovními listy, zaměřenými na aplikaci goniometrických funkcí do reálných situací.
|
|
Verifikace a dokazování geometrických vět s podporou počítače
CUKR, Pavel
Cílem diplomové práce Verifikace a dokazování geometrických vět s podporou počítače je ověření a dokazování vybraných geometrických vět a tvrzení pomocí programů GeoGebra a CoCoA. Každý problém je nejprve demonstrován v programu GeoGebra, poté následuje ověření (verifikace) problému v tomtéž programu. Dále je uveden klasickýdůkaz a důkaz, případně určení rovnice křivky, pomocí matematického programu CoCoA. Využití programu dynamické geometrie současně s programem počítačové algebry je vhodné jako učební pomůcka v hodinách matematiky na základních a středních školách.
|
|
Přínos akceleračního programu klisen českého teplokrevníka pro sport a chov
Kupčíková, Magdalena ; Janošíková, Martina (vedoucí práce)
V následujících řádcích mé práce zjišťuji, zda jsou klisny zařazené do akceleračního programu dále využívány v chovu a zda AP přispívá či je jistotou pro zvyšující se počty hříbat ČT a jestli jsou výsledky hodnocení klisen ve 3 letech ukazatelem kvality a úspěchu klisen samotných i jejich hříbat v další sportovní kariéře. Dále se pokusím posoudit, zda jsou dotace získané zařazením klisny do AP využívány v plné míře, což se odvíjí od počtu porozených hříbat.
|
|
Výskyt látek skupiny PBDE a Bisfenol A ve vodních tocích s výskytem raků
Svobodová, Kateřina ; Vach, Marek (vedoucí práce)
Práce se zabývá vyhodnocením výsledků projektu pod záštitou EAA and Norway grants, který probíhal v letech 2015 až 2016. Projekt se zabýval jakostí vody na lokalitách s původními a invazními raky. Součástí projektu bylo i sledování organických látek např. polybromovaných difenyletherů (PBDE). Věnovat se budu zejména látkám skupiny PBDE tedy polybromovaným difenyletherům, které patří mezi bromované zpomalovače hoření (BFR). Tyto látky, jsou sledovány od 70. let 20. století, kdy v USA došlo k náhodné kontaminaci potravy a následnému zamoření blízké oblasti. Alarmující je jejich perzistence v prostředí, díky které se neustále zvyšují hladiny v přírodní matrici. Informace o transformaci a biodegradaci PBDE v prostředí jsou stále omezené a neustále probíhají nejrůznější studie. Jsou to látky málo těkavé a i nerozpustné, proto hlavním zdrojem jejich úniků je prach a částice vznikající z výrobků, ve kterých jsou tyto látky obsaženy. Další látkou, jejímž výskytem v životním prostředí České republiky bych se ráda zabývala, je Bisfenol A (BPA). Toxická látka využívaná při výrobě epoxidových pryskyřic a polykarbonátových plastů. BPA je toxická látka se schopností narušovat funkci hormonů. Obsah těchto látek byl potvrzen i v kojeneckých lahvích. V dubnu 2004 byl vládou ČR schválen (program na snížení znečištění povrchových vod nebezpečnými závadnými látkami). Od srpna roku 2004 platí v EU zákaz prodeje a používaní penta-BDE a okta-BDE ve všech oborech. Bisfenol A se od roku 2011 nesmí používat při výrobě kojeneckých lahví. Cílem práce je analyzovat a následně vyhodnotit množství a možné důsledky obsahu těchto látek v našem životním prostředí, které jsou alarmující i po úplném či částečném zákazu užívání těchto látek.
|
|
Management produkčních populací lesních dřevin s využitím metod matematického programování
Hořejší, Matouš ; Lstibůrek, Milan (vedoucí práce) ; Stejskal, Jan (oponent)
Šlechtění lesních dřevin představuje obrovskou příležitost pro lesní hospodářství, jak uspět v současném moderním světě. Vyšlechtěné lesní dřeviny mají lepší růstové vlastnosti a projevuje se u nich vyšší odolnost vůči stresu a nepříznivým podmínkám, které budou pravděpodobně v budoucnu narůstat.
Pro zakládání semenných sadů je nezbytné vytvořit kvalitní a spolehlivý algoritmus, podle kterého bude probíhat selekce klonů. Model vytvořený v této práci na bázi matematického programování optimalizuje směs klonů s nejvyšší možnou šlechtitelskou hodnotou a zároveň zabraňuje nárůstu příbuznosti, která by vedla k nežádoucímu poklesu genové diverzity.
|
host ::
