|
|
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.
|
|
|
Analysis of structural and proportional criteria of Romanesque and Pre-Romanesque rotundas.
Kříž, Pavel ; Kalousek, Lubor (referee) ; Unger,, Josef (referee) ; Vlček, Milan (advisor)
Topic of this dissertation thesis follows previous dissertations dealing with reconstructions of historical buildings that were successfully defended at Institute of Building Structures, Faculty of Civil Engineering, Brno University of Technology. The thesis deals with Romanesque and Pre-Romanesque round churches, called rotundas, that were built between 9th and 13th century in the historical territory of Great Moravia. Churches of similar shape can be also found in surrounding countries, but only scarcely. By the time of origin these rotundas were among the oldest masonry buildings built within borders of contemporary Czech Republic. Later some rotundas were destroyed and are known only thanks to the archaeological findings or written records. Some are still waiting to be discovered. Surviving rotundas are the oldest masonry buildings in Czech Republic, therefore it can be said that they belong to the most valuable historical buildings in the country. Preserved rotundas were often modified or rebuild in some way. Thanks to their age, origins of many of these buildings are shrouded in a mystery, which is one of the reasons why they attract attention of many researchers – archaeologists, historians and art historians. Many questions arise from their research. These questions have interdisciplinary character and finding the answers requires cooperation of specialists in different fields. One of these fields is building engineering. This dissertation thesis deals with proportional and structural analysis of Pre-Romanesque and Romanesque rotundas. For the proportional analysis author focused on verifying of some of the hypotheses of other researchers connected to the Romanesque rotundas. These include hypothesis dealing with use of historical units for the design of rotundas, hypothetical use of proportional canon, or some universal sets of proportional ratios of vertical and horizontal dimensions. The proportional analysis also helped with verification of some hypothe
|
|
|
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.
|
|
|
Static Analysis Using Facebook Infer to Find Atomicity Violations
Harmim, Dominik ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.
|
|
|
Automatic Generation of Test Cases from Data-Flow
Kraut, Daniel ; Fiedor, Tomáš (referee) ; Smrčka, Aleš (advisor)
This thesis deals with automatic generation of test cases on Unit testing level for source codes in C language. In order to achieve automatization are used methods of approach to software as a Data-flow of variables. There is outlined a process of creating tests here as well as a function of CSP solvers which are necessary part of solving this problems. Static code analysis is accessed with LibTooling libraring as part of a compiler front-end project Clang. Output of a developed application are provided here which is automatically generated input values for test cases.
|
|
|
Design of bridge on the motorway D48
Holuša, Adam ; Nováček, Jan (referee) ; Zich, Miloš (advisor)
Diploma thesis deals with design of a new bridge on motorway D48 located on bypass of Frýdek – Místek. Total spread of the bridge is 113 meters. Thesis includes 3 studies. For next assesment was chosen concrete girder box construction with 3 spans. Bridge is bulit on falsework. Structural analysis includes influences of construction by TDA method. Load effect is solved in Scia Engineer 18.0. The assessment of the bridge was made according to EC.
|
guest ::
