|
|
Static Analysis of NumPy Programs
Zimen, Martin ; Kofroň, Jan (advisor) ; Blicha, Martin (referee)
NumPy programs can be hard to debug. Due to the dynamic nature of Python, a bug can manifest itself after a long time of run time. This causes the computation to crash, ditching all the progress. Existing static analysis tools can't detect NumPy-specific errors. We propose a solution that uses data-flow analysis combined with symbolic execution to detect ndarray shape mismatch errors. With a dynamic set of symbols, our method tracks ndarray dimensions and constraints between them throughout the program. It uses an SMT solver to solve the constraints and locate the bug. Our implementation understands core NumPy constructs and detects some shape mismatch errors for 1D and 2D ndarrays.
|
|
|
Federated learning
Georgiu, Martin ; Švarný, Petr (advisor) ; Blicha, Martin (referee)
for thesis Federated learning by Martin Georgiu The remarkable advancements in machine learning in recent years have been unprece- dented, yet the constant need for more and more data to train artificial neural networks (ANNs) remains. In sectors such as healthcare, it is unrealistic to aim to create one single dataset that would consolidate all the information about patients from various hospitals. When training ANNs, the data cannot leave the hospital, and therefore any ANN training can be executed solely locally on the given hospital's data. Federated learning (FL) is a novel approach that can be used in such settings, maintaining the system's privacy with- out compromises. In this thesis, we are comparing FL against other approaches striving for the same objective, diving into the security of FL and investigating concrete strategies for FL. Lastly, we've created a fully working open-source example of skin spot analysis trained using FL, which can also be easily extended and used with other datasets. 1
|
|
|
Effective Automated Software Verification: A Multilayered Approach
Blicha, Martin ; Kofroň, Jan (advisor) ; Rümmer, Philipp (referee) ; Bjørner, Nikolaj (referee)
In recent years, automated formal verification of software has progressed from a few research labs into large-scale applications, such as cloud infrastructure and smart contracts. Formal verification techniques based on model checking provide the necessary guarantees by exploring systems' behaviour exhaustively and automatically. Moreover, they provide witnesses (explana- tions) for the result of their analysis: a faulty behaviour, if there exists one, or a proof of the absence of such behaviour. However, the general problem that automated software verification is trying to solve is un- decidable. Despite this theoretical barrier, it is quite efficient on many instances that arise in practice. We ascribe this (perhaps surprising) success to a combination of factors: the relentless effort of researchers that come up with new verification procedures to tackle classes of problems where existing techniques struggle; amazing progress in the foundational technologies of satis- fiability solving, especially in Satisfiability Modulo Theories (SMT); and increase of available computational power through parallel and cloud computing. Nevertheless, the growing complex- ity of real-world systems poses new challenges for formal verification, especially for the scalability of the techniques. The task of automated software...
|
|
|
The continuum function on regular cardinals in the presence of large cardinals
Blicha, Martin ; Honzík, Radek (advisor) ; Verner, Jonathan (referee)
This thesis examines the interactions between the continuum function and large cardinals. It is know, by a result of Easton, that the continuum function on regular cardinals has great freedom in ZFC. However, large cardinals lay additional constraints to possible behaviour of the continuum function. We focus on weakly compact and measurable cardinal to point out the differences in interactions with the continuum function between various types of large cardinals. We also study the case of indescribable cardinals for the comparison, and the results lead us to conclude that it is not easy to pinpoint the reason for these differences. 1
|
|
|
Using Constrained Horn Clauses for Hierarchical Planning
Kažimír, Marián ; Blicha, Martin (advisor) ; Pantůčková, Kristýna (referee)
Title: Using Constrained Horn Clauses for Hierarchical Planning Author: Marián Kažimír Department: Department of Distributed and Dependable Systems Supervisor: Mgr. Martin Blicha, Department of Distributed and Dependable System Abstract: HTN planning is a popular approach to modelling planning problems. The goal of this project is to implement a HTN solver based on translating the planning problem to a reachability problem in a transition system and using off-the-shelf reachability solver for the actual solving. Keywords: Hierarchical Task Networks Planning problem Solver Transition sys- tem Constrained Horn Clauses
|
|
|
Branching loop summarization
Tatarko, William ; Blicha, Martin (advisor) ; Bednárek, David (referee)
In this thesis we present a novel algorithm for summarization of loops with multiple branches operating over integers. The algorithm is based on anal- ysis of a so-called state diagram, which reflects feasibility of various branch interleavings. Summarization can be used to replace loops with equivalent non-iterative statements. This supports examination of reachability and can be used for software verification. For instance, summarization may also be used for (compiler) optimizations. 1
|
|
|
Data Lineage Analysis for Qlik Sense
Jurčo, Andrej ; Parízek, Pavel (advisor) ; Blicha, Martin (referee)
Business Intelligence has become essential for all companies and organizations in the world over the past few years when it comes to decision-making and observing long-term trends. It often happens that Business Intelligence tools that are used become very com- plex over time and it can then be very difficult to make any changes. Data lineage solves this problem by visualizing data flows and showing relative dependencies. Manta Flow is the platform which creates such lineage which supports programming languages (Java, C), databases (Oracle, MS SQL) or Business Intelligence tools (Cognos, Qlik Sense). The goal of this thesis was to implement a prototype of a scanner module for the Manta Flow platform, which would analyze data flows in Qlik Sense and create a data lineage graph from data sources to the presentation layer. This module extracts metadata neces- sary for the analysis, resolves the objects that are present in the Qlik Sense applications, and analyzes data flows in them. The resulting data lineage graph is then visualized by other components of the Manta Flow platform. 1
|
|
|
Methods for reduction of Craig's interpolant size using partial variable assignment
Blicha, Martin ; Kofroň, Jan (advisor) ; Kučera, Petr (referee)
Abstract. Since the introduction of interpolants to the field of symbolic model checking, interpolation-based methods have been successfully used in both hardware and software model checking. Recently, variable assignments have been introduced to the computation of interpolants. In the context of abstract reachability graphs, variable assignment can be used not only to prevent out-of-scope variables from appearing in interpolants, but also to reduce the size of the interpolant significantly. We further extend the framework for computing interpolants under variable assignment, prove the correctness of the system and show that it has potential to further decrease the size of the computed interpolants. At the end we analyze under which conditions the computed interpolants will still have the path interpolation property, a desired property in many interpolation-based techniques. 1
|
|
|
Konstrukce modelů v polynomiální reprezentaci
Blicha, Martin ; Stanovský, David (advisor) ; Surynek, Pavel (referee)
Finite model finding is a problem defined as follows: given a theory in first-order logic, find a finite model of this theory. We present a new ap- proach to finite model finding based on a translation of axioms to a system of multivariate polynomial equation. Existence of a model of given size is then equivalent to an existence of a solution of the system. We prove the correctness of this approach, implement it and compare its performance with current state-of-the-art model finders. 1
|
|
|
The continuum function on regular cardinals in the presence of large cardinals
Blicha, Martin ; Honzík, Radek (advisor) ; Verner, Jonathan (referee)
This thesis examines the interactions between the continuum function and large cardinals. It is know, by a result of Easton, that the continuum function on regular cardinals has great freedom in ZFC. However, large cardinals lay additional constraints to possible behaviour of the continuum function. We focus on weakly compact and measurable cardinal to point out the differences in interactions with the continuum function between various types of large cardinals. We also study the case of indescribable cardinals for the comparison, and the results lead us to conclude that it is not easy to pinpoint the reason for these differences. 1
|
guest ::
