| |
|
Family housing decision-making
Kačírková, Petra ; Brožová, Helena (advisor) ; Adam, Adam (referee)
This thesis is concerned with choosing the best and most real estate mortgage loans for family with children. The family should be chosen property near his residence momentary, then it should be recommended for this property the best mortgage loan. Selecting the property was affected by the demands of all family members and subsequent mortgage loans was selected from the products offered on the Czech market in November 2016. The thesis can be thematically divided into three main parts. The first part includes a literature search, which is divided into two areas. First described methods of multi-criteria decision making, which will be used in the decision making process. Along with these methods includes a literature review and theoretical part of the program area Super Decisions, which will be used in the practical part. Furthermore, theoretically they recognized concepts related to mortgage loans, according to which are then laid down criteria for assessing mortgage loans. The second part contains already a practical perspective on family issues, which therefore includes the selection of the best and most real estate mortgage loan program with the help of Super Decisions. The third part includes a summary of the work and the interpretation of results obtained through the program Super Decisions.
|
|
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.
|
|
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.
|
|
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.
|
|
Work in social integration process of adults with intellectual disability.
SVITÁKOVÁ, Iveta
In my bachelor thesis, I dealt with the use of work activities in the process of social integration of adults with mental disabilities, the aim was to create, implement and evaluate regular work activities intended to a specific group of adults with mental disability and focused primarily on the development of social integration. The thesis is structured into six chapters. The first of them is focused on the definition of mental disability, characteristic of adulthood as an important developmental period in human life, and on adulthood of individuals with mental disabilities with a goal to find and identify the specifics that were needed to be taken into account when working with this target group of people. The following section is devoted to the social integration, its determinants and the environment in which it operates. I continued with the outputs in the third chapter, where I focused on key competencies, which them are the necessary basis for social integration, especially social and personal skills and communication skills, necessary basis. Targeted professional development can be realized through educational activities, but has to respect the specificities of the participants and voluntary participation. Both of these assumptions can be fulfilled within the leisure education using adequate pedagogical methods. For this reason, I decided to focus my attention on these areas at the end of the chapter. The fourth chapter is devoted to work and work activities, namely the definition of concepts, their characteristics and importance and role of work activities in human life, or a person with mental disability. Based on all acquired theoretical knowledge and using previous experience with the target group in the fifth chapter, I designed a specific training program based on the work and activities focused on the development of selected key competences. The educational program volunteered four participants, but I have decided to follow the development of competencies of three participants because one participant attended the program very irregularly. The program has been implemented three times a week, two and a half hours for seven months (from October 2015 to May 2016) in the premises of the training centre Mo-zai-ka. At the beginning of the realisation of the created educational program, the participants agreed that we will adhere and develop good habits necessary for good relations within the group and the results of the work. On a basis of the individual characteristics of the participants, I prepared the work, which should also contribute to the development of social and personal and interpersonal skills. I have continuously monitored and recorded them. During the implementation of the program, I put emphasis on repetition, patient negotiations with participants and creating a friendly atmosphere. After completing the training program, I evaluated the development of competencies in three selected participants. On that basis, I concluded that the biggest change was in the communicative competence. I also experienced a change in social and personal competencies, however, results varied widely among individual participants. Yet, I believe that the goal of the thesis was achieved. These results show that education in leisure time, based on work activities may lead to the development of social and personal and interpersonal skills that are for adults with mental disabilities necessary in the process of social integration. This thesis can be an interesting source of inspiration for the realisation of similar programs aimed at social integration of persons with mental disabilities.
|
|
The use of new technologies in teaching mathematics
BUMBÁLEK, Roman
Modern information technologies accompany all of us in our daily life. They not only use to serve to our work and for the entertainment, they even have got a great potential to be used in the education. The submitted thesis deals with the appropriate utilization of the special IT application in the pedagogic process, especially in teaching of maths, the topic of trigonometric functions. The aim of this thesis is to create structures with a high potential of the modern technology handling. To tackle this task the graphical program GeoGebra was chosen due to its qualities for creating dynamic structures and the other advantages presented further in the thesis. To the created constructions the detailed instructions how they can be constructed are added. The thesis is also accompanied by worksheets with solved tasks, focusing on the application of trigonometric functions in real situations.
|
|
Computer aided verification and proving geometric theorems
CUKR, Pavel
The aim of this diploma thesis Computer aided verification and proving of geometric theorems is verification and proving of selected geometric theorems and statements using dynamic geometry software (GeoGebra) and computer algebra programs (CoCoA). Each problem is first demonstrated and verified in the GeoGebra program. Then classical proof and computer aided proof, or determination of the equation of a curve, using the program CoCoA follow. The use of dynamic geometry software and computer algebra programs is suitable as a teaching tool in maths lessons at primary and secondary schools.
|
guest ::
