|
|
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.
|
|
|
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.
|
|
|
Topology optimization of movable, fixed and based plate of electromechanical injection-moulding machine
Kecík, Samuel ; Halabuk, Dávid (referee) ; Návrat, Tomáš (advisor)
The master thesis deals with the design of geometry of plates of the injection molding unit using the FEM tool Topological Optimization. The reason for this is to reduce the weight of these components, which is beneficial in the transport and assembly of the injection molding machine. However, the final models of geometry of plates must meet certain requirements in terms of the limit state of deformation, the limit state to the critical value of the equivalent stress. This condition involves both limit state of elasticity and limit state of fatigue. Computational modeling and also Topological Optimization are performed in ANSYS Workbench.
|
|
|
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.
|
|
|
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 ::
