Národní úložiště šedé literatury Nalezeno 21 záznamů.  1 - 10dalšíkonec  přejít na záznam: Hledání trvalo 0.00 vteřin. 
Framework for Testing Student Projects
Dižová, Natália ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
This Master's Thesis is about design and implementation of a framework, whose target is to improve effectiveness and simplify student project's evaluation process. Theoretical part of this Thesis is dedicated to software testing fundamentals and used principles. It also describes Linux containerization technology. In the next part, Thesis contains analysis of requirements for student project testing in various University courses. Core of the Thesis describes design and its implementation of a system, which satisfies analyzed requirements. Last part shows how implemented system was verified and shows possible future extensions of this work.
Static Analysis Using Facebook Infer Focused on Errors in RCU-Based Synchronisation
Marek, Daniel ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Read Copy Update (RCU) is a synchronization mechanism, found mostly in the Linux kernel. Its sought-after features include almost zero overhead and high speed when reading shared memory. RCU has a set of rules of use, which need to be followed in order for the synchronization to work properly. To the best of our knowledge, there is no analyzer that sufficiently verifies if the RCU rules of use are adhered to. To overcome this, we propose a new analyzer, with the focus on finding violations in the use of RCU rules. The analyzer is based on static analysis and implemented as a module for the static analysis framework Facebook/Meta Infer. This platform was chosen because it provides scalability, which is needed when dealing with such an extensive software as the Linux kernel. The designed analyzer is capable of detecting multiple different ways in which the RCU usage rules can be broken, each causing either a race condition or a deadlock. It is also capable of generating warnings for situations when a deprecated function call is used or when the use of incompatible RCU reader and writer primitives is detected. The analyzer is the first of its kind. It may become a basis for future analyzer development in the field of Read Copy Update. Furthermore, it may be used as a test tool in the Linux kernel development cycle.
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called k I k I. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.
Performance Analysis Based on Noise Injection
Liščinský, Matúš ; Malík, Viktor (oponent) ; Fiedor, Tomáš (vedoucí práce)
In this work, we proposed a Perun-Blower framework which utilises the perfblowing technique: injecting of noise into the functions of the tested program, followed by collecting of runtime data of these functions from the program run and evaluating the impact of the noise on the program performance. We build on the dynamic binary instrumentation of the Pin framework to inject the noise into program. We then focus on finding functions with high impact on performance as well as estimate the thread run's potential acceleration when optimising the particular functions. Moreover, we have extended the existing Trace collector used in the Perun framework to collect the runtime of functions with a new so-called engine based on the Pin framework. We tested the functionality of our implementation on two non-trivial projects, where we were able to find functions (1) with considerable impact on performance, (2) with the most significant optimisation benefit, and (3) whose degradation forces the non-termination of the program after several hours of running.
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Static analysis is nowadays often used in the development process to find defects in the produced software. Although static analysis tools can effectively find bugs in software with millions of lines of code, they have also some disadvantages. The main disadvantages are the difficulty to deploy the chosen tool on the given project, high numbers of false reports, and the time and space requirements. This thesis focuses on mitigating these negative features of the Facebook Infer tool mainly for the context of using it to analyse Linux utilities shipped as SRPM packages. To simplify its deployment, an Infer plugin has been created for the csmock tool, which allows static analysers to run automatically on packages for CentOS or Fedora. To reduce the number of false reports, a filter has been created, which filters Infer's output according to several proposed heuristics based on experience obtained by analysing the reports produced by Infer. The filter has been also included into the csmock plugin and tested on a number of packages. On the analysed packages, the filter was able to remove 60 % of false reports with a loss of 2.5 % of real defects. The time required to run the analysis can be reduced by using incremental analysis. Shortcomings of the incremental analysis provided implicitly by Infer were experimentally found, so this thesis also describes the creation of a wrapper for Infer, which replaces the incremental analysis in Infer.
Equivalence-Based Slicing of Programs
Malecová, Tatiana ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The aim of this work is to design a method that simplifies two programs based on the results of analysis of their semantic difference. The goal is to remove as many semantically equivalent parts of the programs as possible. To find these equivalent parts, we apply our own solution to the problem of finding the maximum common induced subgraph. Subsequently, we are able to simplify the programs by using backward static slicing. By applying this simplification, we obtain sliced programs that consist of the differing parts and parts that can affect these differences. The method has been implemented as an extension of the DiffKemp tool, which is a static analyser of semantic differences between different versions of large scale programs. Our experiments on the Linux kernel show that the method is able to produce correct slices very efficiently (the analysis is prolonged only by 3.2%). Moreover, the created slices are much smaller than the original programs, which makes them suitable for further analysis.
Applying Code Change Patterns during Analysis of Program Equivalence
Šilling, Petr ; Fiedor, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this thesis is to propose a static analysis method for recognition of code change patterns describing recurrent changes between different versions of low-level code. The thesis proposes an encoding method of patterns, which uses the LLVM intermediate representation, and a pattern matching algorithm based on gradual comparison of instructions according to their control flow. The proposed analysis has been implemented as an extension of DiffKemp, a tool for analysing semantic differences between versions of large C projects. Results of experiments conducted on three pairs of past versions of the Linux kernel show that the extension is able to eliminate a substantial amount of false-positive or generally undesirable differences from the output of DiffKemp, which would otherwise require manual inspection.
Webový prohlížeč reportů analýzy zdrojových kódů
Dolejší, Jakub ; Malík, Viktor (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato bakalářská práce se zabývá návrhem a vývojem webové aplikace RepView. Tento nástroj slouží k interaktivní revizi zdrojových kódů na základě příslušného reportu analýzy zdrojových kódů. Aplikace se skládá ze dvou oddělených služeb, které běží v separátních kontejnerech technologie Docker. Cílem aplikace je usnadnit interpretaci reportu a jeho vazbu na zdrojové kódy. Výsledku je dosaženo za použití moderních webových technologií (Vuejs, Quasar), které umožňují provést uživatelsky přívětivou revizi zdrojových kódů.
Automatic Forward Slicing of Programs
Patrik, Nikolas ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
This thesis presents designing new forward slicing solution for the DiffKemp tool. After strenuous analysis of currently implemented solution in DiffKemp for forward slicing we decided to retain current solution and extend it by few enhancements that should improve the analysis provided by DiffKemp in a quite big scope. We have implemented extensions so DiffKemp can perform analysis on fields of structured types which might represent run-time parameters and also we extended slicing criterion with the value of analyzed variable. Also we added support for slicing module kernel parameters. After implementing this solutions, we did experiments which proved that implemented solution has improved the analysis performed by DiffKemp.
System for Automatic Filtering of Tests
Lysoněk, Milan ; Smrčka, Aleš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this thesis is to create a system that automatically determines a set of tests that must be run when a change is done in the ComplianceAsCode project. The proposed method selects a set of tests based on static analysis of the changed sources, taking into account the internal structure of ComplianceAsCode. The created system is divided into four parts - obtaining changes from the versioning system, static analysis of different types of files, computing the set of files affected by the change, and computing the set of tests that must be run to test the given change. We implemented analysis of several types of files and our system is designed to be easily extended by other analyses for other file types. The created implementation is deployed on the server where it automatically analyzes new contributions to the ComplianceAsCode project. The automatic running informs contributors and developers about changes that it found and recommends which tests should be run for the change. This saves the time spent on verifying the correctness of contributions as well as the time spent on running tests.

Národní úložiště šedé literatury : Nalezeno 21 záznamů.   1 - 10dalšíkonec  přejít na záznam:
Viz též: podobná jména autorů
2 MALÍK, Vladimír
1 Malík, Václav
Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.