|
|
Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti
Harmim, Dominik ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce je navrhnout statický analyzátor, který bude sloužit pro detekci porušení atomicity. Navržený analyzátor Atomer je implementován jako modul pro Facebook Infer, což je volně šířený a snadno rozšířitelný nástroj, který umožňuje efektivní modulární a inkrementální analýzu. Analyzátor pracuje na úrovni sekvencí volání funkcí. Navržené řešení je založeno na předpokladu, že sekvence, které jsou zavolány atomicky jednou, by měly být pravděpodobně volány atomicky vždy. Implementovaný analyzátor byl úspěšně ověřen a vyhodnocen jak na malých programech, vytvořených pro testovací účely, tak na veřejně dostupných testovacích programech, které vznikly ze skutečných nízkoúrovňových programů.
|
|
|
Automatická tvorba testovacích případů z datových toků
Kraut, Daniel ; Fiedor, Tomáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá automatickou tvorbou testovacích případů na úrovni jednotkového testování, pro zdrojové texty v jazyce C. K dosažení automatizace jsou použity metody přístupu k software jako k datovým tokům proměnných. Je zde nastíněn náhled na průběh tvorby testů a funkci CSP solverů, které jsou nezbytnou částí pro rozhodnutelnost těhto problémů. Statická analýza kódu je umožněna knihovnou LibTooling v projektu překladačového front-endu Clang. Jsou uvedeny výstupy z aplikace, jimiž jsou automaticky vytvořené vstupní hodnoty pro testovací případy.
|
|
|
Návrh mostu na dálnici D48
Holuša, Adam ; Nováček, Jan (oponent) ; Zich, Miloš (vedoucí práce)
Diplomová práce se zabývá návrhem mostu na dálnici D48 na obchvatu města Frýdek – Místek. Celkové rozpětí mostu je 113 m. Byly navrženy 3 studie. Pro podrobný návrh byla vybrána varianta monolitického komorového nosníku o 3 polích. Most je betonován na pevné skruži. Do statické analýzy je zahrnut také vliv výstavby pomocí TDA. Posudek je proveden pomocí programu Scia Engineer 18.0. Konstrukce byla posuzována podle platných EC.
|
|
|
Nástroj pro statickou analýzu programů se seznamy
Kotoun, Michal ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tvorba softwarového analyzátoru je komplexní úloha -- je nutno implementovat parsování zdrojového kódu, reprezentaci instrukcí, abstrakci hodnot, uživatelské rozhraní, ... a také analýzu samu. Abychom předešli zbytečné práci vývojářů analýz, rozhodli jsme se vytvořit framework pro statickou analýzu programů. Předkládáme obecný návrh frameworku zvaného Angie s důrazem na jeho použitelnost a popisujeme prototyp frameworku, včetně modelové analýzy založené na symbolických paměťových grafech. Angie je implementován v C++ a používá nástroje z kolekce LLVM pro parsování zdrojového kódu analyzovaných programů.
|
|
|
Topology optimization of movable, fixed and based plate of electromechanical injection-moulding machine
Kecík, Samuel ; Halabuk, Dávid (oponent) ; Návrat, Tomáš (vedoucí práce)
The master thesis deals with the design of geometry of plates of the injection molding unit using the FEM tool Topological Optimization. The reason for this is to reduce the weight of these components, which is beneficial in the transport and assembly of the injection molding machine. However, the final models of geometry of plates must meet certain requirements in terms of the limit state of deformation, the limit state to the critical value of the equivalent stress. This condition involves both limit state of elasticity and limit state of fatigue. Computational modeling and also Topological Optimization are performed in ANSYS Workbench.
|
|
|
Vliv tuhosti spojů na namáhání ocelových prutových konstrukcí
Šik, Jan ; Vlk, Zbyněk (oponent) ; Nevařil, Aleš (vedoucí práce)
Tato bakalářská práce se zaměřuje na analýzu skutečného chování styčníků ocelových prutových konstrukcí. V úvodních kapitolách jsou popsány jednotlivé přístupy k modelování styčníků. První přístup je založen na algoritmech dle norem ČSN EN. Druhý přístup využívá numerický model řešený metodou konečných prvků (MKP) v systému ANSYS. Na závěr je provedeno porovnání výsledků jednotlivých přístupů k modelování styčníků.
|
|
|
Vysokovýklopná lopata
Petro, Roman ; Lžičař, Roman (oponent) ; Škopán, Miroslav (vedoucí práce)
Tato diplomová práce řeší konstrukční návrh vysokovýklopné lopaty pro nakladače New Holand B100 a B110. Úvodem jsou pospány provozní podmínky, přepravovaný materiál a rypadlo-nakladač B100, B110. Jsou zde uvedena možná konstrukční řešení a vlastní konstrukční návrh. Následuje kinematický rozbor vykládání materiálu a statická analýza na lopatě a rámu. Na statickou analýzu navazuje kontrola čepů a pevnostní analýza lopaty i rámu pro různé zatěžovací stavy provedená metodou konečných prvků
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to design and to implement a generic strategy solver to the 2LS tool. 2LS is an analyser for a static verification of programs written in C language. A verified program is analysed by an SMT solver using abstract interpretation. Convertion from an abstract state of the program into a logical formula, that an SMT solver can work with, is done by a component called strategy solver. In the current implementation, there is one strategy solver for each abstract domain. Our approach introduces a single generic strategy solver, which makes creating new domains easier. Also, this approach enables migration of the existing domains and hence the codebase can be reduced.
|
|
| |
host ::
RSS.