|
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.
|
|
Acceleration Methods for Evolutionary Design of Digital Circuits
Vašíček, Zdeněk ; Miller, Julian (referee) ; Zelinka,, Ivan (referee) ; Sekanina, Lukáš (advisor)
Ačkoliv můžeme v literatuře nalézt řadu příkladů prezentujících evoluční návrh jakožto zajímavou a slibnou alternativu k tradičním návrhovým technikám používaným v oblasti číslicových obvodů, praktické nasazení je často problematické zejména v důsledku tzv. problému škálovatelnosti, který se projevuje např. tak, že evoluční algoritmus je schopen poskytovat uspokojivé výsledky pouze pro malé instance řešeného problému. Vážný problém představuje tzv. problém škálovatelnosti evaluace fitness funkce, který je markantní zejména v oblasti syntézy kombinačních obvodů, kde doba potřebná pro ohodnocení kandidátního řešení typicky roste exponenciálně se zvyšujícím se počtem primárních vstupů. Tato disertační práce se zabývá návrhem několika metod umožňujících redukovat problem škálovatelnosti evaluace v oblasti evolučního návrhu a optimalizace číslicových systémů. Cílem je pomocí několika případových studií ukázat, že s využitím vhodných akceleračních technik jsou evoluční techniky schopny automaticky navrhovat inovativní/kompetitivní řešení praktických problémů. Aby bylo možné redukovat problém škálovatelnosti v oblasti evolučního návrhu číslicových filtrů, byl navržen doménově specifický akcelerátor na bázi FPGA. Tato problematika reprezentuje případ, kdy je nutné ohodnotit velké množství trénovacích dat a současně provést mnoho generací. Pomocí navrženého akcelerátoru se podařilo objevit efektivní implementace různých nelineárních obrazových filtrů. S využitím evolučně navržených filtrů byl vytvořen robustní nelineární filtr implusního šumu, který je chráněn užitným vzorem. Navržený filtr vykazuje v porovnání s konvenčními řešeními vysokou kvalitu filtrace a nízkou implementační cenu. Spojením evolučního návrhu a technik známých z oblasti formální verifikace se podařilo vytvořit systém umožňující výrazně redukovat problém škálovatelnosti evoluční syntézy kombinačních obvodů na úrovni hradel. Navržená metoda dovoluje produkovat komplexní a přesto kvalitní řešení, která jsou schopna konkurovat komerčním nástrojům pro logickou syntézu. Navržený algoritmus byl experimentálně ověřen na sadě několika benchmarkových obvodů včetně tzv. obtížně syntetizovatelných obvodů, kde dosahoval v průměru o 25% lepších výsledků než dostupné akademické i komerční nástroje. Poslední doménou, kterou se práce zabývá, je akcelerace evolučního návrhu lineárních systémů. Na příkladu evolučního návrhu násobiček s vícenásobnými konstantními koeficienty bylo ukázáno, že čas potřebný k evaluaci kandidátního řešení lze výrazně redukovat (defacto na ohodocení jediného testovacího vektoru), je-li brán v potaz charakter řešeného problému (v tomto případě linearita).
|
|
The impact of reconversion on the value of a former church building in South Moravia
Sýkorová, Michaela ; Gardášová, Alena (referee) ; Hlavinková, Vítězslava (advisor)
The diploma thesis deals with specific case of valuation of the former vicarage in the village Přítluky in South Moravia. The basic idea is to evaluate the imact of change in the purpose of use associated with building reconstruction, from view of market approach and also valid valuation laws. First part deals with theoretical basis as valuation terms, laws and approaches. Next chapter describes specific situation of the site and the building and in the last part is described and justified own valuation methods. Results are analyzed at the end.
|
|
Methods for class prediction with high-dimensional gene expression data
Šilhavá, Jana ; Matula, Petr (referee) ; Železný, Filip (referee) ; Smrž, Pavel (advisor)
Dizertační práce se zabývá predikcí vysokodimenzionálních dat genových expresí. Množství dostupných genomických dat významně vzrostlo v průběhu posledního desetiletí. Kombinování dat genových expresí s dalšími daty nachází uplatnění v mnoha oblastech. Například v klinickém řízení rakoviny (clinical cancer management) může přispět k přesnějšímu určení prognózy nemocí. Hlavní část této dizertační práce je zaměřena na kombinování dat genových expresí a klinických dat. Používáme logistické regresní modely vytvořené prostřednictvím různých regularizačních technik. Generalizované lineární modely umožňují kombinování modelů s různou strukturou dat. V dizertační práci je ukázáno, že kombinování modelu dat genových expresí a klinických dat může vést ke zpřesnění výsledku predikce oproti vytvoření modelu pouze z dat genových expresí nebo klinických dat. Navrhované postupy přitom nejsou výpočetně náročné. Testování je provedeno nejprve se simulovanými datovými sadami v různých nastaveních a následně s~reálnými srovnávacími daty. Také se zde zabýváme určením přídavné hodnoty microarray dat. Dizertační práce obsahuje porovnání příznaků vybraných pomocí klasifikátoru genových expresí na pěti různých sadách dat týkajících se rakoviny prsu. Navrhujeme také postup výběru příznaků, který kombinuje data genových expresí a znalosti z genových ontologií.
|
|
Organization and management of production in selected enterprise
DRNOVÁ, Markéta
The topic of my dissertation is "Organization and management of production in selected enterprise". The main goal of this dissertation is mapping of selected enterprise in one year period and obtain sufficient amount of information for future analysis and suggest possible improvements. The identification data, characteristic, products and services and production planning of selected enterprise are provided in introduction of practical part of this dissertation. Analysis of present state with mapping of present state for individually semi-finished products is introduced in the next part of dissertation. For analysis of present state was calculated VA index and for each semi-finished product was created diagram of material movement in next chapter. The goal of analyses and diagram is the finding of narrow spaces in the material flow. The target map of future state was created in the next part. This map is based on present map. The future map presents critical factors that need to be improved. Finally it defines a new VA index, which should be approach to the current state. The penultimate section includes recommendations methods and elements of lean production to the new production hall which the company wants to build. Among the recommended methods are mainly the 5S method, visualization, standardization, SMED and Bottleneck. The last chapter contains a number of measures. For example employee motivation, continuous improvement, personal responsibility, introduction of EDI and ergonomics which would lead to the improvement of the business this enterprise.
|
|
Differentiation of offers and methods of working physiotherapy of persons with a mental or combined handicap in a practice of social service providers and another subjects.
POŠMUROVÁ, Nikola
In the Bachelor's thesis I have dealt with differentiation of tenders and rehabilitation methods. Specifically, individuals with mental or multiple disabilities and for providers of social services and other bodies. In the theoretical part I focused on defining the basic terms relating to that issue. In the introductory chapter I dealt with the definition of the concept of mental disability, causes of its creation and definition of degrees of mental retardation. The next chapter is devoted to the combined disability, specifically the yoke of the definition, causes of and classification. In the third chapter is devoted to the importance of the work, the status of the work in a person's life and the status of work for persons with disabilities, including individuals with mental or multiple disabilities in Bachelor thesis I. In the next chapter, I deal with comprehensive rehabilitation system, specifically the remedies rehabilitation, educational resources, social resources, rehabilitation, rehabilitation and special attention devoted work resources, rehabilitation, which will directly affect the Bachelor thesis. Furthermore, I determine a target group the work of rehabilitation and the preconditions for its implementation. In other chapters is devoted to the specification of tools and resources work rehabilitation, employment policy tools and I define jobs that are offered to persons with intellectual disabilities. In the practical part of the thesis, first determine the main aim and target work. The main goal was to determine what are the menus and methods of rehabilitation for people with mental or multiple disabilities with providers of social services. As the target I had set to determine what are the possibilities of transmission from individual to social services on the open employment market. Specifically, I've focused on the resources provided by the rehabilitation of daily, weekly care centers or day service center, in addition to the socio-therapeutic workshops, in a sheltered employment, and employment on the open employment market. To meet the objectives I used a qualitative approach, specifically the semi-structured interview with six providers of social services of the South Bohemian region The analysis of the information obtained, I discovered that if the device is operated daily, weekly social welfare institution or Centre, day services, the services provided are identical, not different from each other. In the case of socio-therapeutic workshops is the diversity of the wider, each device provides a variety of services, different options, some devices have socio-therapeutic workshops directly on the device, others have socio-therapeutic workshops and externally, outside of your device. Protected jobs are also in the majority of providers of social services offered both within and outside the device, always the odd jobs, such as in the kitchen, cleaning, in teahouses and the like. It always depends on the type and degree of disability, on the basis of a levy for the client to the appropriate activities. Location of the client on the open employment market is not very common in most devices, some devices that offer clients or do not provide. Partial objective was to detect transmission, I found that the only limiting factor is the client's disability that limits its options and device options, of course, that the services it offers and delivers. The aim of all devices is to achieve the greatest possible degree of autonomy of the client and allow it to advance from care centers or day service center in the socio-therapeutic workshops, found a protected job, and a job on the open employment market.
|
|
The reflection of František Bakule's work in a relation to a current special educational practice
BALÍKOVÁ, Tereza
František Bakule was a significant Czech teacher during the first half of the 20th century. He was known as the first director of the "Jedlicka Institute in Prague" as well as the founder of so-called "Bakule´s Institute" as well as one of the few representatives of the "Czech alternative approach towards education" which is very well recognized all around the world. His legacy and teachings, however, are currently not being developed on the systematic level and neither they are being put into practise by Czech professional mainstream educational community. We also need to mention that is not used by even the stream of special education, in contrast to many foreign alternative pedagogical trends, which are gaining popularity and are generally applied with success. The aim of this thesis is therefore to analyse the work of Frantisek Bakule through the prism of contemporary school educational environment with emphasis on the education of students with disabilities. The first chapter is devoted to outlining the life journey of Frantisek Bakule, particularly focusing on the major milestones that influenced the formation of his personality, his ideas, inspiration and motivation which was reflected in his teachings and then in his very own coherent concept of education. To be specific, we are introduced to his family background and a significant part is then devoted to description of Frantisek´s experience as a teacher, including stages of operating in Jedlicka´s Institute and in his own "Bakule´s institute". The second part is then focused solely on Bakule´s specific educational concept. First, the core principles of the concept are defined. Later parts then talk about Bakule´s original curriculum and a his proposal of an ideal classroom environment. The text also contains a detailed description of how Bakule approached several subjects, which were at the core of his teaching concept, namely "Work activities", "Music education" and "Arts". Original teaching practices are analysed by using current teaching methodology and terminology. Due to the identified aim and goals of the thesis, the third chapter analyses the current concept of education of the above, according to Bakule´s core areas and principles. The text is designed specifically to be subsequently reflecting the work of Frantisek Bakule from the perspective of today's teaching methods, namely the methods of special education. The idea is to define common points and possible differences and uncover hidden inspirational potential, which is then the main content of the fourth and final chapter. Based on the analysis and all its subsequent reflections, the final chapter tells us that although Bakule´s educational goals don´t differ too significantly from the current concept embedded in the relevant framework of educational programs, to achieve such goals we are currently using very different techniques and methods in comparison to Bakule´s ways. Even though Bakule himself tested and verified all of his concepts in practice, which can be very simply described as "do not teach students about life and work, but through life and work", and these concepts also have been proven correct by various subsequent results of psychological researches, the current system still doesn´t draw from them too much. From all the above it is quite obvious that the legacy of life´s work of Frantisek Bakule is currently not utilized nor it is being appreciated by our professional pedagogical community. On the other hand, we need to note that it may also be due to the level of fragmentation in which his concept and materials were preserved to the present days.
|
|
Specifics of nursing care in patients after transapical aortic valve implantation.
VOTRUBOVÁ, Nataliya
Transcatheter aortic valve implantation (TAVI) is a new and an attractive method in cardiology and as well as in cardiac surgery. It is constantly evolving method which has been developed as an alternative to standard open surgery, especially in patients with severe symptomatic aortic stenosis with unacceptably high perioperative risk or patients who are not suitable for conventional open heart surgery because of age and comorbidities.A teamwork is very importantfor this new method and approach. The choice for TAVI is discussed by the institutional multidisciplinary heart team, typically consisting of interventional cardiologists, imaging-specialists, cardiac surgeons and anaesthesiologists. The first implant in a human being was performed by Cribierin 2002. In Czech Republic this method was first used in 2008. Transcatheter aortic valve implantation (TAVI) was accepted as a minimally invasive alternative to open surgery. This method does not require the use of cardiopulmonary bypass, and cardiac arrest. Other several benefits includinglower risks of bleeding and stroke events, better wound healing, less pain, as well as more rapid early recovery due to preservation of continuity of the sternumthat result in shorter durations of stay in the hospital, earlier rehabilitation and faster returns to normal life. In the presented work was used a combination of qualitative-quantitative methods of investigation. The data was obtained by using the quantitative research. The main technique was using the questionnaires designed for nurses working at the Department of Cardiac Surgery, Hospital Czech Budejovice, a. s. These results were backed up by the implementation of qualitative research, which investigated the patients and physicians view on monitored issues. Questioning method using a semi structured interview technique was used for qualitative research. The results of the survey were processed using descriptive statistics charts in LibreOffice Calc and using diagrams created in LibreOffice Writer. Qualitative results of the research were transcribed from audio recordings and coded, and the base code was created nine categories of interviews with clients/patients and three categories of interviews with doctors. The aim of this work was to explore the specific problem of nursing care about the clients / patients after transapical aortic valve implantation. On the base of our obtained data it is evident, that the client/patient after TAVI may be positioned sideways, the use of surgical drains are less frequently, so the care about the surgical wounds is simpler, patients report less pain in the surgical wound and postoperative rehabilitation and recovery is shorter. H1 - The nurses take care about the clients/patients after transapical aortic valve implantation in the same way as about the clients/patients after open aortic valve replacement, without realizing the differences between the patients treated with different approaches, was not confirmed. The nurses'sees/reported major differences in invasiveness and extent of providing care, rehabilitation, convalescent, in the duration of the hospitalization and better cosmetic effect. The results of the research can serve as a basis for creating the standards of nursing care or educational material for clients/patients. It is also possible to present the results of this work at a specialized seminar for non medical healthcare workers and results can also increase the quality of nursing care about the clients/patients after transapical aortic valve implantation.
|
|
Lifestyle of patients with peripheral arterial disease before and after surgery
REZKOVÁ, Helena
Theoretical background: Peripheral arterial disease is a serious disease of Loir limb arteries which originates from atherosclerosis. The theoretical part deals with the lifestyle. There are mentioned basic risk factors of chronic forms. Further described are the pathophysiology changes generated on the basis of atherosclerosis and related causes for the origin of the disease. Subsequently there are explained methods of classification, developed clinical symptoms, diagnosis and therapy. This section also looks at the role of a nurse in the care of patients with peripheral arterial disease. Objectives: The aim of this work was to evaluate how patients with peripheral arterial disease changed their lifestyle after invasive vascular surgery. There were provided the following research questions: How do patients with peripheral arterial disease approach to the prevention of risk factors? What is in patients with peripheral arterial disease the main impuls for the possible change of their lifestyle? What influences surgery patient's attitude to risk factors for peripheral arterial disease? How crucial is a lifestyle change in patients after surgery for peripheral arterial disease? Methods: The theoretical part is processed using expert sources. The empirical part of the theses was processed using qualitative research. The chosen technique for data collection was semi-structured interviews with patients, with prepared open questions. The research was done in several phases - the first interview was conducted at the patient admission department (before surgery), followed by the next phase after three months, and 6 months after surgery. The interviews were recorded on a prepared form, then transcribed into electronic form and analyzed by open coding method. Results: The research showed that surgery can sometimes be triggered by changes in the patient's lifestyle. The first interviews in the preoperative period focused on how respondents felt, what was their lifestyle before surgery for atherosclerotic changes of the lower extremities. One of the questions was focused on patient knowledge about risk factors for the development of PAD and possible prevention. The second phase of interviews took place 3 months after the surgery. It dealt with the question about the respndents´ lifestyle, the respondents in the postoperative period, whether there were any changes. Some positive changes occurred in eating and there were some changes in doing physical activity. The third stage was carried out six months after surgery, again in order to detect changes in lifestyle. Minor changes came in smoking habits, the issue of diet and physical aktivity. Questions were also focused on the psychological level. We found out who helped patients and what was most motivating in implementing changes. In the conclusion/summing up question the patients marked themselves ow they managed to make a change. Conclusion: The number of patients with peripheral arterial disease and other cardiovascular diseases is increasing. The basis is the start to modify risk factors, namely tobacco use,dietary habits, physical activity. The medical staff members participate on changes in patients´ lifestyle by appropriate education. The problem occurs when the patient despite the support of close people can not cope to carry a twist in their life. There should a medical staff member offer a professional help to deal with this important step. Practical use: The aim is to draw attention to the expansion of education about lifestyle changes for patients diagnosed with PAD also in the postoperative period. Patients who are released to home care should receive enough information that would convince them to change their attitude towards their health, and that surgery is only one of the ways to prevent further attacks and complications. Results can improve communication with patients and focus on increasing their awareness and possibly offer assistance.
|
guest ::
