|
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.
|
|
Navigation of mobile robots
Rozman, Jaroslav ; Matoušek,, Václav (referee) ; Šolc, František (referee) ; Zbořil, František (advisor)
Mobile robotics has been very discussed and wide spread topic recently. This due to the development in the computer technology that allows us to create better and more sophisticated robots. The goal of this effort is to create robots that will be able to autonomously move in the chosen environment. To achieve this goal, it is necessary for the robot to create the map of its environment, where the motion planning will occur. Nowadays, the probabilistic algorithms based on the SLAM algorithm are considered standard in the mapping in these times. This Phd. thesis deals with the proposal of the motion planning of the robot with stereocamera placed on the pan-and-tilt unit. The motion planning is designed with regard to the use of algorithms, which will look for the significant features in the pair of the images. With the use of the triangulation the map, or a model will be created. The benefits of this work can be divided into three parts. In the first one the way of marking the free area, where the robot will plan its motion, is described. The second part describes the motion planning of the robot in this free area. It takes into account the properties of the SLAM algorithm and it tries to plan the exploration in order to create the most precise map. The motion of the pan-and-tilt unit is described in the third part. It takes advantage of the fact that the robot can observe places that are in the different directions than the robot moves. This allows us to observe much bigger space without losing the information about the precision of the movements.
|
|
Optimization of network flow monitoring
Žádník, Martin ; Lhotka,, Ladislav (referee) ; Matoušek, Radomil (referee) ; Sekanina, Lukáš (advisor)
The thesis deals with optimization of network flow monitoring. Flow-based network traffic processing, that is, processing packets based on some state information associated to the flows which the packets belong to, is a key enabler for a variety of network services and applications. The number of simultaneous flows increases with the growing number of new services and applications. It has become a challenge to keep a state per each flow in a network device processing high speed traffic. A flow table, a structure with flow states, must be stored in a memory hierarchy. The memory closest to the processing is known as a flow cache. Flow cache management plays an important role in terms of its effective utilization, which affects the performance of the whole system. This thesis focuses on an automated design of cache replacement policy optimized to a deployment on particular networks. A genetic algorithm is proposed to automate this process. The genetic algorithm generates and evaluates evolved replacement policies by a simulation on obtained traffic traces. The proposed algorithm is evaluated by designing replacement policies for two variations of the cache management problem. The first variation is an evolution of the replacement policy with an overall low number of state evictions from the flow cache. The second variation represents an evolution of the replacement policy with a low number of evictions belonging to large flows only. Optimized replacement policies for both variations are found while experimenting with various encoding of the replacement policy and genetic operators. The newly evolved replacement policies achieve better results than other tested policies. The evolved replacement policy lowers the overall amount of evictions by ten percent in comparison with the best compared policy. The evolved replacement policy focusing on large flows lowers the amount of their evictions two times. Moreover, no eviction occurs for most of the large flows (over 90%). The evolved replacement policy offers better resilience against flooding the flow cache with large amount of short flows which are typical side effects of scanning or distributed denial of service activities. An extension of the replacement policy is also proposed. The extension complements the replacement policy with an additional information extracted from packet headers. The results show further decrease in the number of evictions when the extension is used.
|
|
Právní a zdravotně sociální aspekty činnosti OSPOD jako ustanovených opatrovníků v zámu nezletilých dětí
BORSKÁ, Jana
The Czech Republic as a signatory of the Convention on the Rights of the Child has vested the practice of state administration in the field of care for minor children to municipalities with extended powers, where the protection of the rights and legitimate interests of minor children is safeguarded by state authorities of social and legal protection of children (ASLPC hereinafter). These authorities are incorporated to the extent laid down by the Act on Social and Legal Protection of Children (Act No 359/1999 Coll., as amended). The position and roles of ASLPC and their competence and jurisdiction are also regulated by the same act. The position of workers of these authorities and its legal embodiment is equally important. Regarding professionality, there are high demands on these workers. In the Czech Republic, significant changes in legislature have been made over the past three years. These amendments have led to the strengthening of the rights of minor children and to the establishing of new tools for their protection. In connection with the adoption of new substantive regulation of family law, which is now exhaustively dealt with by the Act No 89/2012 Coll., the Civil Code, new procedural rules have been established regarding protection of rights of minor children. Such procedural legislation includes (apart from the long-existent Act No. 99/1963, the Code of Civil Procedure) the Act No 292/2013 Coll., on Special Civil Proceedings. The decision-making regarding minor children has been vested mainly by the state into the competence of courts. The courts appoint the locally relevant ASLPC as a guardian who then represents the interests of minor children. The purpose, interwoven with and derived from the first one, was to explore the opinions of selected social workers of ASLPC and of district court judges regarding the defined problems occurring during the work of ASLPCs and courts while protecting the interests of minor children. These particularly include: the use of the tool of precautionary measure; problems of different territorial jurisdiction of courts and ASLPCs; processing of complaints regarding bias in various phases of the proceedings; professional training of workers of ASLPC It is evident from the proposals of both judges and ASLPC workers that it is necessary to unify territorial jurisdiction. The courts are suggesting the priority criterion of the address where the child mainly resides. ASLPC workers suggest the official permanent residence as the prime criterion. Bias causes problems in all phases of proceedings. It is obvious that courts take differing approaches towards the solution of this problem (some courts solve the problem of bias complaints filed by the parties while other courts do not) and for ASLPC workers it is difficult to assess how to act when such complaint is raised against them. The training of ASLPC workers - workers are obliged to educate themselves and their employer is obliged to finance such training. Not all ASLPCs are able to provide training in the required extent - due to financial reasons (the average costs of education of one employee pose from 9,169 to 13,400 CZK annually and they cover approximately 6 days of training). The heavy work-load caused by insufficient numbers of ASLPC employees prevents them from completing such compulsory training. As part of the examination of the "participation of a collision guardian in court proceedings" it has been found out that irregular participation of the worker in the proceedings (absence from participation in appeals proceedings); incomplete reports (directed to courts) from surveys in families. Based on comprehensive examination of the problems of territorial jurisdiction, it was recommended that requests are independently recorded and financial compensation is provided for ASLPCs who are requested to represent minors in front of courts, to draft proposals for precautionary measures.
|
|
Are There Any Digital Curators in Czech Libraries?
Římanová, Radka ; Melichar, Marek
The development of digital repositories reveals the need for new Czech terminologies for library positions. One such job title or specialization is “digital curator”, a term which refers to a specialist responsible for digital collections. Competencies for digital curators include technical, organizational, communication, and marketing skills as well as some level of expertise in computer science as well as in information and library science. A survey of several administrators of Czech digital libraries asks how to best professionally label this group of library staff with respect to the actual activities they perform in their jobs - digital curators, administrators of digital libraries, or digital librarians? Job titles have a strong impact on higher education curricula, on the management of libraries, and also on the coordinated system of remuneration of employees at libraries, academic, and research institutions.
Fulltext: idr-1041_3 -  PDF; idr-1041_4 - PDF
Slides: idr-1041_1 - PDF; idr-1041_2 - PDF
Video: idr-1041_5 -  MP4
|
|
Faktory ovlivňující poptávku po osobních automobilech v ČR
ČURILLOVÁ, Michaela
The bachelor thesis investigates factors which influence the demand for passenger cars in the Czech Republic. The theoretical part of this work is focused on basic terms and determinants which are important for the demand. Further it describes particular statistical methods, which are used for the analysis. The practical part contains the introduction to the automotive industry and the description of specific attributes of the demand for passenger cars. This part analyses factors which may have an effect on the demand for passenger cars in the Czech Republic. The main factors and the dependence are explained by applying econometric methods. Analyzing reveals these important factors: number of registrations of passenger cars, consumer prices of new and used passenger cars, consumer prices of fuel, population and income.The conclusion contains the summary of impacts on the specific demand.
|
|
The Potential of Railway Stations in Trade and Tourism
MALECHOVÁ, Adéla
The diploma thesis was focused especially on train station service supplies and on the potential offered by unutilized or misused spaces of a train station hall. The main goal was to find, define and examine this potential in a chosen station within Trade and Tourism development in a chosen place. The railway station in Ceske Budejovice became the chosen train station. The thesis contains a mapping of the given place, a marketing research carried out among train passengers travelling with the Czech Railway company, as well as on social networks through an on-line survey. The secondary objective was a determination of several possible suggestions to improve the train station, out of which one main suggestion was chosen and subsequently analysed.
|
|
Exchange Differences in Accountancy in an Enterprise
ŠPILAUEROVÁ, Hana
In connection with economy globalisation, international cooperation of companies and expansion of international trade, the issue of exchange rates, transfer of currencies and exchange differences concerns companies more and more. The aim of this thesis was to show in theory as well as in practice how a company transfers assets and liabilities expressed in a foreign currency into Czech crowns by means of exchange rates. In the theoretical part, methods are described how to realise this transfer and abide by legal regulations concerning this issue. Next, accounting operations are given where it comes to creation of exchange differences. Data for the practical part were provided by the enterprise ESSA Ltd. On these data, the influence of exchange differences on the company's economic results in the years 2009-2015 is shown. The method of accounting exchange differences is presented on individual cases of accounts receivable and accounts payable. For orientation in the issue, model examples of other accounting cases are given where exchange differences may arise.
|
|
Business Plan of a Small Enterprise Providing Services
BOČANOVÁ, Eliška
This bachelor thesis is dedicated to develop a business plan for the establishment and the development of small enterprise providing services in the fashion industry. The thesis is divided into two parts the theoretical part and the practical part. The theoretical part involves the basic terminology about business. It defines structure, contents and the principles of building development a business plan too. The practical part is completely prepared business plan for enterprise start-up. It is focused on the market analysis dealing with internal and external environment of the company, such as Porter five forces analysis and analysis of strenghts and weaknesses. Then a financial plan with initial costs, anticipated revenues and from the default operating result follows. The practical part includes opening balance sheet of corporate assets and liabilities. This business plan can eventually serve as a basic for real setting up a business.
|
guest ::
