|
|
Improvement of Live Variable Analysis Using Points-to Analysis
Raiskup, Pavel ; Rogalewicz, Adam (referee) ; Dudka, Kamil (advisor)
Languages such as C use pointers very heavily. Implementation of operations on dynamically linked structures is, however, quite difficult. This can cause the programmer to make more mistakes than usual. One method for dealing with this situation is to use the static analysis tools. This thesis elaborates on the extension to the Code Listener architecture which is an interface for building static analysis tools. Code Listener is able to construct a call-graph or a control flow graph for a given source code and send it to the analyzing tool. One ability of the architecture is that it can conduct the live variable analysis internally. It detects places in the control flow graph where some subset of variables may be killed. The problem was that every variable for which a pointer address was assigned could not been killed, before. This decision had been made because there was no assurance that the variable could never been used through the pointer. So the goal of this work was to design and incorporate a points-to analysis which is able to exclude some references from the set of considered pointers to improve the live variable analysis.
|
|
|
Static Analysis of Computer Networks
Hozza, Tomáš ; Veselý, Vladimír (referee) ; Ryšavý, Ondřej (advisor)
Some problems in configurations of network devices are difficult to identify. Access control lists present an important part of many configurations. Conflicts among rules of an access control list can cause holes in security policy or quality of service. In this paper we focus on identifying and classifying conflicts among rules of an access control list. Discovering all possible types of conflicts is not a trivial task. We present optimized algorithm for complete access control list analysis using tries, based on existing research by Baboescu and Varghese. The tool for detecting conflicts among access control list rules of one given Cisco, HP or Juniper device using tries based algorithm has been implemented. Bit vectors in tries use WAH compression method to reduce memory consumption. Implemented tool was tested for correctness and performance. The hypothesis that this solution would make the analysis of access lists significantly faster has been proven.
|
|
|
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.
|
|
|
Verification of Pointer Programs Based on Forest Automata
Hruška, Martin ; Rogalewicz, Adam (referee) ; Holík, Lukáš (advisor)
In this work, we focus on improving the forest automata based shape analysis implemented in the Forester tool. This approach represents shapes of the heap using forest automata. Forest automata are based on tree automata and Forester currently has only a simple implementation of tree automata. Our first contribution is replacing this implementation by the general purpose tree automata library VATA, which contains the highly optimized implementations of automata operations. The version of Forester using the VATA library participated in the competition SV-COMP 2015. We further extended the forest automata based verification method with two new techniques - a counterexample analysis and predicate abstraction. The first one allows us to determine whether a found error is a real or spurious one. The results of the counterexample analysis is also used for creating new predicates which are used for the refinement of predicate abstraction. We show that both of these techniques contribute to an improvement over the early approach.
|
|
|
Material nonlinear solution of structures made of plastics
Weis, Lukáš ; Krejsa,, Martin (referee) ; Králík,, Juraj (referee) ; Kytýr, Jiří (referee) ; Němec, Ivan (advisor)
The presented thesis focuses on static analysis of plastic structures, taking into account nonlinear behaviour of the material depending on the stress. The static analysis is performed using the finite element method. The difference between material linear and material nonlinear approach is illustratively described in the introduction. A shell finite element, which is enhanced by the possibility of further delamination into layers and integration points along its thickness, is suitable to be used for a numerical analysis of a plastic structures. Separate chapters are devoted to the integration of the resulting values over the height of the cross-section. The integration of the material stiffness matrix correctly reflects the emergence of eccentricity. A part of the attention is devoted to the numerical quadrature rules. Next chapter is devoted to material nonlinear models. Two approaches are described: a simpler one, using the isotropic nonlinear elastic model, and more general one, using the orthotropic plastic model. The theoretical description is complemented by the graphic interpretation of the criteria according to the individual authors. A significant portion of this work is devoted to the algorithmization of calculation procedures described in the theoretical chapters. The algorithmization itself is implemented in Fortran language into a dynamic-link library which is part of the software program RFEM 5 which is widely used in engineering practice. A part of the work is a study comparing the performance of the different technologies applicable for the algorithmization of the described issues. The agreement of the theoretical analysis of the material models and subsequent implementation within the RFEM 5 is demonstrated on the example of the bent cantilever. The thermoplastic aboveground tank structure is subject of detailed material linear, and nonlinear analysis respectively. The various approaches are compared on the results of stress, deformation an
|
|
|
High loading shovel for telehandlers LM1345 Turbo
Dragan, Lukáš ; Kubín, Martin (referee) ; Škopán, Miroslav (advisor)
This diploma thesis follow up the structural design high loading shovel for telehandlers LM1345 TURBO by New Holland. The introduction processed basic characteristics and parameters of the machine and material which will be in operation most frequently transported by the shovel. The work includes static analysis load acting on the shovel and frame when the machine is operating, strength calculations and the design and control of the peg.
|
|
|
Modification of Aluminium Cooler Holder
Malovaný, Daniel ; Ramík, Pavel (referee) ; Svída, David (advisor)
The purpose of this thesis is to overview the basic design solutions of full aluminum radiators. By finite element method to check the first generation of full aluminum low temperature radiator bracket and based on this calculation to modify the design to reduce tension in the critical areas. At the end of this thesis to evaluate the new design.
|
|
|
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
|
|
|
Hydraulic and mechanical holding device of front shovel of excavator LB 115
Bělov, Pavel ; Lžičař, Roman (referee) ; Škopán, Miroslav (advisor)
This Diploma thesis solves a quick coupler design for a loader. In introduction of the Diploma thesis are mentioned two potential designes and convenient solutions. Subsequently are outlined two practicable designes of a quick coupler for a original bucket, as a data componant of the second construction design is enclosed basic strength calculation. The ending point of the thesis deals and compare with the force decrease in use of a quick coupler and appraisals achieved ascertainment.
|
|
|
Analysis of the wind effect on the construction
Tačner, Jan ; Hradil, Petr (referee) ; Kala, Jiří (advisor)
Diploma thesis deals with static and dynamic analyses of a slender bridge structure behavior. The footbridge structure model was created in ANSYS 14.5 programing system. Static and a modal analyses were made afterwards and according to these analyses dynamic wind load and dynamic pedestrian load were applied. Wind load was applied as option of deck without a handrail and as option of deck with fully airtight handrail. Pedestrians were perceived as group of pedestrians and as a sparse crowd. Both applied loads were solved by harmonic analyses. Results of these analyses are resonance curves and tables of accleration.
|
guest ::
