|
|
Statická analýza NumPy programů
Zimen, Martin ; Kofroň, Jan (vedoucí práce) ; Blicha, Martin (oponent)
NumPy programy se těžko ladí. Kvůli dynamické povaze Pythonu se chyba často projeví až poté, co program delší dobu běží. Výpočet poté spadne a všechen výpočet je ztracen. Existující nástroje statické analýzy nedokážou poznat chyby specifické pro NumPy. Použili jsme data-flow analýzu zkombi- novanou se symbolickým vykonáváním programu k detekování chyb plynoucí z nevyhovujících tvarů matic. Naše metoda pomocí dynamické množiny sym- bolů sleduje ve vstupním program rozměry matic a vztahy mezi nimi. Ná- sledně pomocí SMT vyhodnotí, jestli jsou vztahy splnitelné, nebo jestli došlo k chybě a kde. Naše implementace rozumí základním NumPy konstrukcím a detekuje některé chyby pro pole a matice.
|
|
|
Federated learning
Georgiu, Martin ; Švarný, Petr (vedoucí práce) ; Blicha, Martin (oponent)
pro práci Federated learning od Martina Georgiu Pokrok v oblasti strojového učení v posledních letech byl bezprecedentní, přesto je stále potřeba stále více dat pro trénování umělých neuronových sítí (artificial neural network, ANN). V sektorech jako je zdravotnictví je velice těžké, většinou nereálné, vytvořit je- den soubor dat, který by konsolidoval všechny pacientské informace z různých nemoc- nic. Proto lze jakékoli trénování ANN provádět výhradně lokálně na datech jedné dané nemocnice. Federativní učení (FL) je nový přístup, který lze v takovém prostředí použít a uchovat tak uživatelská data v soukromí. V této práci porovnáváme FL s jinými přístupy usilujícími o stejný cíl, zaměřujeme se na bezpečnost FL a prozkoumáváme konkrétní strategie pro FL. Nakonec jsme také vytvořili plně funkční open-source ukázku analýzy pih natrénovanou pomocí FL. Tu lze snadno rozšířit a použít i s jinými soubory dat a cíly. 1
|
|
|
Effective Automated Software Verification: A Multilayered Approach
Blicha, Martin ; Kofroň, Jan (vedoucí práce) ; Rümmer, Philipp (oponent) ; Bjørner, Nikolaj (oponent)
V posledních letech automatická formální verifikace software pokročila z několika výzkumných laboratoří do rozsáhlých aplikací, jako je cloudová infrastruktura a smart kontrakty. Formální verifikační techniky založené na technice model checking poskytují nezbytné záruky úplným a automatickým zkoumáním chování systémů. Navíc poskytují svědky (vysvětlení) pro výsledek své analýzy: chybové chování, pokud nějaké existuje, nebo důkaz o absenci takového chování. Obecný problém, který se automatická verifikace software snaží vyřešit, je však nerozhodnu- telný. Navzdory této teoretické překážce je v mnoha případech, které se v praxi vyskytují, docela efektivní. Tento (možná překvapivý) úspěch připisujeme kombinaci faktorů: neutuchajícímu úsilí výzkumníků, kteří přicházejí s novými verifikačními postupy pro třídy problémů, kde existující techniky narážejí na své možnosti; úžasný pokrok v základních technologiích řešení splnitel- nosti, zvláště v Satisfiability Modulo Theories (SMT); a zvýšení dostupného výpočetního výkonu prostřednictvím paralelních a cloudových výpočtů. Nicméně rostoucí složitost systémů v reálném světě představuje nové výzvy pro formální verifikace,...
|
|
|
The continuum function on regular cardinals in the presence of large cardinals
Blicha, Martin ; Honzík, Radek (vedoucí práce) ; Verner, Jonathan (oponent)
V této práci zkoumáme, jak na sebe vzájemně působí velké kardinály a funkce kontinua. Z Eastonova výsledku víme, že funkce kontinua na regulárních kardinálech má v ZFC velkou volnost. Avšak velké kardinály kladou na chování funkce kontinua další omezující podmínky. Vzájemné ovlivňování velkých kardinálů a funkce kontinua se liší pro jednotlivé typy velkých kardinálů. Abychom poukázali na tyto rozdíly, soustředíme se na slabě kompaktní a měřitelný kardinál. Pro srovná- ní také přezkoumáme nepopsatelné kardinály, na kterých ukážeme, že není snadné přesně určit důvod těchto rozdílů. 1
|
|
|
Using Constrained Horn Clauses for Hierarchical Planning
Kažimír, Marián ; Blicha, Martin (vedoucí práce) ; Pantůčková, Kristýna (oponent)
Název práce: Užití omezených Hornových klauzulí pro hierarchické plánování Autor: Marián Kažimír Katedra / Ústav: Katedra distribuovaných a spolehlivých systémů Vedoucí bakalářské práce: Mgr. Martin Blicha, Katedra distribuovaných a spo- lehlivých systémů Abstrakt: HTN plánování je populární způsob jak modelovat plánovací problémy. Cílem této práce je naimplementovat HTN řešič založený na překladu plánovacího problému do problému dosažitelnosti v tranzitním systému a ten následně vyřešit pomocí běžného řešiče dosažitelnosti. Klíčová slova: HTN Plánovací problém řešič Tranzitní systém Omezené Hornove klauzule
|
|
|
Branching loop summarization
Tatarko, William ; Blicha, Martin (vedoucí práce) ; Bednárek, David (oponent)
V této práci představujeme nový algoritmus na sumarizaci cyklů s více větvemi pracujícími s celými čísly. Algoritmus je založen na analýze tzv. stavového diagramu, který zachycuje možné přechody mezi větvemi. Suma- rizace může být použita na nahrazení cyklů ekvivalentními neiterativními příkazy. Toto umožňuje analýzu dosažitelnosti a může být použito na veri- fikaci softwaru. Sumarizace může být také například použita na optimalizace (kompilátorů). 1
|
|
|
Data Lineage Analysis for Qlik Sense
Jurčo, Andrej ; Parízek, Pavel (vedoucí práce) ; Blicha, Martin (oponent)
Počas posledných rokov sa Business Intelligence stala veľmi dôležitou pre všetky spoločnosti a organizácie po celom svete v oblasti rozhodovania a pozorovania dlhodobých trendov. Často sa stáva, že nástroje Business Intelligence sa postupne stanú veľmi zložitými a vykonanie akýchkoľvek zmien je veľmi náročné. Tento problém dokáže riešiť data lineage vizualizáciou dátových tokov a zobrazením vzájomných závislostí. Manta Flow je platforma, ktorá takúto lineage vytvára a podporuje programovacie jazyky (Java, C), databázy (Oracle, MS SQL), či nástroje Business Intelligence (Cognos, Qlik Sense). Cieľom tejto práce bolo implementovať prototyp skenerového modulu pre platformu Manta Flow, ktorý by zanalyzoval dátové toky v Qlik Sense a vytvoril by graf data lineage od dátových zdrojov až po prezentačnú vrstvu. Tento modul extrahuje metadáta potrebné pre analýzu, resolvuje objekty prítomné v danej Qlik Sense aplikácii a analyzuje dátové toky v nich. Výsledný graf data lineage je následne vizualizovaný inými komponentami platformy Manta Flow. 1
|
|
|
Methods for reduction of Craig's interpolant size using partial variable assignment
Blicha, Martin ; Kofroň, Jan (vedoucí práce) ; Kučera, Petr (oponent)
V čase, ktorý ubehol od prvého použitia interpolantov v oblasti symbolického overovania modelov (symbolic model checking), sa metódy založené na interpolantoch s úspechom uplatnili v oblasti overovania hardvéru aj softvéru. Prednedávnom sa v oblasti výpočtu interpolantov objavili čiastočné ohodnotenia premenných. V kontexte takzvaných "abstract reachability graphs" predstavujú čiatočné ohodnotenia spôsob ako sa zároveň elegantne vysporiadať s premennými mimo aktuálny kontext a zároveň dosiahnuť zmenšenie spočítaného interpolantu. V tejto práci sme ďalej rozvinuli systém pre počítanie interpolantov za prítomnosti čiastočných ohodnotení, dokázali sme jeho korektnosť a ukázali sme jeho potenciál pre ďalšie zmenšenie počítaných interpolantov. Nakoniec sme analyzovali za akých podmienok budú mať počítané interpolanty vlastnosť dôležitú pre mnoho techník založených na interpolácií - tzv. path interpolation property. Powered by TCPDF (www.tcpdf.org)
|
|
|
Konstrukce modelů v polynomiální reprezentaci
Blicha, Martin ; Stanovský, David (vedoucí práce) ; Surynek, Pavel (oponent)
Hledání konečných modelů je problém definovaný takto: k dané teorii prvořádové logiky najít její konečný model. V této práci předkládáme nový způsob řešení tohoto problému, který je založen na překladu axiomů na sous- tavu polynomiálních rovnic. Existence modelu dané velikosti je pak ekviva- lentní existenci řešení této soustavy. Ukážeme korektnost tohoto přístupu, implementujeme algoritmus založen na tomto přístupu a porovnáme jeho výkon s aktuálně nejlepšími systémy na hledání modelů. 1
|
|
|
The continuum function on regular cardinals in the presence of large cardinals
Blicha, Martin ; Honzík, Radek (vedoucí práce) ; Verner, Jonathan (oponent)
V této práci zkoumáme, jak na sebe vzájemně působí velké kardinály a funkce kontinua. Z Eastonova výsledku víme, že funkce kontinua na regulárních kardinálech má v ZFC velkou volnost. Avšak velké kardinály kladou na chování funkce kontinua další omezující podmínky. Vzájemné ovlivňování velkých kardinálů a funkce kontinua se liší pro jednotlivé typy velkých kardinálů. Abychom poukázali na tyto rozdíly, soustředíme se na slabě kompaktní a měřitelný kardinál. Pro srovná- ní také přezkoumáme nepopsatelné kardinály, na kterých ukážeme, že není snadné přesně určit důvod těchto rozdílů. 1
|
host ::
RSS.