|
|
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ů.
|
|
| |
|
|
Statická analýza zastřešení sportovní haly
Meissnerová, Sabina ; Hokeš, Filip (oponent) ; Vlk, Zbyněk (vedoucí práce)
Diplomová práce se zabývá statickou analýzou zastřešení sportovní haly. Výpočtový model byl dle poskytnutých podkladů vytvořen ve výpočetním programu Dlubal RFEM 6.04. Bylo provedeno zatížení dle platných norem a konstrukce posouzena na mezní stav únosnosti a pevnosti. Ruční výpočty posouzení byly porovnány s programem. V diplomové práci je řešen ruční výpočet vnitřních sil na zaobleném nosníku od vlastní tíhy konstrukce a stabilita konstrukce demonstrována nejprve na jednostranně vetknutém nosníku poté na vytvořeném prostorovém modelu.
|
|
|
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.