Analýza cyklů ve verifikačním frameworku pro LLVM IR
Kubík, Jakub; Kofroň, Jan; Parízek, Pavel
2024 - anglický 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. Klíčová slova: překladače|LLVM|translation validation|formální verifikace; compilers|LLVM|translation validation|formal verification Plné texty jsou dostupné v digitálním repozitáři NUŠL 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 ...

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

Nutriční aspekty v dermatologii
Mihu, Ecaterina; Maruna, Pavel; Horová, Eva
2024 - český Klíčová slova: Klíčová slova: nutrice; dermatologie; psoriáza; pelagra; kurděje; akné; růžovka; dna; Keywords: nutrition; dermatology; psoriasis; pellagra; scorbut; acne vulgaris; rosacea; gout Plné texty jsou dostupné v digitálním repozitáři NUŠL Nutriční aspekty v dermatologii

Mihu, Ecaterina; Maruna, Pavel; Horová, Eva
Univerzita Karlova, 2024

Aproximační techniky pro dynamické problémy rozvozu
Zeman, David; Barták, Roman; Fink, Jiří
2024 - anglický 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 Klíčová slova: problém rozvozu|optimalizace|on-line; vehicle routing|optimization|on-line Plné texty jsou dostupné v digitálním repozitáři NUŠL 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 ...

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

Validátor CSV souborů dle W3C doporučení CSV on the Web
Kolcun, Michal; Klímek, Jakub; Svoboda, Martin
2024 - slovenský The goal of this thesis was to create a validator of CSV files according to the CSV on the Web recommendations, which enhance CSV data format. This validation is needed to increase the quality of data on the web. Validator offers multiple user-friendly interfaces in the form of CLI app, web service and web app. The validator itself is a library implemented in the popular object-oriented programming language C#. In this thesis we will describe the development of the validator, starting with the recommendations and analysis of existing solutions, through the design of architecture and user interfaces, and finish with the description of implementation, testing, and evaluation of software solution. 1 Cieľom práce bolo vytvorenie validátoru CSV súborov podľa odporúčaní CSV on the Web, ktoré bližšie špecifikujú dátový formát CSV. Takáto validácia je potrebná pre zvýšenie kvality dát na webe. Validátor poskytuje používateľom viacero prívetivých používateľských rozhraní v podobe CLI aplikácie, webovej služby a webovej aplikácie. Validačná funkcionalita je implementovaná v podobe knižnice v populárnom objektovo- orientovanom jazyku C#. V texte práce priblížime vývoj validátora a všetkých jeho po- užívateľských rozhraní od samotných doporučení CSV on the Web, analýzy existujúcich riešení, návrhu architektúry, až po samotnú implementáciu, testovanie a evaluáciu vý- sledného softvérového diela. 1 Klíčová slova: CSV|JSON-LD|Validácia dát|web; CSV|JSON-LD|web|validator Plné texty jsou dostupné v digitálním repozitáři NUŠL Validátor CSV souborů dle W3C doporučení CSV on the Web

The goal of this thesis was to create a validator of CSV files according to the CSV on the Web recommendations, which enhance CSV data format. This validation is needed to increase the quality of data ...

Kolcun, Michal; Klímek, Jakub; Svoboda, Martin
Univerzita Karlova, 2024

Řízení robotického šachového manipulátoru
Kapustík, Boris; Kruliš, Martin; Kopecký, Michal
2024 - anglický 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. Klíčová slova: 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 Plné texty jsou dostupné v digitálním repozitáři NUŠL Ří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 ...

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 - anglický 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++. Klíčová slova: Důkazy pro mocnění|Ověřitelné zpožďovací funkce|Dávkové důkazy; Proof of Exponentiation|Batching|Verifiable Delay Function Plné texty jsou dostupné v digitálním repozitáři NUŠL 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 ...

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

Generování textů českých coververzí anglických písní
Štěpánková, Barbora; Rosa, Rudolf; Mareček, David
2024 - český This thesis explores the topic of generating Czech lyrics to English cover songs. Songs are often adapted to different languages to make them more available to people who do not necessarily speak the language of the original song. During the translation process, however, it is essential to preserve the singability of the text in relation to the melody of the original song, as well as the meaning of the song, so that the translated text fits the context of the original. Currently, such translations are done by hand. We analyze and present the first approaches to solve this problem for Czech through automatic generation using NLP methods. In our work, we create and provide a dataset consisting of pairs of English song lyrics and their official Czech translations. We also provide a dataset of pure Czech song lyrics. We compare the quality of several generative language models. To thoroughly evaluate and analyze their quality, we introduce several automatic metrics and take into account the results of manual evaluation. We find that smaller trained models perform better than larger untrained models. In addition, context is important for the generation of good covers. Finally, we show that our task can be approached from both the translation and generation point of view. 1 Tato práce se zabývá tvorbou českých textů k anglickým originálním písním. Písně jsou často překládány do různých jazyků, aby byly přístupné i lidem, kteří nerozumějí původnímu jazyku. Během procesu překladu je však nezbytné zachovat zpěvnost textu vzhledem k melodii půvdní písně, stejně tak jako význam písně, aby i přeložený text seděl do kontextu originálu. V současné době se takové překlady provádějí ručně. Provádíme analýzu a představujeme první přístupy k řešení tohoto problému pro češtinu prostřed- nictvím automatického generování pomocí NLP metod. V naší práci vytváříme a poskytu- jeme dataset sestávající se z dvojic Anglických písňových textů a jejich oficiálních Českých překladů. Také poskytujeme dataset z čistě Českých písňových textů. Porovnáváme kval- itu několika generativních jazykových modelů. Pro důkladné zhodnocení a analýzu jejich kvality zavádíme několik automatických metrik a bereme v úvahu i výsledky od lidských hodnotitelů. Zjistili jsme, menší natrénované modely mají lepší výsledky než větší ne- natrénované modely.. Kromě toho je pro kvalitní generování coververzí důležitý kontext. Nakonec ukazujeme, že k našemu úkolu lze přistupovat jak prostřednictvím přístupu založeném na překladu, tak prostřednictvím generativních modelů. 1 Klíčová slova: zpracování přirozeného jazyka|generování textu|literární NLP|strojový překlad; natural language processing|text generation|literary NLP|machine translation Plné texty jsou dostupné v digitálním repozitáři NUŠL Generování textů českých coververzí anglických písní

This thesis explores the topic of generating Czech lyrics to English cover songs. Songs are often adapted to different languages to make them more available to people who do not necessarily speak the ...

Štěpánková, Barbora; Rosa, Rudolf; Mareček, David
Univerzita Karlova, 2024

Generování proteinových sekvencí s danou charakteristikou
Hrbáň, Hugo; Hoksza, David; Lokoč, Jakub
2024 - český Proteins are essential for life as they play a fundamental role in many biological processes. Designing novel proteins with a desired function is an important problem in drug development and biological research. Large databases of protein sequences can be used to train large language models adapted from natural language processing on the language of proteins, written in the alphabet of amino acids. In this work, we demonstrate how large language models based on pretrained deep neural networks can be effectively finetuned for controllable generation of protein sequences from several distinct protein families. Using bioinformatic and deep learning-based methods, we show that the model is able to generate high-quality protein sequences that exhibit low similarity to existing proteins. Proteiny jsou nezbytné pro život, protože hrají zásadní roli v mnoha biologických procesech. Navrhování nových proteinů s požadovanou funkcí je důležitým problémem ve vývoji léků a biologickém výzkumu. Velké databáze proteinových sekvencí lze použít k trénování velkých jazykových modelů převzatých ze zpracování přirozeného jazyka na řeči proteinů zapsané v abecedě aminokyselin. V této práci demonstrujeme, jak lze velké jazy- kové modely založené na předtrénovaných hlubokých neuronových sítích efektivně vyladit pro kontrolovatelné generování proteinových sekvencí z několika odlišných proteinových rodin. Pomocí bioinformatických metod a metod založených na hlubokém učení ukazu- jeme, že model je schopen generovat vysoce kvalitní proteinové sekvence, které vykazují nízkou podobnost s existujícími proteiny. Klíčová slova: bioinformatika|velké jazykové modely|proteinové inženýrství; bioinformatics|large language models|protein engineering Plné texty jsou dostupné v digitálním repozitáři NUŠL Generování proteinových sekvencí s danou charakteristikou

Proteins are essential for life as they play a fundamental role in many biological processes. Designing novel proteins with a desired function is an important problem in drug development and ...

Hrbáň, Hugo; Hoksza, David; Lokoč, Jakub
Univerzita Karlova, 2024

Návrh LLM promptu pro iterativní data exploraci
Fromm, Mikoláš; Petříček, Tomáš; Nečaský, Martin
2024 - český Klíčová slova: velký jazykový model|LLM prompting|iterativní data explorace|asistované generování dotazů|porovnání promptovacích strategií; large language model|LLM prompting|iterative data exploration|assisted query generation|prompting strategies comparison Plné texty jsou dostupné v digitálním repozitáři NUŠL Návrh LLM promptu pro iterativní data exploraci

Fromm, Mikoláš; Petříček, Tomáš; Nečaský, Martin
Univerzita Karlova, 2024

Srovnání stravování pracovníků v třísměnném provozu ve zdravotnictví vs. doporučení Zdravá třináctka
Hladíková, Barbora; Starnovská, Tamara; Vojtová, Markéta
2024 - český Klíčová slova: Třísměnný provoz; směnný provoz; stravování; stravovací návyky; stravovací režim; zdravotníci; výživová doporučení; stravovací návyky; výživa; třísměnný provoz; zdraví; Three-shift operation; shift operation; diet; dietary habits; dietary regime; health; health professionals; nutritional recommendations; dietary habits; nutrition; three- shift operation; health Plné texty jsou dostupné v digitálním repozitáři NUŠL Srovnání stravování pracovníků v třísměnném provozu ve zdravotnictví vs. doporučení Zdravá třináctka

Hladíková, Barbora; Starnovská, Tamara; Vojtová, Markéta
Univerzita Karlova, 2024