| |
|
Požadavky podniků na profil absolventa – softwarového vývojáře
Trnková, Michaela ; Pecinovský, Rudolf (vedoucí práce) ; Pavlíčková, Jarmila (oponent)
Předmětem bakalářské práce je zmapování požadavků, které jsou kladeny na absolventy - softwarové vývojáře. Cíle je dosaženo pomocí rozhovorů s odborníky z praxe. Důležitou částí práce je zhodnocení různých metodik výuky programování s blížším zaměřením na metodiku. Přístupy jsou zhodnoceny z pohledu zástupců podniků, učitelů programování a obdobných předmětů na vysokých školách i studentů informatických oborů. Hlavním přínosem práce je souhrn doporučení pro školy pro výuku studentů, která vyplývají z názorů vývojářů a vedoucích vývojářských týmů z technologických firem a názorů studentů, kteří předměty programování absolvovali. Práce obsahuje i doporučení pro studenty, kteří se chtějí v budoucnu zabývat vývojem softwaru.
|
|
Spolupráce středních škol s externími firmami v přípravě školních vzdělávacích programů
Tulach, David ; Lačev, Alek (vedoucí práce) ; Hochel, Matej (oponent)
Tato práce, Spolupráce středních škol s externími firmami v přípravě školních vzdělávacích programů, se zabývá otázkou, zdali je možné a přínosné, aby střední školy spolupracovaly s firmami na přípravě či úpravě svých vzdělávacích programů za cílem zlepšení kvality vzdělávání. Po prvotních příspěvcích ze strany odborníků, které na tuto otázku odpovídaly negativně, byl pohled zaměřen na kořen věci - na čem stojí historické pilíře školství a pedagogiky, co o učení se a výuce říká věda, jak pedagogika reaguje na krizi věd. Při porovnání literárních zdrojů a závěrů z rozhovorů s odborníky v kombinaci s analýzou stop a výsledků činnosti odborníků dalších byla stanovena teorie, že veřejné školství dospívá do bodu krize, ve své podstatě se od svého vzniku nezměnilo a nejlepším řešením může být vytvoření alternativních vzdělávacích institucí.
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
Retargetable Analysis of Machine Code
Křoustek, Jakub ; Janoušek, Jan (oponent) ; Návrat,, Pavol (oponent) ; Kolář, Dušan (vedoucí práce)
Program analysis is a computer-science methodology whose task is to analyse the behavior of a given program. The methods of program analysis can also be used in other methodologies such as reverse engineering, re-engineering, code migration, etc. In this thesis, we focus on program analysis of a machine-code and we address the limitations of a nowadays approaches by proposing novel methods of a fast and accurate retargetable analysis (i.e. they are designed to be independent of a particular target platform). We focus on two types of analysis - dynamic analysis (i.e. run-time analysis) and static analysis (i.e. analysing application without its execution). The contribution of this thesis within the dynamic analysis lays in the extension and enhancement of existing methods and their implementation as a retargetable debugger and two types of a retargetable translated simulator. Within the static analysis, we present a concept and implementation of a retargetable decompiler that performs a program transformation from a machine code into a human-readable form of representation. All of these tools are based on several novel methods defined by the author. According to our experimental results and users feed-back, all of the proposed tools are at least fully competitive to existing solutions, while outperforming these solutions in several ways.
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating
|
|
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.
|
|
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.
|
| |
|
Nadváha a obezita adolescentů
JINDROVÁ, Kateřina
Tato bakalářská práce se zabývá problematikou nadváhy a obezity adolescentů. Problematika u dospívajících je podrobně popsána a následně rozdělena. Hlavním stanoveným cílem mé bakalářské práce bylo zmapovat problematiku nadváhy a obezity v období dospívání v rozmezí 15 - 18 let a to především jejich stravovací zvyklosti a pohybovou aktivitu. Teoretická část se zaměřuje na výskyt nadváhy a obezity v České Republice a ve světě, příčiny vzniku, rizikové faktory, klasifikaci a diagnostiku, typy, léčbu a prevenci. Zabývá se zde racionální stravou, popisuji zásady správného stravování a vhodné či nevhodné potraviny. Snažím se klást důraz na prevenci nadváhy a obezity a to především na stravování a pohybovou aktivitu. Metodická část byla zpracována pomocí kvantitativního výzkumu. Technikou sběru dat jsou dotazníky určené pro dospívající středních škol v rozmezí 1. - 3. ročník. Výzkumný soubor bude zahrnovat 150 respondentů z různých škol v Českých Budějovicích a okolí. Výsledky budou zaznamenány v podobě grafů, které budou okomentovány a doplněny tabulkami. V souladu s cílem a použitím kvantitativního výzkumu byly stanoveny hypotéza. Hypotéza 1 zněla: Nadváha a obezita se bude vyskytovat více u dospívajících se špatnými stravovacími návyky. Hypotéze 2 zněla: Nadváha a obezita se bude vyskytovat více u dospívajících s nízkou pohybovou aktivitou. Pro vypracování výzkumné části byl použit kvantitativní výzkum, který byl prováděn formou dotazníků, které byly rozdány studentům v období dospívání v rozmezí 15 - 18 let. Získaná data jsem zpracovala pomocí programu "Microsoft Excel", ve kterém jsem používala jednotlivé početní relace a funkce. Odpovědi od jednotlivých respondentů jsem zaznamenávala do databáze a za pomoci daných funkcí v Excelu jsem vyhodnocovala jednotlivé určené kategorie. Nejvíce jsem se zaměřila na kategorie týkající se pohybu a stravování. Zpracovaná data jsou interpretována jednoduchými grafy, které jsou vždy okomentovány, popřípadě doplněny tabulkami a následně statisticky zhodnoceny. Z výsledku vyplývají 2 hlavní rozdíly mezi dospívajícími s normální váhou a trpícími nadváhou a obezitou. Jedním z nich je nepravidelnost ve stravování a celkově špatné stravovací zvyklosti, velký rozdíl se též objevuje u pohybové aktivity. U obézních adolescentů se často objevuje nerovnoměrný a nepravidelný příjem potravy, nadměrný příjem kalorických nápojů typu coca cola, fanta, sprite apod., nedostatečný příjem ovoce, zeleniny, luštěnin, ryb, či žádná nebo velmi nízká pohybová aktivita. Pouze několik obézních dospívajících se od těchto kritérií odlišuje, ti však toto onemocnění mají dané geneticky. U zkoumaných respondentů s normální váhou je stravování pravidelné, vyskytují se však výjimky, které se stravují obdobně jako obézní, avšak společnou vlastností, všech dětí s normální váhou, je pravidelná fyzická aktivita. Hypotéza 1 i hypotéza 2 byly potvrzeny. Výsledky ukazují, že na vzniku obezity se podílejí velmi často genetické faktory, které lze aspoň z části pozitivně ovlivnit pravidelnou pohybovou aktivitou a vhodnými stravovacími návyky. Závěrem práce bych chtěla říci, že je nepostradatelné zaměřit se na vhodné stravovací návyky a pravidelnou pohybovou aktivity již od útlého věku, kdy si dítě osvojuje většinu návyků a zvyklostí a to včetně rodičů, kteří jsou mnohdy vzorem pro své děti. Je důležité rozvíjet znalosti o jednotlivých formách prevence, které jsou mnohdy zásadní v zabránění vzniku nadváhy a obezity.
|
host ::
