|
|
Static Analyzer for List Manipulating Programs
Kotoun, Michal ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Creating a software verification tool is a complex task -- one must implement source code parsing, instruction representation, value abstraction, user interface, ... and the analysis itself. Therefore, we decided to create a static analysis framework to prevent unnecessary wheel reinventing by an analyses implementers. We propose a general design of the framework called Angie with a primary focus on usability, and describe a prototype implementation of the framework, including a model analysis based on symbolic memory graphs. Angie is implemented in C++ and uses the LLVM toolchain as the front-end for parsing the source code of analysed programs.
|
|
| |
|
|
Static analysis of the sports hall roof
Meissnerová, Sabina ; Hokeš, Filip (referee) ; Vlk, Zbyněk (advisor)
The final thesis deals with structural analysis of the roofing of the sports hall. Computational model was created in the computational software Dlubal RFEM 6.04 according to the provided documents. The loads were performed in accordance with valid standards and the structure was assessed for the ultimate and serviceability limit state. Manual assessment calculations were compared with the software. The final thesis deals with the manual calculation of internal forces on a curved beam from the self-weight of the structure and the stability of the structure is demonstrated first on a single-sided fixed beam and then on the created spatial model.
|
|
|
Influence of stiffness connections on loading of steel structures
Šik, Jan ; Vlk, Zbyněk (referee) ; Nevařil, Aleš (advisor)
This bachelor thesis focuses on the analysis of the real behavior of the joints in steel structures. The introduction describes different approaches to the modeling of joints. The first approach is based on algorithms found in normative documents ČSN EN. The other approach deals with numerical modeling of the joints using the finite element method (FEM) in SW ANSYS. In conclusion, the comparison of results of different approaches to the modeling of joints.
|
|
|
High loading shovel
Petro, Roman ; Lžičař, Roman (referee) ; Škopán, Miroslav (advisor)
This diploma thesis solves construction project high dumping shovel for back hoe loader New Holland B100 and B110. There are described operating conditions in the introduction, transport material and technical parameters for back hoe loader B100, B110. There are mentioned possible construction’s solutions and own design. Follow the kinematics analysis of material’s dumping and the static analysis on shovel and frame. This is connected with following peg’s control and the solidity analysis of shovel and frame for different load cases, where the MFE was used
|
|
|
Dynamic Data Race Detection and Self-Healing in Java Programs
Letko, Zdeněk ; Kolář, Dušan (referee) ; Vojnar, Tomáš (advisor)
Finding concurrency bugs in complex software is difficult. As a contribution to coping with this problem the thesis proposes an architecture for a fully automated dynamic detection and healing of data races and atomicity violations in Java. Two distinct algorithms for detecting of data races are presented. One of them is a novel algorithm called AtomRace which detects data races as a special case of atomicity violations. The healing is based on suppressing a recurrence of the detected problem and can be performed by introducing an additional synchronization or by legally influencing the Java scheduler. Basically forces certain parts of the code to be executed atomically. The proposed architecture uses bytecode instrumentation to be able to track and influence the execution. The architecture and algorithms were implemented and tested on multiple case studies.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS. 2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovaný program je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab- straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonáva komponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýto solver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbu nových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a teda zmenšuje program analyzátora.
|
|
|
Plan curved arch footbridge
Trenz, Jan ; Romportl, Tomáš (referee) ; Stráský, Jiří (advisor)
The scope of thesis is to design a curved arch footbridge. The main structure consists of composite deck supported by steel arch. The focus is on finding optimal shape of arch and proper cross-sections of elements. Bridge is analysed according to limit states.
|
|
|
Static Analysis of Steel Joints
Vojtek, Jiří ; Kytýr, Jiří (referee) ; Gratza, Roman (advisor)
Elaboration of design principles of steel joints. Creation of the finite element model in ANSYS program, the study of static behaviour near the bolt hole, deformation of the screw and the stress components of the welded joint. Comparison with the analytical formulas.
|
|
| |
guest ::
