|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which nonterminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs.
|
|
|
Jízdní dynamika traktoru
Renza, Jaroslav ; Bradáč, Albert (oponent) ; Panáček, Vladimír (vedoucí práce)
Tato diplomová práce se zabývá rozborem jízdní dynamiky traktorů v závislosti na jejich hmotnosti a stáří. V úvodní části se práce zabývá stručnou historií vývoje a teoreticky definuje základní koncepci rozboru traktoru. Dále práce obsahuje postupy při zjišťování jednotlivých veličin potřebných k určení jízdní dynamiky. Experimentální část rozebírá průběh realizovaného měření na vybraném vzorku traktorů a interpretuje naměřené hodnoty. Závěrečná analogie se zabývá vyhodnocením provedeného měření a údajů z těchto měření zjištěných.
|
|
|
Knihovna pro zpracování obrazu v GPU
Čermák, Michal ; Španěl, Michal (oponent) ; Smrž, Pavel (vedoucí práce)
Tato práce se zabývá architekturou grafických karet Nvidia a s ní související programátorské rozhranní CUDA, které je využito při tvorbě knihovny akcelerující algoritmy zpracování obrazu. Velký důraz je kladen na testování výkonnostního zisku oproti optimalizované a používané knihovně OpenCV.
|
|
|
Překladač pro platformu EdkDSP
Baručák, Robert ; Dolíhal, Luděk (oponent) ; Masařík, Karel (vedoucí práce)
Cílem bakalářské práce bylo vytvoření překladového systému pro platformu EdkDSP. Prezentovány jsou dva odlišné přístupy ke konstrukci překladového systému určeného pro multiprocesorovou platformu. Práce je založená na překladačové infrastruktuře LLVM. Výsledkem jsou dvě funkční verze překladového systému, které generují kód využívající všechny hardwarové prostředky poskytované cílovou platformou. Vytvořená řešení mají sadu omezení, která jsou diskutována v textu práce.
|
|
|
Akcelerace neuronových sítí v FPGA
Krčma, Martin ; Vašíček, Zdeněk (oponent) ; Kaštil, Jan (vedoucí práce)
Tato práce se zabývá problematikou akcelerace výpočtu neuronových sítí skrze jejich implementaci v programovatelných hradlových polích FPGA. Práce představuje dvě různé hardwarové implementace neuronových sítí, které porovnává mezi sebou a s volně dostupnou softwarovou implementací. Dále práce představuje nástroje usnadňující VHDL implementaci neuronových sítí.
|
|
|
Akcelerace RSA na GPU
Balogh, Tomáš ; Jaroš, Jiří (oponent) ; Vašíček, Zdeněk (vedoucí práce)
Tato bakalářská práce se zabývá implementací obecného algoritmu RSA prostřednictvím Montgomeryho násobení pro grafické karty. Pro vybranou platformu CUDA jsou vytvořeny čtyři verze implementace s cílem dosáhnutí co nejvyššího zrychlení výpočtu v porovnání s výpočtem na procesoru. Zrychlení výpočtu je kromě jiného dosaženo paralelizací aritmetických operací sčítání a násobení velkých čísel.
|
|
| |
|
|
Akcelerace šifrovacích algoritmů pomocí FPGA
Gajdoš, Miroslav ; Kaštil, Jan (oponent) ; Šimek, Václav (vedoucí práce)
Tato práce se zabývá možností akcelerace šifrovacích algoritmů pomocí rekonfigurovatelných obvodů FPGA a zkoumáním rozdílu rychlosti implementace oproti implementaci softwarové. Práce popisuje základy šifrování a akcelerace algoritmů na FPGA. Dále se zabývá procesem návrhu, implementace, simulace a syntézy výsledné implementace. Provádí rozbor dosaženého řešení. Cílem projektu bylo vytvořit funkční řešení akcelerovaného algoritmu, tím umožnit jeho další použití v reálném provozu a dále vytvoření česky psaného materiálu o této problematice.
|
|
|
Hardwarová akcelerace šifrování síťového provozu
Novotňák, Jiří ; Kořenek, Jan (oponent) ; Žádník, Martin (vedoucí práce)
Cílem této práce je navrhnout a implementovat vyskorychlostní šifrátor síťového provozus propustností 10Gb/s v jednom směru. Implementační platformou je FPGA Xilinx Virtex5vlx155t umístěné na kartě COMBOv2-LXT. Šifrování je založeno na algoritmu AESs použitím 128 bitového klíče. Zabezpečený protokol je použit ESP pracující nad protokolem IPv4. Design je plně syntetizovatelný nástrojem Xilinx ISE 11.3, bohužel se jej však nepodařilo prakticky otestovat na reálném hardware. Úspěšné testy byly provedeny v simulaci.
|
|
|
Akcelerace heuristických metod diskrétní optimalizace na GPU
Pecháček, Václav ; Jaroš, Jiří (oponent) ; Pospíchal, Petr (vedoucí práce)
Práce se zabývá řešením diskrétních optimalizačních úloh. Zaměřuje se na zkrácení doby výpočtu s využitím heuristických metod a paralelismu. Teoretický základ tvoří kombinace algoritmů ant colony optimization (ACO) a lokálního prohledávání k-optimization. Platformu použitou při implementaci pak představuje technologie Nvidia CUDA umožňující efektivní provádění obecných výpočtů na moderních grafických čipech. Návrh využívá případové studie v podobě známého problému obchodního cestujícího (TSP). Řešení je založeno na rozdělení úlohy na podproblémy s pomocí techniky tour-based partitioning, paralelním zpracování jednotlivých částí a jejich opětovném spojení. Vytvořený paralelní kód dokáže provádět výpočet více než sedmnáctkrát rychleji než jeho sekvenční verze.
|
host ::
RSS.