Aleš Rýznar, M.A.

2022 - 2024

Many ongoing and future experiments utilize medium-mass atomic nuclei as exquisite laboratories for exploring the fundamental symmetries of nature and searching for signals of new physics beyond the Standard Model. While large particle colliders probe the high-energy frontier, sensitive studies of low-energy nuclear processes provide a complementary approach. We will exploit a novel combination of physics, mathematics, and advanced computational methods to build a novel quantum many-body framework for solving the structure of medium- mass nuclei and their processes from first principles with unprecedented accuracy and scope. This will allow us to provide a number of key nuclear theory predictions needed for the interpretation of ongoing and future experimental efforts to detect dark matter and to search for violations of predictions of the Standard model in electroweak nuclear processes.

2020 - 2023

Combinatorics on words is an area of discrete mathematics and like other combinatorial fields it naturally tends to technical and tedious proofs that often repeat similar arguments and contain complex case analysis. As such it is suitable for a computer verifiable formalization, which however has not been seriously attempted so far. Our intention is to formalize basic theory of combinatorics on words in the proof assistant Isabelle/HOL, and then to focus on the vast project of classification of binary equality words, whose complexity is on the borderline of human control. The project will provide an incontestable presentation of existing results, will explore their boundaries, and test capability of automated provers to find new facts in this area, or at least to accelerate human research.

2024 - 2026

While there is an increasing number of practical applications of game theory, there are still severe computational limitations of the current models and algorithms used to find approximate optimal strategies. One such limitation is the high computational complexity of finding an equilibrium for games with large or even infinite sets of actions. Moreover, the strategy space in applications have often a complex inner structure making the equilibrium computations even more difficult. We propose advancing the state-of-the-art in the theoretical understanding of the structure of equilibria in games with complex strategy spaces, developing novel iterative strategy-generating algorithms for finding approximate solutions, investigating the computational complexity of equilibrium problem for special classes of games, and applying these fundamental results to various card games.

2023

Projekt má přímou vazbu na cíle Inovační strategie České republiky 2019–2030 v oblasti ochrany duševního vlastnictví, a to zejména na cíle týkající se zvýšení povědomí o ochraně duševního vlastnictví a využívání patentových informací. Projekt podpoří informovanost veřejnosti o problematice duševního vlastnictví, usnadní přípravu přihlášek k předmětům průmyslové ochrany, využije dostupné patentové informace a umožní snížit nároky na kapacitu pracovní síly a poskytnout nepřetržitý servis interním a externím zákazníkům. Účelem je kvalitnější a efektivní výkon státní správy. Hlavními cíli projektu je vyvinout systém obsahující bázi znalostí zachycující obecné informace ke správnímu řízení.

2023 - 2027

This project will create novel mathematical methods that facilitate a better understanding of the properties of massive networks. Such networks appear in many real-life situations including links between Internet routers, user connections on social networks, or protein-to-protein interactions inside a molecule. Large networks are, however, also fundamental to many open problems in pure mathematics. In particular, they are a central object in extremal combinatorics. One of the key elements of this project focuses on providing new techniques of using a computer in order to find mathematical proofs. Another important aspect of the project revolves around randomness, which turns out to be extremely effective in various mathematical and computer science scenarios. In fact, for many problems involving decisions that were solved in this randomized way, we currently do not know anything that would perform even nearly as good as random choices do. In this project, we will study so-called pseudorandomness - a systematic way that aims at catching up with the randomness by being smart.

2022 - 2025

The project researches new methods of effective protection against cyber threats that misuse secured communication for cyber attacks against servers and computers in the environment of high-speed networks. Based on available metadata, the project will investigate Machine learning methods suitable for determining the characteristics of the encrypted network flows and associated risks. The system will be implemented using a hardware-accelerated traffic monitor and a software prototype for high-speed detection of security incidents, which will be reported to the SIEM tool. Further, a plug-in to the QRadar system for the incident analysis will be developed. The project outcomes will also include reference data sets of network traffic and a system for their collection and annotation.

2022 - 2025

The goal of this project is to study number fields of higher degrees and use the local-global principle to determine their structure. We will focus on composite fields, for which one can extend partial information from their subfields to the whole field. For them, we will investigate their additively indecomposable integers and derive asymptotic formulas for the number of elements of small norms. Moreover, we plan to estimate their Pythagoras number and the number of variables of their universal quadratic forms. This was studied by many great mathematicians, including Lagrange or Siegel, but we still do not understand it fully. The methodology is based, for example, on the Hasse norm principle or representation of quadratic forms. Furthermore, considering a system of linear polynomials in one variable, we will aim to find an asymptotic formula for the number of integers up to some bound, for which the values of these polynomials are primes with given prescribed primitive root. For that, we want to use the nilpotent circle method developed by Green, Tao, and Ziegler.

2022 - 2024

Motion planning for multiple robotic agents (MR-MoP) is a task to find non-colliding sequences of simple movements for individual robotic agents so each agent achieves its individual goal. An important character-istic of the task is the large number of relatively simple robotic agents that can physically interact with each other in various ways. The task is based on the well-known multi-agent path finding (MAPF), but places more emphasis on the real properties of the environment in which the robotic agents operate, namely the continuity of space and time is assumed. Considering the continuity of the environment directly in abstract models can lead to more precise and mode efficient plans. The project assumes algorithmic contributions to motion planning for a multi-agent system on all important layers of common planning abstractions, i.e. from the level of (discrete) classical planning, through (continuous) motion planning, to the execution of plans with physical robots. The new algorithms will be based on the principles of logical reasoning, in particular lazy compilation approaches.

2023 - 2027

Cílem projektu je vyrobit virtuální model dnes neexistujících, či změněných lokací v historické části města Most. Jako zdrojový materiál poslouží převážně historické kresby a fotky, které budou augmenotvány, opraveny, kolorovány a poslouží k vytvoření 3D modelů pro virtuální realitu dostupnou jak přes webové rozhraní, tak VR headsety.

2022 - 2024

Fixed-parameter tractability and approximation algorithms are nowadays standard tools for design of algorithms for hard problems in the area of Computational Social Choice. Surprisingly, kernelization, a prominent technique in FPT algorithmics, is not used as often to tackle social choice problems. Kernelization is a formalism of safe data reduction which we believe does have its place in all research disciplines dealing with large and complex datasets. The most recent approach is the so-called lossy kernelization which on the one hand cooperates with approximation algorithms (unlike kernelization which can only be pipelined with exact algorithms) and on the other hand, allows circumventing hardness results (in exchange for introducing a possible loss in the quality of the solution). This project aims on filling this gap of usage of these tools in computational social choice. The suggested line of research continues our current studies in this area and the new proposed directions will need novel algorithmic approaches as they focus on the boundaries of traceability. We have identified several interesting questions where there is potential to apply the above. Our aim is to significantly deepen our understanding of these computationally hard problems by providing polynomial-sized (lossy) kernels or showing that the problems are resistant to this line of attack.

2024 - 2027

The project deals with streamlining the work with FAIR data in research - their planning (plan), monitoring (track) and evaluation (assess). It is primarily about introducing interoperability between existing DMP creation tools, SKG-type services and evaluation tools. Likewise, other supporting tools related to research data management will be incorporated. The results of the project will be verified by a number of pilots across Europe.

2022 - 2025

A framework which is a graph together with a realization of its vertices in some space is called rigid if there are only finitely many realizations inducing the same edge lengths as the given one, up to isometries. Otherwise, the framework is flexible. Since rigidity is a generic property, the graph itself can be called rigid if every generic realization yields a rigid framework. Nevertheless, such a rigid graph can have non-generic flexible realizations. These paradoxical situations are investigated in the frame of this project. Using tools from algebraic geometry, the existence of paradoxical motions in the plane was recently characterized in terms of a special type of colorings of the edges. The purpose of this project is to combine graph theory and combinatorics with more sophisticated tools from algebraic geometry in order to be able to answer paradoxical flexibility questions in a broader sense. As such we are interested in symmetric flexes, different generalizations of rigidity, applications thereof to sensor networks and the above mentioned edge colorings.

2024 - 2025

Creating a reproducible environment for data-analysis pipelines is hard. The current practice is to assemble it manually. That is both labor-intensive and error-prone and requires skills and knowledge that data analysts do not usually have. While there exist tools that try to simplify this process, they all rely on some metadata that has to be provided by the user. Getting this metadata is not trivial. Not only does one have to include all the libraries directly imported with their transitive dependencies, but each of these libraries can depend on native libraries and tools, which themselves have their dependencies and configurations. Versions have to be pinned appropriately as libraries frequently update and change their behavior. There is no description of these dependencies, and thus the process of gathering the metadata is mainly based on experience and trial-and-error. The challenge that we are addressing is to build an automated system that can track all of the pipeline dependencies, data inputs, and other sources of non-determinism to prepare an environment where data-analysis pipelines can repeatedly run, producing identical results.

2023 - 2027

The RiGiD project lays the groundwork for this research programme and aims to develop a methodology for rigorous engineering of data analysis pipelines that can be adopted in practice. Our approach is pragmatic. Rather than chasing functional correctness, we hope to substantially reduce the incidence of errors in the wild. The research is structured in three overlapping chapters. First, identify the problem by carrying out user studies and large-scale program analysis of a corpus of over 100,000 data science pipelines. The outcome will be a catalog of error patterns as well as a labeled dataset to be shared with other researchers. The technical advances will focus on combining dynamic and static program analysis to approximate the behavior of partial programs and programs written in highly dynamic languages. The second part of our effort proposes a methodology and tooling for developing data sciences codes with reduced error rates. The technical contributions of this part of the project focus on lightweight specification techniques and, in particular, the development of a novel gradual typing system that deals with common programming idioms found in our corpus. This includes various forms of object orientation, data frames, and rich value specifications. These specifications are complemented with an automated test generation technique that combines test and input synthesis with fuzzing and test minimization. Finally, the execution environment is extended to support automatic reproducibility and result audits through data lineage. The third and last part of the work evaluates the proposal by conducting user studies and developing tools for automating deployment. The contribution will be a qualitative and quantitative assessment of the RiGiD methodology and tooling. The technical contribution will be tools that leverage program analysis to infer approximate specifications to assist deployment and adoption. Our tools target R, a language for data analytics with 2 milli

2023 - 2027

The project will be focused on several fundamental problems in discrete and computational geometry, and their surrounding (sub)areas.

2023 - 2024

The project deals with the design (and implementation) of new side-channel attacks on the postquantum algorithms, as well as the design (and implementation) of countermeasures that will prevent these attacks.

2022 - 2024

Free Banach spaces play an important role in the study of nonlinear geometry of Banach spaces and in areas involving transportation problems. This brings them to the forefront of modern functional analysis and interest in them continues to grow. The free space of a metric space M is given by the fact that M isometrically embeds in it and that any Lipschitz map from M to a Banach space extends uniquely to a bounded linear map from the free space. This allows the linearization of nonlinear problems, but at the cost of a complicated linear structure. Its closer examination is the aim of our project. The free space lies in the dual of the space of Lipschitz functions and forms its predual. Hence, one should analyze all three of the spaces to understand free space. We intend to study representation of functionals on the spaces of Lipschitz functions and topological aspects of isomorphic free spaces. This could contribute to solving some known open problems in the area, such as the complementability in the bidual, predual uniqueness, or the existence of isomorphisms of certain free spaces.

2022 - 2025

Projekt reaguje na současný nedostatek nástrojů pro analýzu a verifikaci bezpečnostní certifikace zařízení používaných pro zajištění kybernetické bezpečnosti. Zejména u hardwarových zařízení implementujících kryptografické algoritmy, například čipových karet, je v ČR téměř nemožné spolehlivě ověřit deklarovanou úroveň bezpečnosti, což následně znemožňuje analýzu rizik systémů využívajících tato zařízení a tedy použití zařízení např. u bezpečnostních složek státu či v rámci kritických informačních infrastruktur. V rámci projektu budou vyvinuty nové hardwarové a softwarové nástroje založené na principech umělé inteligence, které bude možné využít pro specifické kroky automatizované verifikace bezpečnosti kryptografického zařízení - ať už na základě bezpečnostní certifikace nebo tvrzení výrobce/dodavatele.

2021 - 2023

Currently, a large amount of multimedia content (audio/video) is offered through online platforms, typically at the request of the user (Video-on-Demand). This practice is quite common today for paid services (eg online video rentals), but it also appears on data sharing platforms (eg. Ulož.to), where the legality of the origin of the data cannot be guaranteed. There are even platforms where it can even be argued (see the document "On the Net") that your own content, regardless of origin, can be extremely harmful (eg. terrorism, child pornography, etc.). The whole thing is further complicated by the fact that the majority of this traffic is currently encrypted using the HTTPS protocol, which makes it very difficult to identify. The purpose of the project is to search for ways and mechanisms for finding the fingerprint of specific video streams and then identify them from the network traffic reported via the NetFlow / IPFix protocol. The solution of the project presupposes the creation of a common research infrastructure over a distributed data storage (created from SSD or NVMe disks) between the two university workplaces, the interconnection of which will be realized through the Cesnet backbone network.