Analýza cyklů ve verifikačním frameworku pro LLVM IR
Kubík, Jakub; Kofroň, Jan; Parízek, Pavel
2024 - English 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. 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. 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

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 ...

Kubík, Jakub; Kofroň, Jan; Parízek, Pavel
Univerzita Karlova, 2024

Aproximační techniky pro dynamické problémy rozvozu
Zeman, David; Barták, Roman; Fink, Jiří
2024 - English 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 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 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

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 ...

Zeman, David; Barták, Roman; Fink, Jiří
Univerzita Karlova, 2024

Řízení robotického šachového manipulátoru
Kapustík, Boris; Kruliš, Martin; Kopecký, Michal
2024 - English 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. 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. 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

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é ...

Kapustík, Boris; Kruliš, Martin; Kopecký, Michal
Univerzita Karlova, 2024

Praktické dávkové důkazy pro mocnění
Ivanova, Svetlana; Hubáček, Pavel; Mareš, Martin
2024 - English 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++. 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++. 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í

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 ...

Ivanova, Svetlana; Hubáček, Pavel; Mareš, Martin
Univerzita Karlova, 2024

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

Liao, Wei Chun; Doboš, Bohumil; Halamka, Tomáš
Univerzita Karlova, 2024

Čí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

Lempereur, Pauline; Morgado Valentim Albino, Nuno; Riegl, Martin
Univerzita Karlova, 2024

Mezijazykový transfer pro anotaci SynSemClass ontologie
Kašpárek, Petr; Hajič, Jan; Štěpánek, Jan
2024 - English 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... 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... 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

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 ...

Kašpárek, Petr; Hajič, Jan; Štěpánek, Jan
Univerzita Karlova, 2024

Identifikace úzkých hrdel pro relaxaci podmínek v rozvrhování projektů
Nedbálek, Lukáš; Švancara, Jiří; Bulín, Jakub
2024 - English 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í. 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. 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ů

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 ...

Nedbálek, Lukáš; Švancara, Jiří; Bulín, Jakub
Univerzita Karlova, 2024

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 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... 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... 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 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ě ...

Kvapilová, Kateřina; Kozmik, Zbyněk; Piherová, Lenka; Slabý, Ondřej
Univerzita Karlova, 2024

Gabrielova-Roiterova míra v teorii reprezentací
Krasula, Dominik; Šťovíček, Jan
2024 - English 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 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 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í

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 ...

Krasula, Dominik; Šťovíček, Jan
Univerzita Karlova, 2024