|
|
The roof structure of the industrial hall in Kyjov
Nosková, Nela ; Pilgr, Milan (referee) ; Šmak, Milan (advisor)
The Bachelor´s thesis describes design and static assessment of the main roof structure supporting elements of the roof structure of the industrial hall in Kyjov. The hall is designed from timber. The aisle is rectangular floor plan 17,0 x 40,0 m. The main bearing structure causes as a frame truss supported by columns. Solid frame is made from solid timber C24. Purlin is designed from solid timber C24. The static calculation also includes fire resistance reports of single elements. Static analysis has been accomplished by student version of the SCIA Engineer 2012 software.
|
|
|
Dynamic analysis of railway bridge
Mojrová, Martina ; Vlk, Zbyněk (referee) ; Nevařil, Aleš (advisor)
The content of work is to determine modal characteristics of bridge construction over the Dyje river near Břeclav. That is done in ANSYS software and AxisVM software. These characteristics are compared with results from dynamic loading test and they are compared between themselves. In thesis is also an assessment of response to static traffic loads because of decision about dynamic analysis necessity. Then there is a simulation of dynamic traffic loads and results of this simulation are compared with results of dynamic analysis which was done by the project. The aim is to do a few static and dynamic tasks and compare results with the real dynamic test and with calculated results and to determinate the effect on certain variables.
|
|
|
Equivalence-Based Slicing of Programs
Malecová, Tatiana ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je navrhnúť metódu, ktorá zjednoduší dva porovnávané programy na základe výsledkov ich sémantickej analýzy. Cieľom je odstránenie čo najväčšieho množstva sémanticky ekvivalentných častí porovnávaných programov. Pre nájdenie týchto ekvivalentných častí aplikujeme vlastné riešenie problému nájdenia najväčšieho spoločného indukovaného podgrafu. Následne sme schopní zjednodušiť programy využitím spätného statického prerezávania. Aplikáciou tohto zjednodušenia získame prerezané programy, ktoré obsahujú rozdielne časti a časti programov, ktoré môžu tieto rozdiely ovplyvniť. Táto metóda je naimplementovaná ako rozšírenie nástroja DiffKemp, čo je statický analyzátor sémantických rozdielov medzi rôznymi verziami rozsiahlych programov. Experimenty vykonané na jadrách Linux-u ukazujú, že metóda je schopná veľmi efektívne vyprodukovať korektné prerezané programy (analýza sa predĺžila len o 3.2%). Navyše, vzniknuté prerezané programy sú omnoho menšie, ako originálne, čo ich činí vhodnými pre ďalšiu analýzu.
|
|
|
Analysis of C Programs with Dynamic Linked Data Structures
Šoková, Veronika ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
This master's thesis deals with the analysis of dynamic linked data structures using shape analysis used in the Predator tool. It describes the chosen abstract domain for heap representation - symbolic memory graphs. It deals with the design of framework for the development of static analyzers based on Clang/LLVM. The main contribution is implementing and testing LLVM's transformation passes that simplify the LLVM IR. Second contribution is the optimization of parameters for parallel run of several variants of the Predator tool. Parameters are tuned for benchmark from SV-COMP'16, where our tool won gold medal in Heap Data Structures category. Last contribution is the design of verification core with the focus on the SMG domain.
|
|
|
Detection of Expressions with Undefined Behavior in C Language
Hellebrandt, Lukáš ; Vojnar, Tomáš (referee) ; Müller, Petr (advisor)
Práce se zabývá detekcí nedefinovaného chování v programech v jazyce C. Zaměřujemese na nedefinované chování vznikající nesprávnou prací se sekvenčními body a vedlejšími efekty. Provedeme teoretický rozbor a pojmy jako nedefinované chování nebo vedlejší efekt zasadíme do kontextu práce. Dále vysvětlíme nebezpečnost konstrukcí vedoucích k nedefinovanému chování. Navrhneme metodu pro automatickou detekci zmíněného druhu nedefinovaného chování. Nakonec navrhneme a implementujeme nástroj pro jeho automatizovanou statickou detekci a popíšeme principy funkce tohoto nástroje. Při jeho návrhu klademe, narozdíl od současných řešení, důraz na funkčnost i v případě přístupu k paměti přes ukazatel nebo z volané funkce. Práce obsahuje příklady nebezpečných konstrukcí, na některých z nich jsou demonstrovány funkce vytvořeného nástroje.
|
|
|
Static Analysis of Java Programs
Vyvial, Pavel ; Hýsek, Jiří (referee) ; Křena, Bohuslav (advisor)
The project SHADOWS has started research which is developing software for automatic bug healing. We work with self-healing software, which looks for concurrent bugs. If the~detection software finds a bug, the healing action will be performed. After every healing action, one would like to know whether this action has fixed the detected problem and, perhaps even more importantly, that it has not caused any other, possibly even more serious, problem. Therefore this paper describes a technique which gives the answer for this question after automatical healing. One can fix some concurent bugs by adding healing locks. One does healing assurance by searching monitorenter instruction and uses Control Flow Graph analysis over Java byte-code. The prototype uses static analysis (tool FindBugs) for this purpose.
|
|
|
Model of a prefabricated footbridge for teaching
Gaidos, Daniel ; Koláček, Jan (referee) ; Strnad, Jiří (advisor)
The subject of this thesis was to design a test model of a foot bridge built out of sets of blocks, coupled by prestressing monostrands into one beam. Created model will serve as a test model during the training of machinists on tensioning equipment. Static model for results from load cases was created in Scia Engineering 20.0. Assessment and dimensioning were solved in the MS Excel program. The structure was assessed for the limit state of load-bearing capacity and serviceability. Analysis and calculations are compliant to up-to-date codes and respect the fundamentals of analysis due to limit states.
|
|
|
Automatic Comparison of Static Analysis Outputs on Different Versions of Programs
Kompová, Radmila ; Müller, Petr (referee) ; Vojnar, Tomáš (advisor)
This thesis aims at development of a tool support for comparing the output of static analysis applied to different versions of program source codes. The thesis also comprises a discussion of three opensource static analyzers of the C source code. Based on this discussion, one of these analyzers, Cppcheck, was chosen for the implementation of the designed tool. The static analyzer's outputs, obtained for various versions of a specific program, are compared on the basis of the context of the line at which an error was found. The patch utility is used for comparing the appropriate contexts. Detected errors are classified into three groups: new, old, and fixed errors. A web interface allowing an easier-to-follow presentation of the results is also provided. The designed tool set has been successfully tested on three opensource projects, including the Linux kernel, Coreutils and CPython.
|
|
|
Multiplatform Linux Sandbox for Analyzing IoT Malware
Uhříček, Daniel ; Burget, Radek (referee) ; Kolář, Dušan (advisor)
Analýza IoT malwaru je problematická zejména pro množství a rozlišnost architektur procesorů používaných IoT zařízeními. Práce shrnuje možnosti statické, dynamické a síťové analýzy Linuxového malwaru a hodnotí existující open source řešení oddělených běhových prostředí pro automatizovanou analýzu. Práce navrhuje modulární, rozšířitelný systém s~jednoduchými možnostmi nasazení, dostupnou API a webovým rozhraním. Výsledná implementace podporuje pět architektur a byla testována na vzorcích IoT malwaru.
|
|
|
Survey and Assessment of Masonry Buildings before Modernization
Stanislav, Štěpán ; Kocáb, Dalibor (referee) ; Cikrle, Petr (advisor)
This thesis deals with the exploration and evaluation of historic masonry building. The researched building was built in the 20th 20th century. Is located in the premises of the Philosophical Faculty of Masaryk University in Brno. During preparation for the planned modernization of the survey was conducted several objects of the university complex. In this work, however, we consider only the building named "C". It will be processed by selected diagnostic method. The findings will then serve as a basis for static analysis and follow-up activities associated with modernization.
|
guest ::
