|
|
Administrativní budova
Luža, Radim ; Šulák, Pavel (oponent) ; Jeneš, Rostislav (vedoucí práce)
Tato bakalářská práce se zabývá statickou analýzou a posouzením železobetonové stropní desky nad prvním nadzemním podlažím administrativní budovy. Stropní konstrukci tvoří monolitická lokálně podepřená deska. Statická analýza byla provedena pomocí softwaru Scia Engineer 14. Pro ověření výpočtu bylo užito stejného softwaru, kde nebyla vymodelována deska, ale dva na sebe kolmé rámy. Následně bylo provedeno dimenzování na mezní stav únosnosti. Z hlediska mezního stavu únosnosti byly vyšetřovány hlavně ohybové momenty a protlačení. Dále bylo provedeno posouzení druhého mezního stavu, tedy použitelnosti. U druhého mezního stavu bylo vyšetřováno hlavně omezení vzniku trhlin. Na základě statické analýzy a posudků na jednotlivé mezní stavy byla zhotovena výkresová dokumentace obsahující spodní a horní výztuž včetně protlačení.
|
|
|
Dynamická analýza ocelových nádrží s kapalinou
Farkasová, Zuzana ; Mrózek, Michal (oponent) ; Hradil, Petr (vedoucí práce)
Diplomová práce řeší dynamickou analýzu ocelových nádrží s kapalinou. V práci jsou uvedeny parametry konstrukce a způsob jejich zpracování v programovém systému ANSYS. Pro srovnání jsou vytvořeny tři výpočtové modely, pro které je vypočtena statická a modální analýza. Spektrální analýza je provedena pouze pro výpočtové modely s kapalinovým prostředím. Páce uvádí také posudky skořepinových prvků dle Eurokódu 3.
|
|
|
Statická detekce častých chyb JBoss aplikačního serveru
Vyvial, Pavel ; Rogalewicz, Adam (oponent) ; Letko, Zdeněk (vedoucí práce)
Práce si klade za úkol poskytnout čtenáři popis statické analýzy prováděné prostřednictvím nástroje FindBugs nad aplikačním serverem JBoss od společnosti Red Hat. Na základě analýzy vybraných chyb byly vytvořeny vzory pro jejich detekci, které byly následně naimplementovány jako zásuvné moduly statického analyzátoru FindBugs (tzv. detektory). Vytvořené detektory byly otestovány na vývojové verzi JBoss aplikačního serveru a výsledky jsou publikovány v závěru práce.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
|
Využití optimalizačních metod při navrhování strojních součástí
Kubrický, Daniel ; Pokorný, Přemysl (oponent) ; Zeizinger, Lukáš (vedoucí práce)
Tato bakalářská práce popisuje využití metod strukturální optimalizace při navrhování strojních součástí. V první části práce byl proveden popis současného stavu poznání procesu optimalizačních úloh společně s jeho teoretickými východisky. V druhé části práce byla vytvořena statická analýza a topologická optimalizace nebo Generativní design na příkladu vahadla v šesti komerčních software. V třetí části byly mezi sebou porovnány výsledné modely jednotlivých software a byly srovnány výsledky pomocí kritéria maximálního napětí von Mises a celkové deformace modelu. Na závěr této práce bylo provedeno vyhodnocení použití software pro strukturální optimalizaci.
|
|
|
Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Svobodová, Lucie ; Fiedor, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Modern software systems often use concurrent programs to improve performance and increase efficiency. However, ensuring the reliability and safety of such systems can be challenging due to the increased potential for bugs, including data races, to arise. In this thesis, we introduce a new static data race detector, DarC, designed for programs written in C using the Pthreads library. The proposed detector is implemented as an analyser plugin in Meta Infer, a static analysis framework with an emphasis on compositional, incremental, and consequently highly-scalable analysis. Our approach involves recording a set of accesses that occur in the analysed program along with information about the set of locks held during these accesses. The tool then identifies pairs of accesses that may lead to data races and reports them to the user. Our tool was successfully evaluated on a set of benchmarking programs as well as on real-life projects, showing its potential for effectively detecting data races in C programs.
|
|
|
Detekce komunikace malware v síťových tocích
Korvas, Václav ; Matoušek, Petr (oponent) ; Ryšavý, Ondřej (vedoucí práce)
Tato práce se zabývá problematikou síťové komunikace škodlivého kódu, způsoby jejich analýzy a především srovnáním přesností různých algoritmů strojového učení mezi sebou. Práce přináší srovnání přesnosti jednotlivých algoritmů strojového učení, jak na testovacích datech tak při použití v reálném provozu. Jako metriky pro vyhodnocení výsledků byla použita přesnost, F1-skóre a míra falešné pozitivity. Na testovacích datech se jako nejpřesnější ukázaly algoritmy Random Forest a XGBoost, které dosáhly přesnosti 99.2% s mírou falešné pozitivity 0.6%. Při experimentech v reálném provozu bylo přibližně 9% toků nesprávně detekováno a klasifikováno jako malware. Při napadení počítače pak míra klasifikovaných toků jako malware, vzrostla na 18% a k tomu bylo zachyceno několik indikátorů kompromitace, které toto napadení potvrdily.
|
|
|
Pokročilá statická analýza výkonnosti v nástroji Meta Infer
Pavela, Ondřej ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Looper is a static complexity analysis tool for inference of tight upper bounds on the exe- cution cost of programs. It is based on the previously existing Loopus tool which used abstract program model of difference constraints (inequalities of the form + ), which allows for natural abstraction of common loop counter updates = + + and = + 0. Looper was initially proposed and implemented in author’s bachelor’s thesis as a checker for the Meta Infer framework but the tool failed to meet the expectations when tested on real-world code. This master’s thesis proposes a new improved version of Looper that aims at solving the main limitations of the original tool, namely through introduction of interprocedural analysis. Additionally, various extensions target- ing improved precision of the intraprocedural analysis, such as new abstraction algorithm, handling of compound loop conditions and more, were implemented. Moreover, logging, issue reporting and collection of results has been significantly improved. Finally, through extensive experiments with the new Looper version, the ability to analyze real-world code in a more general, scalable and precise way was shown.
|
|
|
Plugin for a Code Risk Analysis
Kvasnička, Jaroslav ; Lengál, Ondřej (oponent) ; Havlena, Vojtěch (vedoucí práce)
This thesis explores the importance of code analysis and testing and its impact on program functionality and cost. It discusses the basic principles and types of testing, with a focus on static analysis. The Eclipse platform and plugins are also examined, along with the architecture of the target code. We then discussed and implemented an extension of the static MFB analyzer which the BOC-GROUP company developed along with extensions such as the Log4j checker and GDPR analyzer. We also designed and implemented the Eclipse plugin which can highlight the results of the MFB analyzer in the Eclipse IDE. In conclusion, future possible extensions are also discussed, including harmful regular expression detectors and XSS prevention.
|
|
|
Automatické generování šablon změn kódu
Kříž, Daniel ; Vašíček, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
The aim of this thesis is to propose a method for automatic generation of custom code change patterns in LLVM IR language for DiffKemp, a tool for analyzing semantic differences between version of large scale projects. The goal is to enable automatic generation of changes between versions of a project with values, global variables or structure types. This has been achieved by finding the common pattern between changes and then generating its variants, which differ in usage of global variables and types. The proposed solution was implemented as an extension of DiffKemp and our experimentation on small programs shows that out proposed method is able to yield at least partially satisfactory results.
|
host ::
RSS.