1,975 research outputs found
The picture of David Hoyer from Jan Kupecký at Leipzig
No full textThe thesis focuses on portrait on painting of David Hoyer from baroque artist Jan Kupecky that is placed in Museum der bildenden Künste in Leipzig. Firstly, I will deal with life and work of the author Jan Kupecky. The main focus will be dedicated to the painting from 1711 which depicts Saxon painter David Hoyer with lyra. I will try to unveil more information about life of the depicted man, consequently, I will concentrate on the actual type of portaval style and mention other significant work of the same nature made by the author prior 1711. This actual painting example will allow me to show how the portrait creation was forming not only in life of Jan Kupecky but also in context of whole Europe
Analysis of a File System Using the Verifying C Compiler
No full textTitle: Analysis of a File System Using the Verifying C Compiler Author: Bc. David Škorvaga Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Jan Kofroň, Ph.D. Abstract: Formal verification is a way to improve reliability of software systems. One approach of formal verification is focused on proving correctness of annotat- ed source code of an established programming language. Verifying C Compiler (VCC) is a verifier for concurrent C that accepts an annotated code in C language and automatically verifies its correctness with respect to the given annotation. There have been successful attempts to verify some critical systems, including the operating system kernel. Another critical part of operating system is its file system. In the thesis, we choose FatFs file system, a simple device-independent implementation of the FAT file system. We specify a part of it using the VCC annotation and successfully verify its correctness. Keywords: Formal Verification, File System, VC
Analýza souborového systému pomocí Verifying C Compiler
No full textNázev práce: Analýza souborového systému pomocí Verifying C Compiler Autor: Bc. David Škorvaga Katedra: Katedra distribuovaných a spolehlivých systémů Vedoucí diplomové práce: RNDr. Jan Kofroň, Ph.D. Abstrakt: Formální verifikace je jeden ze způsobů, jak zlepšit spolehlivost soft- warových systémů. Jeden z přístupů formální verifikace se zaměřuje na dokazo- vaní správnosti anotovaného zdrojového kódu v široce používaném programovacím jazyce. Verifier C Compiler (VCC) je verifikátor pro concurrent C, který přijímá anotovaný kód v jazyce C a automaticky ověřuje jeho správnost s ohledem na tuto anotaci. Už se objevily úspěšné pokusy o ověření některých kritických systémů, včetně jádra operačního systému. Další důležitou součástí operačního systému je jeho systém souborů. V diplomové práci jsme si vybrali souborový systém FatFs, odlehčenou implementaci souborového systému FAT, nezávislou na zařízení. V této práci vytvoříme specifikaci jeho části pomocí anotace VCC a úspěšně ověříme jeho korektnost. Klíčová slova: Formal Verification, File System, VCCTitle: Analysis of a File System Using the Verifying C Compiler Author: Bc. David Škorvaga Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Jan Kofroň, Ph.D. Abstract: Formal verification is a way to improve reliability of software systems. One approach of formal verification is focused on proving correctness of annotat- ed source code of an established programming language. Verifying C Compiler (VCC) is a verifier for concurrent C that accepts an annotated code in C language and automatically verifies its correctness with respect to the given annotation. There have been successful attempts to verify some critical systems, including the operating system kernel. Another critical part of operating system is its file system. In the thesis, we choose FatFs file system, a simple device-independent implementation of the FAT file system. We specify a part of it using the VCC annotation and successfully verify its correctness. Keywords: Formal Verification, File System, VCCDepartment of Distributed and Dependable SystemsKatedra distribuovaných a spolehlivých systémůMatematicko-fyzikální fakultaFaculty of Mathematics and Physic
Cult: A Composite Novel
No full textCult (redacted)
The first component of the thesis is a composite novel called Cult which falls into two parts with seven narratives in each. Part 1 tracks the protagonist, Ellen, from her first involvement with the cult through to her eventually leaving it. Although fiction, the first half of the book answers the kinds of questions the author is asked when people discover that she was once a sannyasin (a follower of the guru Bhagwan Shree Rajneesh). While the experiences of meditation, group therapy and communal living are all faithfully rendered within the stories, the need for strong characters, narrative drive and a lightness of touch takes precedence.
Part 2 picks up Ellen’s story some twenty or so years later and explores what becomes of her in middle age. It also looks at other groups in society, such as academia, the law and the internet dating community which each have their own jargon, hierarchies, rituals and rules but are not considered to be cults.
The book examines the question raised in the Epigraph, ‘how do we be together when we feel so alone’ with a focus on relationships other than the familial and the romantic.
Collisions, Chasms and Connections: a Performative Exploration of the Composite Novel Form
The second part of the thesis is both a critical and creative response to three contemporary American books: Olive Kitteridge by Elizabeth Strout; A Visit from the Goon Squad by Jennifer Egan; and Legend of a Suicide by David Vann. The critical element comprises a close reading of the three books; a chronological reconstruction of their overarching storylines; and a consideration of what their authors have said about writing the books. It concludes that, in the composite novel, the simultaneous presentation of multiple views and storylines operate much like a 3D image to give the impression of depth to the characters and situations rendered. The creative element of the essay is a playful and personal response to the texts
Home automation
No full textTitle: Home automation Author: Jan Kytka Department: Department of Theoretical Computer Science and Mathematical Logic Supervisor: RNDr. David Obdržálek, Ph.D., Department of Theoretical Computer Science and Mathematical Logic Abstract: In the area of home automation and control based on data from input units, there are many commercial and hobby solutions. They offer different paradigms for repre- senting control rules, such as description of trigger conditions and events, gate networks, etc. We analyzed the shortcomings of event-driven systems and, based on them, we de- signed and implemented an application which represents the rules as explicit transition function expressions. We showed how to formulate more complex control tasks in this different paradigm and had it pre-tested with a small sample of users. They agreed that it is very usable, even if perhaps more difficult to understand. Keywords: automation expressions control application MQTT IoT ASP.NET 1Název práce: Systém pro automatickou regulaci v domácnosti Autor: Jan Kytka Katedra: Katedra teoretické informatiky a matematické logiky Vedoucí bakalářské práce: RNDr. David Obdržálek, Ph.D., Katedra teoretické informa- tiky a matematické logiky Abstrakt: V problematice automatizace domácnosti a obecně řízení na základě dat ze vstupních jednotek existuje mnoho komerčních i hobby řešení. Nabízejí různá paradig- mata zápisu pravidel regulace, jako je popis reakcí na události, propojení pomocí sítě hradel, aj. Analyzovali jsme nedostatky událostmi řízených systémů a na základě nich jsme navrhli a implementovali aplikaci, kde se pravidla popisují explicitním zápisem pře- chodové funkce. Ukázali jsme, jak v tomto odlišném paradigmatu formulovat složitější regulační úlohy a předběžně ho nechali otestovat malým vzorkem uživatelů. Ti se shodli na tom, že je velmi použitelné, i když obtížnější na pochopení. Klíčová slova: automatizace výrazy řízení aplikace MQTT IoT ASP.NET 1Department of Theoretical Computer Science and Mathematical LogicKatedra teoretické informatiky a matematické logikyMatematicko-fyzikální fakultaFaculty of Mathematics and Physic
David Platt Headlines Missions Conference
No full textDavid Platt, president of the Southern Baptist Convention’s International Mission Board, will be the featured speaker during Cedarville University’s annual Missions Conference, January 12-14.
Platt, who previously served as the lead pastor at The Church at Brook Hills in Birmingham, Alabama, is the author of several books and the founder of Radical.net, a resource ministry that helps churches around the globe.
He will speak at 7 p.m. on Jan. 12 and again at 10 a.m. on Jan. 13. Platt is one of four speakers who will take the stage during the Missions Conference, which has the theme “God’s Heart for the Nations.
Does strict employment protection discourage job creation? Evidence from Croatia
No full textEmployment protection legislation in Croatia is among the most strict in Europe. Firing is difficult and costly, and flexible forms of employment are limited. Is this apparent rigidity reflected-as one would expect based on standard economic theory-in low labor market dynamics? Is job creation low and hiring limited? Is the job security of insiders achieved at the cost of outsiders not being able to enter thelabor market? The author attempts to answer these questions by examining job flows. If the employment protection legislation is binding, then job and worker turnover should be low. He shows that this is indeed the case. Hiring is limited and the average job tenure is very long in Croatia. Job destruction is low, however job creation is still lower. The result is accumulation of unemployment, in large part due to new labor market entrants not being able to find a job. The high degree of job protection also seems to strengthen the bargaining position of insiders and results in relatively high wages. So, wages in Croatia are higher than among its competitors, even after adjusting for productivity. These high labor costs are likely to contribute to limited job creation in existing firms, but also are likely to discourage the entry of-and thus job creation in-new firms. The author presents evidence that firm growth has been indeed limited in Croatia, contributing to the low employment level. The author examines other potential causes of high unemployment in Croatia (the unemployment benefit system, labor taxation, the wage structure, and skill and spatial mismatches). He argues that they do not play a substantial part in accounting for poor labor market outcomes in Croatia. The author concludes that the stringent employment protection legislation is the key labor market institution behind low job creation and high unemployment. Based on this he recommends specific measures aimed at liberalizing the labor market to foster job creation and employment.Labor Management and Relations,Labor Policies,Labor Markets,Environmental Economics&Policies,Trade Finance and Investment,Labor Markets,Labor Management and Relations,Labor Standards,Banks&Banking Reform,Environmental Economics&Policies
Static analysis of XSLT programs
No full textNazev prace: Staticka, analyza. XSLT programu Autor: ,Ian Cervak Katedra: Katcdra softwarovcho inzenyr.stvi Vedouci diplomove prace: RNDr. David Bednarek E-mail vedouciho: David.Bcdnarekinnir.cuni.cz Abstrakt: Zabyvame se statickou analyzou XSLT programu se znalosti sche- matu vstupnich dokumeutu. Analyza, je zamcfena, na odhalovani behovych chyb v prograniecli. Konkretue hiedamp nedosazitelna pravidla,, slepa vo- lani a cykly ve volamch pravidcl, jako zdroj potrncialne nekonecneho behu prograniu. XSLT je t\iringo\sky uplny ja/yk, konipletni staticka analyza je z principu neproveditelna, feseni tohoto problcniu jsou Jen i^fiblizna. Pre- zentovane rcseui je kvazi-sinndace bohu programu nad niodeleni XML doku- inentu. Vyslodny graf toku fizeni programu rlava infonnaee o zkouinanych probleineeh. Algcjritinus simulace je zavedeu nezavisle na pouzitein inodclu, coz pfinasi moznost analyzy na. ruzne urovni dotailu. Klicova slova: a.nalyza toku rizeiii, XSLT, XML Schema, behove dryby, zasta- vcni Title: Static analysis of XST/F ]>rograms Author: Jan Cervak Department: Department of Software Engineering Supervisor: RXDr. David Bcdnarek Supervisor's e-mail address: David.BednarekyimU'.cnni.cz Abstract: The aim of this work is static analysis of XSLT programs with the knowledge of an input document's schema...
The Occupational Participation and Coping Experiences of Persons With Visual Changes After Traumatic Brain Injury: A Qualitative Study
No full textAbstract
Date Presented 3/30/2017
A phenomenological approach was applied to understand the experiences of three participants with traumatic brain injury (TBI) and visual inefficiencies. Five themes resulted: symptoms that complicated life, negative feelings during occupation, changes in coping, personal relationship impact, and lack of resource education.
Primary Author and Speaker: Suzanne Vetter
Additional Authors and Speakers: Katie Kruger
Contributing Authors: Jan Stube, David Biberdorf</jats:p
Nové metody ve statistickém rozpoznávání řeči
No full textTitle: New Methods in Statistical Speech Recognition Author: David Klusáček Department: Institute of Formal and Applied Linguistics (ÚFAL), Faculty of Mathematics and Physics in Prague, Malostranské náměstí 25, 118 00 Praha 1. Advisor: Prof. RNDr. Jan Hajič, Dr., Institute of Formal and Applied Linguistics. Abstract: This works aims to identify limits of contemporary speech rec- ognizers and tries to come up with methods that could push back the fron- tiers. After describing the state of the art, the weakest link of the chain has been identified in the acoustic front-end, especially when working in harsh acoustic conditions. NUFIBA front-end, the proposed solution, includes re- verb compensation and speaker/background segmentation as well as contin- uous SNR monitoring which, thru cooperation with acoustic model, hinders from avalanche spreading of recognition errors. Owing to the lack of time, only a phoneme recognizer was finally implemented, although large blocks of originally intended word-based continuous speech recognizer were implemented and tested (such as the MMI-class based language model).Název Práce: Nové metody ve statistickém rozpoznávání řeči Autor: David Klusáček Katedra: Ústav formální a aplikované lingvistiky, MFF UK Školitel: Prof. RNDr. Jan Hajič, Dr., ÚFAL. Abstrakt: Tato práce se pokouší identifikovat limity současných rozpoznávačů řeči a navrhnout metody jak jejich omezení překonat. Po historickém úvodu a popisu současného stavu je jako nejslabší článek řetězu prohlášen akustický front-end, zejména jeho činnost za zhoršených zvukových podmínek. Navrho- vané řešení, tzv. NUFIBA front-end, zahrnuje kompenzaci ozvěny, segmentaci zvuku na řečníka a pozadí, a průběžné sledování SNR, které v součinnosti s akustickým modelem zabraňuje lavinovému šíření chyb. Z důvodu nedostatku času jiz bohužel nedošlo k implementaci celého rozpoznávače řeči (i když ně- které části byly značně rozpracovány, například jazykový model založený na MMI třídách). Nové myšlenky tak byly vyzkoušeny pouze v jednodušším roz- poznávači fonémů. Klíčová slova: Automatické rozpoznávání řeči, souvislá řeč, NUFIBA front- end, Jazykový model, Sluchová dráha, MMI, Shlukování, Slepá dekonvoluce, Časové a frekvenční maskování, Potlačení ozvěny, Rozpoznávání fonémů.Ústav formální a aplikované lingvistikyInstitute of Formal and Applied LinguisticsFaculty of Mathematics and PhysicsMatematicko-fyzikální fakult
- …
