National Repository of Grey Literature 6 records found  Search took 0.00 seconds. 
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
Implicational fragments of intuitionistic propositional logic
Blicha, Martin ; Švejdar, Vítězslav (advisor) ; Chvalovský, Karel (referee)
In this thesis we study implicational fragments of intuitionistic propositional logic with finite number of atoms. The first part is dedicated to the fragment with only two atoms, which is simple enough to analyze the relations between it's formulas, but is not that trivial. In the next part, we introduce the terms prime node and prime model, which allow us to examine other fragments. In the last part, we find out how the results change when we add the constant into out language.

Interested in being notified about new results for this query?
Subscribe to the RSS feed.