Analýza cyklů ve verifikačním frameworku pro LLVM IR
Kubík, Jakub; Kofroň, Jan; Parízek, Pavel
2024 - English
Bugs in compilers can have severe consequences. Apart from traditional methods like testing, one of the ways of keeping compilers correct that gained traction only in recent years is translation validation, a technique ensuring the semantic correctness of optimizations in compilers. Alive2 is an open-source translation validation framework for LLVM that is currently widely used by LLVM developers. In order to make any static analysis tool usable, the frequency of false alarms must be kept to a minimum. Alive2 was designed to have zero false alarms and has been very successful in this endeavor except in the case of certain loops. Our aim in this thesis is to analyze Alive2's loop algorithms in an attempt to find the cause of these false alarms. This was motivated by personal communication with authors of Alive2 who presented the false alarm issue in loops as one of the more challenging and pressing issues in Alive2. We were successful in pinpointing the cause of false alarms and even providing a fix for the issue. Our solution is now a part of the Alive2 framework. Furthermore, we have identified other potential issues in Alive2 which we discuss in the thesis as well. Chyby v překladačích programovacích jazyků mohou mít vážné následky. Kromě tradičních metod, jako je testování, je jedním ze způsobů zajištění správnosti překladačů translation validation, technika zajišťující sémantic- kou správnost optimalizací v překladačích, která se prosadila teprve v po- sledních pár letech. Alive2 je open-source translation validation framework pro LLVM, který je v současnosti široce používán vývojáři LLVM. Pro za- jištění použitelnosti statických analyzátorů je potřeba minimalizovat četnost falešných pozitiv. Alive2 je navržen tak, aby neměl žádná falešná pozitiva a byl v tomto ohledu velmi úspěšný až na některé programy se smyčkami. Na- ším cílem v této práci je analyzovat algoritmy Alive2 pracující se smyčkami se záměrem identifikace příčiny falešných pozitiv. Naše práce byla motivo- vána komunikací s autory Alive2, kteří považovali problematiku falešných poplachů ve smyčkách jako jeden z náročnějších a závažnějších problémů v Alive2. Podařilo se nám přesně určit podstatu problému falešných poplachů a dokonce i opravit tento problém. Naše řešení je aktuálně součástí Alive2. Kromě toho jsme v Alive2 identifikovali další potenciální problémy, o kterých v této práci také pojednáváme.
Keywords:
překladače|LLVM|translation validation|formální verifikace; compilers|LLVM|translation validation|formal verification
Available in a digital repository NRGL
Analýza cyklů ve verifikačním frameworku pro LLVM IR
Bugs in compilers can have severe consequences. Apart from traditional methods like testing, one of the ways of keeping compilers correct that gained traction only in recent years is translation ...
Aproximační techniky pro dynamické problémy rozvozu
Zeman, David; Barták, Roman; Fink, Jiří
2024 - English
This thesis studies the capacitated dynamic vehicle routing problem with changing vehicle availability. It is motivated by the increasing demand for fast and reliable delivery services in recent years. First, we analyze the problem and build its formal model. Then we propose several policies to process dynamically appearing orders. Next, we implement exact and heuristic algorithms like insertion heuristic, mixed integer programming, evo- lutionary algorithm, and ant colony optimization. Finally, we compare the algorithms with different policies and parameters on Kilby's dataset. 1 Tato práce studuje dynamický problém rozvozu s omezenou kapacitou a měnící se dos- tupností vozidel. Motivací pro studium tohoto problému je rostoucí poptávka po rychlých a spolehlivých doručovacích službách v posledních letech. V první části práce analyzujeme problém a vytvoříme jeho formální model. Poté navrhneme a implementujeme strategie pro vypořádání se s dynamickou podstatou problému. Dále implementujeme exaktní a heuristické algoritmy, jako je heuristika vkládáním, celočíselné programování, evoluční algoritmy a optimalizace kolonií mravenců. Nakonec porovnáme algoritmy s různými strategiemi a parametry na Kilbyho datové sadě. 1
Keywords:
problém rozvozu|optimalizace|on-line; vehicle routing|optimization|on-line
Available in a digital repository NRGL
Aproximační techniky pro dynamické problémy rozvozu
This thesis studies the capacitated dynamic vehicle routing problem with changing vehicle availability. It is motivated by the increasing demand for fast and reliable delivery services in recent ...
Řízení robotického šachového manipulátoru
Kapustík, Boris; Kruliš, Martin; Kopecký, Michal
2024 - English
In this thesis, we will use Kinect v2 (from Microsoft Corporation), Stockfish (one of the highest-ranking chess engines), and a custom-made robotic crane capable of accepting simple commands to move across a 3-dimensional plane. The objective is to integrate software for boardgame (Chess) tracking using an easily accessible camera and depth sensor developed by Roman Staněk with an open-source chess engine to create a simple chess robot. Thanks to the tracing, the robot will have the ability to interact with users. The output will be a desktop application for controlling and configuring the robot, switching between game modes, and tracking the game. It will also require creating a virtual mock of the robotic crane to simplify testing and further development. V této práci použijeme Kinect v2 (od Microsoft Corporation), Stockfish (jeden z nej- lépe hodnocených šachových programů), a na zakázku vyrobený robotický manipulátor schopný přijímat jednoduché příkazy k pohybu po 3-rozměrné rovině. Cílem je integrovat software pro sledování deskových her (šachy) pomocí snadno dostupné kamery a hloub- kového senzoru vyvinutýho Romanemem Stankem s open-source šachovým enginem k vytvoření jednoduchého šachového robota. Díky sledování, robot bude mít schopnost ko- munikovat s uživateli. Výstupem bude desktopová aplikace pro ovládání a konfiguraci robota, přepínání mezi herními režimy a sledování hry. Bude to také vyžadovat vytvoření virtuální napodobeniny robotického jeřábu pro zjednodušení testování a dalšího vývoje.
Keywords:
Kinect|integrace|počítačové vidění|Soubory mapované paměti|robotický šachy hrající manipulátor|Meziprocesová komunikace; Kinect|integration|computer vision|memory-mapped files|robotic chess-playing manipulator|inter-process communication
Available in a digital repository NRGL
Řízení robotického šachového manipulátoru
In this thesis, we will use Kinect v2 (from Microsoft Corporation), Stockfish (one of the highest-ranking chess engines), and a custom-made robotic crane capable of accepting simple commands to move ...
Praktické dávkové důkazy pro mocnění
Ivanova, Svetlana; Hubáček, Pavel; Mareš, Martin
2024 - English
This thesis studies batch Proofs of Exponentiation (batch PoE). We explore exist- ing batch PoEs and analyze their verification cost. We also introduce two batch PoEs and compare their performance with the performance of the existing approaches. Our batch PoEs outperform the existing ones, both in theory and in practice. We achieve the improvement in the verification costs by decreasing the expected number of group mul- tiplications. For the practical analysis, we choose the values of the protocol parameters as used in practice, and then measure the time of multiplications and exponentiations on the verifier's side of the discussed protocols in our implementation in C++. Tato práce se zabývá dávkovými důkazy pro mocnění (dávké PoE). Zkoumáme exis- tující dávkové PoE a analyzujeme jejich ověřovací náklady. Také představujeme dva dáv- kové PoE a porovnáváme jejich výkon s výkonem existujících přístupů. Naše dávkové PoE překonávají existující, jak teoreticky, tak i prakticky. Zlepšení ověřovacích nákladů dosahujeme snížením očekávaného počtu grupových násobení. Pro praktickou analýzu vybíráme hodnoty parametrů protokolu používané v praxi a pak měříme čas násobení a mocnění na straně ověřovatele pro zkoumané protokoly v naší implementaci v jazyce C++.
Keywords:
Důkazy pro mocnění|Ověřitelné zpožďovací funkce|Dávkové důkazy; Proof of Exponentiation|Batching|Verifiable Delay Function
Available in a digital repository NRGL
Praktické dávkové důkazy pro mocnění
This thesis studies batch Proofs of Exponentiation (batch PoE). We explore exist- ing batch PoEs and analyze their verification cost. We also introduce two batch PoEs and compare their performance ...
Geopolitické základy nového konfucianismu: Případ Qian Mu
Liao, Wei Chun; Doboš, Bohumil; Halamka, Tomáš
2024 - English
Keywords:
Qian Mu; New Confucianism; geopolitics; critical geopolitics; post-Chineseness; Qian Mu; New Confucianism; geopolitics; critical geopolitics; post-Chineseness
Available in a digital repository NRGL
Geopolitické základy nového konfucianismu: Případ Qian Mu
Čínská dluhová past v Demokratické republice Kongo: Neoklasická geopolitika: případová studie zhrouceného státu (2006-2023) v Demokratické republice Kongo
Lempereur, Pauline; Morgado Valentim Albino, Nuno; Riegl, Martin
2024 - English
Available in a digital repository NRGL
Čínská dluhová past v Demokratické republice Kongo: Neoklasická geopolitika: případová studie zhrouceného státu (2006-2023) v Demokratické republice Kongo
Mezijazykový transfer pro anotaci SynSemClass ontologie
Kašpárek, Petr; Hajič, Jan; Štěpánek, Jan
2024 - English
This work compares two approaches to automatic preannotation of semantic class to verbs in a sentence for the purpose of adding a new language to the SynSemClass ontology. Both approaches rely on a multilingual deep learning classification model fine-tuned on already annotated English, Czech and German data of the ontology. The first, more classical, approach is annotation projection. It uses a parallel corpus and the aforementioned model to make predictions on a source language already present in the ontology and projects the predictions onto the target language using automated word alignment. The second approach, zero-shot cross-lingual transfer, assumes that the multilingual properties of the underlying model are sufficient and that we can make reasonable predictions directly on the target language, even though the model was never trained for that specific task on the specific target language. For the purpose of evaluation, we manually build and annotate a small Korean language dataset to test the performance on a language significantly different from English, Czech and German. We conclude that the zero-shot approach performs notably better than the alignment approach (p < 0.005) obtaining 0.54 both in recall and precision, compared to 0.37 and 0.41 in recall and precision respectively of the alignment... Tato práce porovnává dva přístupy k automatické předanotaci sémantických tříd sloves ve větách za účelem přidání nového jazyka do ontologie SynSemClass. Oba přístupy vycházejí z vícejazyčného deep learning klasifikačního modelu, který byl fine-tunovaný na již anotovaných anglických, českých a německých datech z ontologie. První, více tradiční, přístup je annotation projection. Používá paralelní korpus a výše zmíněný model k vytvoření predikcí na zdrojovém jazyce, který je již obsažen v ontologii, a tyto predikce projektuje na cílový jazyk pomocí automatického word alignmentu. Druhý přístup, zero-shot cross-lingual transfer, předpokládá, že vícejazykové schopnosti deep learning modelu jsou dostatečné a že můžeme vytvořit kvalitní predikce přímo na cílovém jazyce, i když model nebyl nikdy trénován pro danou úlohu na daném cílovém jazyce. Pro účely vyhodnocení ručně vytváříme a anotujeme malý korejský dataset za účelem otestování výsledků na jazyce, který se významně liší od angličtiny, češtiny a němčiny. Dospíváme k závěru, že zero-shot transfer vykazuje výrazně lepší výkon než annotation projection (p < 0,005), s hodnotami recall a precision 0,54, ve srovnání s 0,37 recall a 0,41...
Keywords:
annotation projection|zero-shot cross-lingual transfer|ontologie|vícejazyčné zpracování přirozeného jazyka|lexikální sémantika; annotation projection|zero-shot cross-lingual transfer|ontology|multilingual natural language processing|lexical semantics
Available in a digital repository NRGL
Mezijazykový transfer pro anotaci SynSemClass ontologie
This work compares two approaches to automatic preannotation of semantic class to verbs in a sentence for the purpose of adding a new language to the SynSemClass ontology. Both approaches rely on a ...
Identifikace úzkých hrdel pro relaxaci podmínek v rozvrhování projektů
Nedbálek, Lukáš; Švancara, Jiří; Bulín, Jakub
2024 - English
In modern manufacturing systems, production planners create schedules by iteratively obtaining proposed schedules and adjusting input parameters to satisfy multiple, often competing, optimization goals. The goal of this thesis is to address the problem of reduc- ing the tardiness of a particular manufacturing order in an obtained schedule, which is a practical problem commonly arising in production scheduling. We do this by identifying bottlenecks in the schedule and proposing relaxations to constraints related to the iden- tified bottlenecks. We develop two methods for this purpose, both utilizing constraint programming. The first baseline method adapts existing approaches from the literature and proposes general relaxations. The second method identifies potential improvements in relaxed versions of the problem and proposes relaxations targeting the specific man- ufacturing order. Numerical experiments show that the baseline method achieves great improvements for small costs. while the second method is more reliable in achieving improvements across various problem instances. Plánovači výroby často sestavují rozvrh výroby tak, že iterovavaně získávájí návrhy na rozvrh a upravují vstupní parametry za účelem vyhovět mnohým, často protichůdným, optimalizačním cílům. Cílem této práce je zaměřit se na problém snižování zpoždění, tzv. tardiness, vybrané zakázky v obdrženém rozvrhu, jakožto běžně řešený problém při plánování výroby. Zaměříme se na identifikaci tzv. úzkých hrdel daných rozvrhů za úče- lem relaxace omezujících podmínek souvisejících s těmito úzkými hrdly. Pro tento účel představíme dvě metody. První adaptuje existující přístupy z literatury v kombinaci s návrhy obecných relaxací podmínek. Druhá identifikuje potenciální zlepšení v relaxova- ných verzích problému a navrhuje relaxace zaměřující se na konkrétní zpožděnou zakázku. Numerické experimenty ukazují, že zatímco první metoda nachází dobrá zlepšující řešení za nízké ceny, druhá metoda je v nacházení zlepšujících řešení více konzistentní.
Keywords:
plánování výroby|RCPSP|úzká hrdla|relaxování omezujících podmínek; scheduling|RCPSP|bottlenecks|constraint relaxation
Available in a digital repository NRGL
Identifikace úzkých hrdel pro relaxaci podmínek v rozvrhování projektů
In modern manufacturing systems, production planners create schedules by iteratively obtaining proposed schedules and adjusting input parameters to satisfy multiple, often competing, optimization ...
Význam různých zdrojů a sekvenančních protokolů při zvyšování přesnosti NGS analýz v diagnostických aplikacích
Kvapilová, Kateřina; Kozmik, Zbyněk; Piherová, Lenka; Slabý, Ondřej
2024 - English
1 ABSTRACT Continued advances in next-generation sequencing (NGS) technology, such as capacity, speed, and reduced cost per sequenced base, revolutionize personalized medicine and bring genomics into routine clinical practice. Nevertheless, NGS is still under rapid development, and the variability of sequencing protocols and validation procedures is one of its current bottlenecks. This thesis aimed to study the influence of different sample sources and NGS protocols (NGS library construction-sequencing-data analysis) on the accuracy of NGS analysis in diagnostic applications. In the first study, performed during the COVID-19 pandemic outbreak, we developed NGS protocols suitable for a whole genome analysis of the SARS-CoV-2 virus. Subsequently, in the second study, we examined the suitability of human saliva-derived gDNA for genomic/genetic analysis of selected variant types compared to traditional blood-derived gDNAusing validated NGS protocol and statistical comparison of the obtained data. Whole genome analysis of the SARS-CoV-2 genome was performed using two captured- based approaches and one amplicon-based approach to study the quality and effectivity of the respective NGS protocols. Synthetic controls were employed to verify the accuracy and specificity of the developed NGS protocols. We proved that... 1 Souhrn Neustálé pokroky v technologii sekvenování nové generace (NGS), jakými jsou kapacita, rychlost a snížené náklady na sekvenovaní, vedou k revoluci v personalizované medicíně, tím, jak postupně přináší genomiku do rutinní klinické praxe. NGS se stále rychle vyvíjí, avšak variabilita sekvenačních protokolů a validačních postupů je jedním z jeho problematických rysů. Cílem této práce bylo zhodnotit význam různých zdrojů vzorků a sekvenačních protokolů (od přípravy sekvenační knihovny-sekvenování-analýzi dat) pro zvýšení přesnosti NGS analýzy v diagnostických aplikacích. V první studii, provedené během vypuknutí pandemie COVID-19, jsme vyvinuli NGS protokoly vhodné pro analýzu celého genomu viru SARS-CoV-2. Následně jsme ve druhé studii zkoumali vhodnost lidské genomické DNA (gDNA) pocházející ze slin pro genomickou/genetickou analýzu vybraných variantních k tradiční gDNApocházející z krve pomocí validovaného NGS protokolu a statistického srovnání získaných dat. K ověření účinnosti sekvenačních protokolů pro analýzu celého genomu SARS-CoV-2 byly použity dva sekvenační přístupy založené na zachycení části genomu a jeden sekvenanční přístup založený na amplifikaci částí genomů. K ověření přesnosti a specifičnosti vyvinutých NGS protokolů byly použity syntetické kontroly. Prokázali jsme, že kvantifikace...
Keywords:
NGS; WGS; WES; analýza variant; slinná gDNA; validace NGS protokolu; NGS; WGS; WES; genomics variant analysis; saliva-derived gDNA; validation guideline
Available in a digital repository NRGL
Význam různých zdrojů a sekvenančních protokolů při zvyšování přesnosti NGS analýz v diagnostických aplikacích
1 ABSTRACT Continued advances in next-generation sequencing (NGS) technology, such as capacity, speed, and reduced cost per sequenced base, revolutionize personalized medicine and bring genomics into ...
Gabrielova-Roiterova míra v teorii reprezentací
Krasula, Dominik; Šťovíček, Jan
2024 - English
The Gabriel-Roiter measure is a module-theoretic invariant, defined in 1972 by P. Gabriel. It is an order-preserving function that refines a composition length of a module by also taking lengths of indecomposable submodules into account. We calculate all Gabriel-Roiter measures for finite-length representa- tions of an orientation of a Dynkin graph D4 and an orientation of a Euclidean graph ˜A3. In 2007, H. Krause proposed a combinatorial definition of the Gabriel-Roiter measure based on other length functions instead of composition length. We study these alternative Gabriel-Roiter measures on thin representations of quiv- ers whose underlying graph is a tree. 1 Gabriel-Roiterova míra je invariant na modulech, definovaný v roce 1973 P. Gabrielem. Je to uspořádání-zachovávajicí funkce, která zjemňuje kompoziční délku modulu tím, že bere v potaz též délky nerozložitelných podmodulů. Spočí- táme všechny Gabriel-Roiterovi míry pro reprezentace konečné délky pro konkrét- ní orientaci Dynkinova grafu D4 a Euklidovského grafu ˜A3. V roce 2007 H. Krause navrhl kombinatorickou definici Gabriel-Roiterovi míry založenou na jiných funkcích než kompoziční délce. Tyto alternativní Gabriel- Roiterovi míry studujeme na tenkých reprezentacích toulců, které neobsahují neorientované cesty. 1
Keywords:
Gabriel-Roiter measure|representations of quivers|thin representations; Gabriel-Roiterova míra|reprezentace toulců|tenké reprezentace
Available in a digital repository NRGL
Gabrielova-Roiterova míra v teorii reprezentací
The Gabriel-Roiter measure is a module-theoretic invariant, defined in 1972 by P. Gabriel. It is an order-preserving function that refines a composition length of a module by also taking lengths of ...
NRGL provides central access to information on grey literature produced in the Czech Republic in the fields of science, research and education. You can find more information about grey literature and NRGL at service web
Send your suggestions and comments to nusl@techlib.cz
Provider
Other bases