|
|
Automated Formal Verification of Program Correctness Using SDV, Copper, or Similar Tools
Kovalič, Peter ; Šimáček, Jiří (referee) ; Vojnar, Tomáš (advisor)
This thesis is concerning about verification of drivers. Principally is focused on model checking tools, from which the Static Driver Verifier is the most important. A driver Ext2Fsd is checked by this program. This driver belongs to group of file system drivers. Control is driven by entered rules, which the driver must not violate. The aim of this thesis was to verify chosen driver by selected tool. The results have covered all three types of verification´s end. There were rules that driver passed, that driver violated and also that driver didn´t accept. The final chapter of work is about another model checking tool Copper. It offers the basic knowledge about this program.
|
|
|
Forensic Malware Analysis
Král, Benjamin ; Trchalík, Roman (referee) ; Očenášek, Pavel (advisor)
This master's thesis describes methodologies used in malware forensic analysis including methods used in static and dynamic analysis. Based on those methods a tool intended to be used by Computer Security Incident Response Teams (CSIRT) is designed to allow fast analysis and decisions regarding malware samples in security incident investigations. The design of this tool is thorougly described in the work along with the tool's requirements on which the tool design is based on. Based on the design a ForensIRT tool is implemented and then used to analyze a malware sample Cridex to demonstrate its capabilities. Finally the analysis results are compared to those of other comparable available malware forensics tools.
|
|
|
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.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (referee) ; Malík, Viktor (advisor)
Cílem této práce je navrhnout vylepšený mechanismus rozbalování smyček pro analyzátor 2LS. 2LS je nástroj pro statickou analýzu C programů založený na usuzování o programech pomocí SMT solveru. Kombinuje několik běžných verifikačních technik do algoritmu zvaného k I k I. Jednou z klíčových součástí tohoto algoritmu je rozbalování smyček programu. Současné řešení bohužel neumožňuje správně rozbalovat smyčky obsahující operace s dynamicky alokovanou pamětí. Námi navrhované řešení je založeno na rozbalování smyček v GOTO programu namísto SSA formy, díky čemuž je možné správně pracovat s dynamickými objekty a operacemi s nimi. Navržené řešení bylo implementováno v nástroji 2LS a naše experimenty na sadě testů z mezinárodní soutěže ve verifikaci software (SV-COMP) ukazují, že zvyšuje korektnost analýzy programů pracujících s dynamickými objekty.
|
|
|
A Static Analysis Tool Detecting Bugs in Signal Handlers
Kozovský, Daniel ; Vojnar, Tomáš (referee) ; Peringer, Petr (advisor)
This work is about the plugin csigsafe for the GCC compiler. It uses static code analysis to detect bugs in signal handlers according the POSIX norm. This tool analyzes the source files written in C and C ++. This analyzer is created for the Red Hat, which uses it to test sRPM packages used in their Linux distributions. The tool has been tested on a sample of 37 Open Source projects. Testing has shown the utility of the tool to search for errors associated with violation of rules for proper signal handling.
|
|
|
Static analysis of the roof
Hořínek, Josef ; Vlk, Zbyněk (referee) ; Martinásek, Josef (advisor)
The Bachelor Thesis focuses on a static analysis of a timber roof truss. This roof trust is part of the saddle roof on the family home. The load on the structure is calculated manually according to valid standards. The load is divided into a total of 11 load cases. The calculation model of the structure is created in RFEM. Results of internal forces and deformations are checked by manual calculation using methods for statically indeterminate structures. These values are compared at the end.
|
|
|
Static analysis of acoustic enclosure
Hándlová, Barbora ; Martinásek, Josef (referee) ; Vlk, Zbyněk (advisor)
The subject of this Bachelor’s thesis is a structural analysis of acoustic enclosure, which is located above production facilities. The enclosure is assembled of elements with a load-bearing skeleton made of steel. It is possible to dismount the enclosure in parts. Computational software RFEM was chosen to model the 3D structure. The aim of this thesis is an assessment of ultimate and serviceability limit state of some selected elements. Some of the results obtained from the RFEM program are verified by hand-done calculation.
|
|
|
Multipurpose centre in Hodonín
Zbořil, David ; Štrba, Michal (referee) ; Šmak, Milan (advisor)
This diploma thesis solves with the design and static assessment of a multipurpose center in Hodonín. The structure is divided into three statically separated parts. The two structural units, consisting of steel frames with composite reinforced concrete slabs, are symmetrical and the middle part, formed by wooden frames made of glued laminated timber. The construction was solved using a computational 3D model. The model was created in the program RFEM 5.21.01. Using the model, the internal forces and dimensions of the usual elements were calculated. The construction was assessed in the program RFEM 5.21.01 and in MS Excel 2010. The outermost buildings have 7 floors and are designed for residential and office space. The maximum height of the structure is 27.60 m, including the attic. The central multifunctional hall is roofed by a walkable green roof. The maximum height of the middle part is 12.50 m. The largest floor plan dimensions of the building are 49,050 m x 24,000 m.
|
|
|
Reinforced concrete structure
Malecha, Tomáš ; Šimůnek, Petr (referee) ; Šulák, Pavel (advisor)
This bachelor‘s thesis includes structural analysis and check of reinforced concrete, cast-in-place construction of a building for parking. Here is solved locally supported floor slab above first above ground floor. Structural analysis was solved by program Scia Engineer 14 and checked by manual calculation. Next step was dimensioning for ultimate limit state, concretely for bending moment, punching and for serviceability limit state, concretely for limitation of cracks. For this bachelor’s thesis were made drawings based on calculated results.
|
|
|
The analysis of track response to railway vehicles
Kopeček, Josef ; Plášek, Otto (referee) ; Salajka, Vlastislav (advisor)
The diploma thesis deals with the assembly of numerical models of classical track using the finite element method in several variants. Models are compared with results obtained on analytical models. More complex models simulate the real behavior of a track running on a railway vehicle. The purpose is created methodology of modeling the railway track for use in static and dynamic analysis.
|
guest ::
