Yes (9146)
Number of found documents:
9146
Published from
to
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 ...
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 ...
Základní vlastnosti víceúrovňových metod
Minarovičová, Anna Marie; Papež, Jan; Pultarová, Ivana
2024 - English
Multigrid methods are among the most effective iterative methods for the numerical solution of partial differential equations (PDEs). In the thesis, we consider Poisson's equation as the model problem and present its discretization by the finite difference method. Discretization of PDEs gives typically large algebraic systems of linear equations. Various iterative methods can struggle to find an enough accurate approximation within the allocated time. In particular, relaxation methods such as Jacobi or Gauss-Seidel effectively reduce oscillating parts of the error but are inefficient in reducing smooth error components. Multigrid methods combine relaxation methods with correction on a coarser grid to overcome this deficiency. The problem discretized on a coarser grid is smaller and easier to solve. Typically, a recursive error correction is considered using a hierarchy of grids until the coarsest problem is small enough to get a solution quickly by a direct solver. The purpose of this thesis is to discuss the main principles and thoughts behind the multigrid methods, alongside some practical examples and numerical experiments. Víceúrovňové metody patří mezi nejefektivnější iterační metody pro numerické ře- šení parciálních diferenciálních rovnic (PDR). V práci uvažujeme jako modelový problém Poissonovu rovnici a její diskretizaci metodou konečných diferencí. Obecně diskretizace PDR vede na velké soustavy lineárních rovnic. Různé iterační metody mohou mít potíže s nalezením dostatečně přesné aproximace v daném čase. Zejména relaxační metody, jako je Jacobi nebo Gauss-Seidel, účinně redukují oscilující části chyby, ale jsou neefektivní v redukci hladkých chybových složek. Multigridní metody kombinují relaxační metody s korekcí na hrubší síti, aby překonaly tento nedostatek. Problém diskretizovaný na hrubší síti je menší a snáze řešitelný. Oprava na hrubší síti se obvykle realizuje rekurzivně pomocí hierarchie sítí, dokud nejhrubší problém není dostatečně malý na to, aby jej bylo možné řešit přímým řešičem. Cílem této práce je diskutovat hlavní principy a myšlenky, které stojí za multigridními metodami, spolu s některými praktickými příklady a numerickými experimenty.
Keywords:
víceúrovňové metody|numerické metody|řešení soustav lineárních rovnic|hierarchie diskretizací; multigrid methods|numerical methods|solution of linear algebraic systems|discretization hierarchy
Available in a digital repository NRGL
Základní vlastnosti víceúrovňových metod
Multigrid methods are among the most effective iterative methods for the numerical solution of partial differential equations (PDEs). In the thesis, we consider Poisson's equation as the model problem ...
Parametrické modelování rozptylu v odhadu metodou přípustných nejmenších vážených čtverců
Dávidík, Filip; Hudecová, Šárka; Cipra, Tomáš
2024 - English
This thesis explores the implications of heteroscedasticity in regression models, where the variance of errors is not constant across observations. Traditional estimators such as Ordinary Least Squares (OLS) rely on the assumption of homoscedasticity, but real-world data often deviate from this ideal. In response, Weighted Least Squares (WLS) estima- tion is introduced to address known forms of heteroscedasticity, alongside the Feasible Weighted Least Squares (FWLS) estimation method, which only requires partial knowl- edge of heteroscedasticity's form. The theoretical contribution establishes the efficiency of the WLS over the OLS under known heteroscedasticity, and the introduction of the FWLS as a viable alternative. Simulation studies further illustrate the nuanced behavior of the FWLS estimators, offering a comprehensive comparison of the various candidate FWLS estimators under varying model specifications (including misspecified variance models) and insights into their performance relative to the OLS estimator. Recommen- dations are provided to guide method selection based on specific model characteristics, highlighting the importance of accounting for heteroscedasticity in empirical research. 1 Tato práce zkoumá důsledky heteroskedasticity v regresních modelech, kde rozptyl chyb není konstantní napříč pozorováními. Tradiční odhady jako jest Metoda nejmenších čtverců (OLS) se spoléhají na předpoklad homoskedasticity, avšak reálná data často od- chylují od tohoto ideálu. V reakci na to je představen odhad metody vážených nejmenších čtverců (WLS), který se zabývá známými formami heteroskedasticity. Společně s metodou WLS zavádíme odhad přípustnými váženými nejmenšími čtverci (FWLS), který vyžaduje pouze částečné znalosti formy heteroskedasticity. Teoretická část uvede vyšší efektivitu WLS odhadu ve srovnání s OLS odhadem, je-li známá forma heteroskedasticity, přičemž zavádí FWLS odhad jako alternativu k WLS odhadu. Simulační studie dále ilustrují změnu chování FWLS odhadů a jejich komplexní srovnání při různých specifikacích mod- elů (včetně nesprávně specifikovaných modelů rozptylu) a poznatky o jejich výkonu ve srovnání s odhadem OLS. Nakonec je poskytnuto doporučení pro výběr metody na zák- ladě konkrétních charakteristik modelu, zdůrazňující důležitost zohlednění heteroskedas- ticity v empirickém výzkumu. 1
Keywords:
Heteroskedasticita|Regrese|Vážené nejmenší čtverce|Nejměnší čtverce|Přípustné vážené nejmenší čtverce; Heteroscedasticity|Regression|Weighted least squares|Ordinary least squares|Feasible weighted least squares
Available in a digital repository NRGL
Parametrické modelování rozptylu v odhadu metodou přípustných nejmenších vážených čtverců
This thesis explores the implications of heteroscedasticity in regression models, where the variance of errors is not constant across observations. Traditional estimators such as Ordinary Least ...
Divoká binární segmentace
Lasota, Jakub; Pešta, Michal; Maciak, Matúš
2024 - English
The goal of this work is to describe some (multiple) change-point detection methods that aim to estimate the total number and locations of structural changes in the data. From the variety of all change-point detection methods, only binary segmentation and wild binary segmentation are explained. To enhance the understanding, the work contains a few illustrative examples that try to show the strengths and weaknesses of each method. The practical part of the work focuses on using and comparing both methods with various parameter choices on daily logarithmic returns of the Zoom Video Communications stock. 1 Cílem této práce je popsat a vysvětlit několik metod pro detekci bodů změny, které se snaží odhadnout celkový počet a polohy strukturálních změn v datech. Z rozsáhlé škály dostupných metod se soutředíme pouze na konkrétní dvě, binární segmentaci a divokou binární segmentaci. Pro lepší pochopení obsahuje práce také několik ilustračních příkladů, které se snaží ukázat výhody a nevýhody každé z metod. Praktická část práce se soustředí na použití a porovnání obou metod v závislosti na volbě parametrů na denních logaritmických výnosech akcií společnosti Zoom Video Communications. 1
Keywords:
více bodů změny|detekce bodů změny|binární segmentace|randomizované algoritmy|informační kritérium; multiple change-points|change-point detection|binary segmentation|randomised algorithms|information criterion
Available in a digital repository NRGL
Divoká binární segmentace
The goal of this work is to describe some (multiple) change-point detection methods that aim to estimate the total number and locations of structural changes in the data. From the variety of all ...
Testování aktivace organických molekul pomocí difrakce pomalých elektronů.
Cigániková, Nikola; Kocán, Pavel; Albons Caldentey, Llorenc
2024 - English
Self-assembled organic molecules promise a wide range of applications in many fields such as organic chemistry, nanotechnology or molecular electronics. The goal of this thesis is to create covalent bonds in self-assembled structures that could be later used in the field of 2D superconductors. To create these bonds even on surfaces without catalytic properties, the Radical Deposition Source (RDS) has been constructed. In a student faculty grant we created a modified version of the RDS, which we test in this thesis by the means of low- energy electron diffraction in UHV conditions. As the substrate for deposited molecules, we use the surface of Si(111)-In √ 3× √ 7 reconstruction with reported superconducting properties. We show that there are no diffraction spots that would correspond to activated molecules retrieved by the modified RDS. There are multiple explanations with not enough evidence to support any of them, however, this means that the issue is more complex. Understanding why the modified RDS did not work could aid with understanding the whole concept of self-assembled structures bonded covalently and could therefore contribute to the general knowledge of this phenomenon. 1 Samousporiadané molekuly predstavujú široké spektrum možností využitia v rôznych oboroch, ako je napríklad organická chémia, nanotechnológie alebo molekulárna elektronika. Ciel'om tejto práce je vytvorenie kovalentných v̈azieb v samousporiadaných štruktúrach, ktoré by mohli byt' neskôr použité v ob- lasti 2D supravodičov. Pre vytvorenie takýchto štruktúr aj na povrchoch bez vhodných katalytických vlastností bol skonštruovaný Radical Deposition Source (RDS). V študentskom fakultnom grante sme vyrobili modifikovanú verziu RDS, ktorú v tejto práci testujeme metódou difrakcie pomalých elektrónov v podmien- kach UHV. Ako substrát pre deponované molekuly sme použili povrch Si(111)- In √ 3 × √ 7 rekonštrukcie so zdokumentovanými supravodivými vlastnost'ami. Z práce vyplýva, že neboli pozorované žiadne difrakčné body, ktoré by mohli korešpondovat' s molekulami aktivovanými modifikovaným RDS. Vysvetlení sa ponúka viacero, pre žiadne z nich však nemáme dostatočné dôkazy, čo naz- načuje, že táto problematika je ovel'a komplexnejšia. Porozumenie dôvodu, prečo modifikovaný prístroj RDS nefungoval, by mohlo pomôct' s pochopením celého konceptu samousporiadaných štruktúr spojených kovalentnými v̈azbami, a tým pádom prispiet' všeobecnej...
Keywords:
samousporiadanie|aktivácia molekúl|difrakcia pomalých elektrónov|rekonštrukcie povrchov|kremík; self-assembly|molecular activation|low-energy electron diffraction|surface reconstructions|silicon
Available in a digital repository NRGL
Testování aktivace organických molekul pomocí difrakce pomalých elektronů.
Self-assembled organic molecules promise a wide range of applications in many fields such as organic chemistry, nanotechnology or molecular electronics. The goal of this thesis is to create covalent ...
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