Výsledky

Adam Žitňansḱý

Shape Model Detection, Cuboid Detection, Stacked Hourglass Network

Zpracování dat (obraz, zvuk, text apod.)

This work addresses the problem of cuboid detection, more specifically detection of boxes in RGB images. The main result is the implementation of a system for detecting boxes and their accurate localization based on the detection of cuboid primitives: corners and edge points. The system consists of a detector of corner and edge points based on convolutional neural networks. Such detected primitives are processed into a model of the cuboid. Our system was trained and evaluated on a custom dataset of packaging boxes which was created as a part of this work. The trained model achieved PCK 90 % and recall 86 % for corners resp. 97.5 % and 96 % for edge points on unseen data.

Šimon Sedláček

Voice Activity Detection, Recurrent Neural Networks, Speaker Verification

Zpracování dat (obraz, zvuk, text apod.)

This work aims to implement, test, and evaluate a speaker-conditioned voice activity detection method proposed by [1], originally called "Personal VAD". The method builds upon an LSTM based approach to voice activity detection and its purpose is to introduce a system that can reliably detect speech of a target speaker, while retaining the typical characteristics of a VAD system, mainly in terms of small model size, low latency, and low necessary computational resources. The system is trained to distinguish between three classes: non-speech, target speaker speech, and non-target speaker speech. For this purpose, the method utilizes speaker embeddings as a part of the input feature vector to represent the target speaker. Some of the more heavyweight personal VAD variants also make use of speaker verification scores issued to each frame based on the target embedding, resulting in a more robust system. In addition to the one scoring method presented in the original paper, two other scoring approaches are introduced, both outperforming the baseline method and improving the system's performance even for acoustically challenging conditions.

Roman Dobiáš

OpenGL, autostereoscopic display, single to multiview conversion, automated conversion, pipeline injection, API call hooking

Počítačová grafika

The adaptation of upcoming autostereoscopic displays by regular users depends on the availability of supported applications. To increase such a set, this paper describes compatibility software which turns (semi) automatically the output of regular OpenGL 3D applications to display-native output, which takes advantage of true 3D displays capabilities. This is achieved using a conversion layer that intercepts parts of OpenGL API and translates such API calls to ones that produce a multiview output of the original application.

Jana Gregorová

Automatic Score Evaluation for Bullseye Shooting, Computer Vision in Sports Shooting, Background Subtraction, Template Matching, Image Stabilization, Cross-correlation of Two 2D Arrays

Zpracování dat (obraz, zvuk, text apod.)

Bullseye shooting is a shooting sports discipline where the shooter is standing in one place and shooting at a static paper target. The shooter’s goal is to land as many hits in the centre of the target as possible. The distance between the shooter and the target usually ranges from 10 m to 300 m. That way, while shooting, the shooter is unable to see where exactly their hits land unless some kind of auxiliary equipment is used. To calculate the score, all shooting needs to be stopped as the shooter walks right into the field to see their target up close. For a new round, the shooter either has to change the target for a new one or cover target hits up with cover up patches. The goal of this work is to find a solution to calculate shooter’s score automatically. One of the possible approaches to this problem is taking a video of the target and processing it, so that new hits in the target can be detected and their score calculated. The resulting image will then be shown to the shooter on a screen near them. The result of this paper is a commercial distribution-ready solution both for individual shooters and commercial shooting ranges. The solution consists of a camera setup and an application which displays the video from camera and evaluates the shooter’s score using computer vision. The solution brings significant improvements in terms of shooter’s comfort and bullseye shooting training effectiveness. It is an innovative equipment not only for skilled shooters, but also for beginner shooters.

Jan Zavřel

EIGRP, Simulation, Routing, OMNeT++

Modelování a simulace Počítačové sítě

This paper deals with the implementation and the evaluation of a simulation model of a modern dynamic routing protocol designed by Cisco Systems, Inc. called Enhanced Interior Gateway Routing Protocol (EIGRP) in a discrete simulator OMNeT++ implemented in C++. The resulting simulation model can be used to conduct various experiments which allow network designers and alike to explore the protocol's behavior in different situations inside a safe discrete environment. In order to produce a trustworthy simulation course, the protocol model must be as accurate as possible to the real implementation and thoroughly tested. This paper provides a basic overview of both protocol EIGRP and simulator OMNeT++. It also discusses the state of the model before and after the integration into a newer version of the INET framework, showcases improvements, and outlines the testing methodology.

Tomáš Vondráček

Identifikace uživatelů, Otisk prohlížeče, Otisk zařízení, Detekce webových rozšíření

Bezpečnost Webové technologie

Práce se zabývá vytvořením knihovny pro získávání informací o uživatelích na webových stránkách, kde získané informace mohou být použity pro identifikaci uživatelů. Navrhl jsem nové techniky získávání informací a optimalizoval některé aktuálně používané techniky. Implementovány jsou také techniky, kterými lze odhalit vedlejší efekty způsobené webovými rozšířeními, které maskují identitu uživatelů. Na základě analýzy webových rozšíření byly detekovány dříve neznámé informace, které mohou být taktéž použity pro identifikaci uživatele. Analyzovány jsou i získané informace o prohlížeči a zařízení z hlediska míry získané informace, doby jejich získání a stability v čase. Z výsledků analýzy lze optimalizovat množství získávaných informací, čímž lze omezit potenciální zpomalení webových stránek.

Pavel Eis

Automatizovaná anotace síťových zařízení, Klasifikace zařízení, Statistická klasifikace

Počítačové sítě

Automatická klasifikace zařízení v počítačové síti lze využít pro detekci anomálií v síti a také umožňuje aplikaci bezpečnostních politik dle typu zařízení. Pro vytvoření klasifikátoru zařízení je stěžejní kvalitní datová sada, jejichž veřejná dostupnost je nízká a tvorba nové datové sady je složitá. Cílem práce je vytvořit nástroj, který umožní automatizovanou anotaci datové sady síťových zařízení a vytvoření klasifikátoru síťových zařízení, který využívá pouze základní údaje o síťových tocích. Výsledkem této práce je modulární nástroj poskytující automatizovanou anotaci síťových zařízení využívající systém ADiCT sdružení Cesnet, vyhledávače Shodan a Censys, informace ze služeb PassiveDNS, TOR, WhoIs, geolokační databáze a informace z blacklistů. Na základě anotované datové sady je vytvořeno několik klasifikátorů klasifikujících síťová zařízení podle používaných služeb. Výsledky práce nejen výrazně zjednodušují proces vytváření nových datových sad síťových zařízení, ale zároveň ukazují neinvazivní přístup ke klasifikaci síťových zařízení.

Vladimir Jerabek

Monitorování sítě, Peer-to-Peer, Bitcoin, Kryptoměny, Analýza dat

Počítačové sítě

Cílem této práce je vytvořit platformu, která bude shromažďovat relevantní informace o aktivních uzlech v peer-to-peer síti Bitcoin. Díky monitorování chování jednotlivých uzlů v síti, jsem schopen sbírat důležité data pro podrobnější analýzu. Implementované řešení využívá nemodifikovaného Bitcoin Core klienta, a nabízí jednoduchou škálovatelnost díky modulární architektuře, která je dosažena za pomoci Docker kontejnerizace. Platforma poskytuje i jednoduchou vizualizaci nashromážděných dat. Součástí této práce je také analýza nashromážděných dat z dvouměsíčního běhu platformy BiNMon. Tato platforma v rukou vědců bude představovat relevantní a autentický zdroj informací o kryptoměně Bitcoin. V neposlední řadě může tato práce sloužit i jako zdroj inspirace pro ostatní vývojáře, kteří chtějí vytvořit podobný nástroj na shromažďování a analýzu velkého množství dat například z dalších kryptoměn.

Aleš Postulka

Rozšíření pro webové prohlížeče, Transparency and Consent Framework, Consent Management Platform, Souhlas se zpracováním osobních údajů

Webové technologie

Cílem této práce je návrh a implementace rozšíření pro webové prohlížeče Mozilla Firefox a Google Chrome. Účelem rozšíření je umožnění automatizované správy poskytnutých souhlasů se zpracováním osobních údajů. Souhlas se zpracováním osobních údajů je kvůli evropskému nařízení GDPR potřeba poskytovat na většině webových stránek. Za účelem usnadnění získávání souhlasu se zpracováním osobních údajů byl organizací IAB Europe vytvořen rámec Transparency and Consent Framework (TCF), který mimo jiné poskytuje rozhraní pro přístup k informacím o uloženém souhlasu. Vytvořené rozšíření interaguje s webovými stránkami využívajícími TCF. Umožňuje automatické poskytnutí souhlasu na základě nastavení, a také zobrazení informací o poskytnutém souhlasu. Rozšíření je publikováno v obchodu s doplňky pro prohlížeč Mozilla Firefox.

Filip Kočica

sklad, optimalizace, simulace, generátor, objednávka, produkt, pickování, evoluce

Robotika a umělá inteligence

Tato práce řeší problematiku alokace produktů do lokací ve skladu za pomoci moderních meta-heuristických přístupů v kombinaci s realistickou simulací skladu. Práce poskytuje grafický nástroj umožňující sestavení modelu skladu, generování syntetických zákaznických objednávek, optimalizaci alokace produktů za pomoci kombinace state of the art technik, simulátor vytvořeného modelu skladu a nakonec nástroj pro hledání nejkratší cesty objednávky skrze sklad. Práce také uvádí porovnání různých přístupů a experimenty s vytvořenými nástroji. Podařilo se optimalizovat propustnost experimentálního skladu na téměř dvojnásobek (~57%). Přínosem této práce je možnost vytvoření modelu plánovaného či již existujícího skladu a jeho simulace i optimalizace, což může značně zvýšit propustnost skladu a pomoci detekovat a odstranit vytížená místa. To může vést k ušetření zdrojů či pomáhat v plánování. Dále tato práce přináší nový způsob optimalizace skladu a nové optimalizační kritérium.

Anton Firc

deepfake, cybersecurity, voice biometrics

Bezpečnost Robotika a umělá inteligence

Deepfake technology is on the rise, many techniques and tools for deepfake creation are being developed and publicly released. These techniques and tools are being used for both illicit and legitimate purposes. One of the unexplored areas of the illicit usage is using deepfakes to spoof voice authentication. There are mixed opinions on feasibility of deepfake powered attacks on voice biometrics systems providing the voice authentication, and minimal scientific evidence. The aim of this work is to research the current state of readiness of voice biometrics systems to face deepfakes. The executed experiments show that the voice biometrics systems are vulnerable to deepfake powered attacks. As almost all of the publicly available models or tools are tailored to synthesize the English language, one might think that using a different language might mitigate mentioned vulnerabilities, but as shown in this work, synthesizing speech in any language is not that complicated. Finally measures to mitigate the threat posed by deepfakes are proposed, like using text-dependent verification because it proved to be more resilient against deepfakes.

Silvie Němcová

Neural Network Training, Loss Function, Training Process Examination

Robotika a umělá inteligence

The neural network training process involves a highly dimensional non-convex optimization problem. The training is a highly computationally demanding task with a risk that the optimization algorithm will be stuck at a local optimum or a saddle-point. Despite these concerns, modern neural networks are trained successfully only using straightforward training with SGD algorithm and regularization. A simple technique for analyzing the training process is presented in this paper, it consists of a linear interpolation of the parameters of a neural network. The developed tool examines the training process on the level of layers and individual parameters. The results obtained in the experiments confirm that the linear path of training is avoiding local optima, identifies the ambient and robust layers in the neural network and the results are consistent with the examination on the level of layers.

Petr Buchal

neuronová síť, rozpoznání textu, self-training, neanotovaná data, jazykový model

Robotika a umělá inteligence

Vytvoření kvalitního systému rozpoznání textu (OCR) vyžaduje velké množství anotovaných dat. Získání, potažmo vytvoření anotací je nákladný proces. Tato práce se zabývá využitím neanotovaných dat pro trénování OCR neuronové sítě. Navržená metoda využívající neanotovaná data spadá do kategorie self-training algoritmů. Nejprve je na omezeném množství anotovaných dat natrénován počáteční model neuronové sítě. Ten je následně spolu s jazykovým modelem použit k vygenerování několika nejpravděpodobnějších variant pseudo-štítků neanotovaných dat. Takto strojově anotovaná data jsou smíchána s trénovacími daty, která byla použita k vytvoření počátečního modelu a následně jsou využita k natrénování cílového modelu. Na ručně psaném ICFHR 2014 Bentham datasetu dosahuje nejlepší takto trénovaný model 1.99 % CER, což je relativní zlepšení o 23 % oproti počátečnímu modelu trénovaném pouze na anotovaných datech. Za pomocí navržené metody lze zvýšit úspěšnost OCR pomocí neanotovaných dat.

David Chocholatý, Lukáš Holík

Finite Automata, Product Construction, Emptiness Test, Intersection Computation Optimization, State Space Reduction, Length Abstraction

Nekonvenční výpočetní techniky Překladače a gramatiky

Finite automata are a well-known field of computational theory, and we use them widely in many situations. We will focus our attention to different heuristics for optimizing several typical problems with finite automata. We are interested especially in computation of intersection of automata product construction and its emptiness test, which is time and again required in modern computation technologies, but requires a lot of computational time and generates vast yet unnecessary so-called state space in the end. For this reason, we will try to use length abstraction for solving these problems and optimizing the product construction and its emptiness test as good as possible using solely knowledge about recognized words lengths.

Ľuboš Mjachky

Privacy Preservation, Machine Learning, Generative Adversarial Networks

Bezpečnost

Biometric-based authentication systems are getting broadly adopted in many areas. However, these systems do not allow participating users to influence the way their data are used. Furthermore, the data may leak and can be misused without the users’ knowledge. In this paper, we propose a new authentication method that preserves the privacy of individuals and is based on a generative adversarial network (GAN). Concretely, we suggest using the GAN for translating images of faces to a visually private domain (e.g., flowers or shoes). Classifiers, which are used for authentication purposes, are then trained on the images from the visually private domain. Based on our experiments, the method is robust against attacks and still provides meaningful utility.

Michal Šedý

nondeterministic finite automata, minimization, state merging, SAT solver

Testování, analýza a verifikace

Nondeterministic finite automata (NFA) are widely used in computer science fields, such as regular languages in formal language theory, formal verification, high-speed network monitoring, image recognition, hardware modeling, or even in bioinformatic for the detection of the sequence of nucleotide acids in DNA. Automata minimization is a fundamental technique that helps to decrease resource claims (memory, time, or a number of hardware components) of implemented automata. Commonly used minimization techniques, such as state merging, transition pruning, and saturation, can leave potentially minimizable automaton subgraphs with duplicit language information. These fragments consist of a group of states, where the whole language of one state is piecewise covered by the other states in this group. The paper describes a new minimization approach, which uses SAT solver Z3, which provides information for efficient minimization of these so far nonminimizable automaton parts. Moreover, the newly investigated method, which only uses solver information and state merging, can minimize automata similarly and with a transition density up to 2.5 (from each state lead approximately 2.5 transition edges) faster than a tool RABIT, which uses state merging and transition pruning.

Šimon Stupinský

automated synthesis, probabilistic programs, Markov models, model checking

Testování, analýza a verifikace

Probabilistic programs play a key role in various engineering domains, including computer networks, embedded systems, power management policies, or software product lines. This paper presents PAYNT, a tool for the automatic synthesis of probabilistic programs satisfying the given specification. It supports the synthesis of finite-state probabilistic programs representing a finite family of candidate programs. PAYNT provides a novel integrated approach for probabilistic synthesis developed on the principles of abstraction refinement (AR) and counterexample-guided inductive synthesis (CEGIS) methods. PAYNT is able to efficiently synthesise the topology of the program as well as continuous parameters affecting the transition probabilities – this is a unique feature. Existing tools for topology synthesis implement only naive approaches and thus typically do not scale to practically relevant synthesis problems. Tools leveraging search-based techniques can handle both synthesis problems, but they do not ensure the complete exploration of the design space. For challenging synthesis problems, PAYNT is able to significantly decreases the run-time from days to minutes while ensuring the completeness of the synthesis process. We demonstrate the usefulness and performance of PAYNT on a wide range of benchmarks from different application domains. Our tool paper presenting PAYNT has been recently accepted at CAV’21, an A* conference.

Dominik Harmim

Facebook Infer, Static Analysis, Abstract Interpretation, Atomicity Violation, Contracts for Concurrency, Concurrent Programs, Program Analysis, Atomicity, Atomer

Testování, analýza a verifikace

Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The first version of Atomer was proposed within the BSc thesis of the author of this paper and implemented as a plugin of the Facebook Infer framework. In this paper, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.

Filip Kočica

sklad, optimalizace, simulace, generátor, objednávka, produkt, pickování, evoluce

Robotika a umělá inteligence

Tato práce řeší problematiku alokace produktů do lokací ve skladu za pomoci moderních meta-heuristických přístupů v kombinaci s realistickou simulací skladu. Práce poskytuje grafický nástroj umožňující sestavení modelu skladu, generování syntetických zákaznických objednávek, optimalizaci alokace produktů za pomoci kombinace state of the art technik, simulátor vytvořeného modelu skladu a nakonec nástroj pro hledání nejkratší cesty objednávky skrze sklad. Práce také uvádí porovnání různých přístupů a experimenty s vytvořenými nástroji. Podařilo se optimalizovat propustnost experimentálního skladu na téměř dvojnásobek (~57%). Přínosem této práce je možnost vytvoření modelu plánovaného či již existujícího skladu a jeho simulace i optimalizace, což může značně zvýšit propustnost skladu a pomoci detekovat a odstranit vytížená místa. To může vést k ušetření zdrojů či pomáhat v plánování. Dále tato práce přináší nový způsob optimalizace skladu a nové optimalizační kritérium.

Roman Dobiáš

OpenGL, autostereoscopic display, single to multiview conversion, automated conversion, pipeline injection, API call hooking

Počítačová grafika

The adaptation of upcoming autostereoscopic displays by regular users depends on the availability of supported applications. To increase such a set, this paper describes compatibility software which turns (semi) automatically the output of regular OpenGL 3D applications to display-native output, which takes advantage of true 3D displays capabilities. This is achieved using a conversion layer that intercepts parts of OpenGL API and translates such API calls to ones that produce a multiview output of the original application.

Jiří Kutálek

Yoga Poses Detection, Video Annotation Application, Training CNN for Yoga Poses Recognition

Zpracování dat (obraz, zvuk, text apod.)

In this paper, the concept of a smartphone app detecting Yoga poses and displaying several frames to a user is presented. The goal of this project is proving that even a simple Convolutional Neural Network (CNN) model can be trained to recognize and classify video frames from a Yoga session. I created an application in which the videos are manually annotated. The data, consisting of frames captured from 162 collected videos based on the annotations, is then passed to train a CNN model. The Dataset consists of 22 000 images of 22 different Yoga poses. The frames are captured using the OpenCV library, the training process is handled by the TensorFlow platform and the Keras API, and the results are visualized in the TensorBoard toolkit. The Model’s multi-class classification accuracy reaches 91% when the binary cross-entropy loss function and the sigmoid activation function are used. Despite the experimental results are promising, the main contributions are the dataset forming tools and the Dataset itself, which both helped to confirm the proof-of-concept.

Kateřina Kunorzová

FM-CW radar, detekce parkovacích míst, zpracování signálu

Zpracování dat (obraz, zvuk, text apod.)

Cílem práce je detekovat parkovací místa a využít k tomu radarové zařízení. Radar vysílá signál a ten se následně odráží od objektů v okolí radaru a je zpět přijímán. Po zpracování je k dispozici 2D/3D point cloud (prostor kolem radaru). Propojením této informace s rychlostí vozu či GPS polohou je možné získat posun automobilu a vypočítat souřadnice bodů z okolí. Následně lze tyto body postupně ukládat a zpřesňovat tak prostor, kudy auto projíždí. Výsledkem je mapa bodů, ve které lze pomocí vhodných metod detekovat volná parkovací místa. Propojením místa s příslušným GPS záznamem je k dispozici přesná GPS poloha volného místa. Výsledkem práce je systém analyzující radarová data. Přínosný může být jako vstup pro celkový systém monitorovaní volných míst, který by řidičům jeho využíváním ušetřil spoustu času.

Oliver Rainoch

AR, Navigace uvnitř budov, Mobilní aplikace, Android, Rozšířená realita, Unity, ARCore

Uživatelská rozhraní

Tato práce se zabývá využitím rozšířené reality pro navigaci v budovách. Cílem je vytvořit mobilní aplikaci s prvky rozšířené reality pro navádění uživatele. K určení polohy jsou využity vizuální markery a technologie SLAM. Výsledná aplikace je implementována s pomocí knihovny ARCore a herního enginu Unity. Uživatel naskenuje marker, vybere hledanou místnost a pomocí plánku a šipky v rozšířené realitě je naváděn k cíli. Díky aplikaci je možné se efektivně a snadno dostat k hledané místnosti. Použité principy mohou být využity k navigování i v rozsáhlých areálech škol, společností a skladech.

Ľuboš Mjachky

Privacy Preservation, Machine Learning, Generative Adversarial Networks

Bezpečnost

Biometric-based authentication systems are getting broadly adopted in many areas. However, these systems do not allow participating users to influence the way their data are used. Furthermore, the data may leak and can be misused without the users’ knowledge. In this paper, we propose a new authentication method that preserves the privacy of individuals and is based on a generative adversarial network (GAN). Concretely, we suggest using the GAN for translating images of faces to a visually private domain (e.g., flowers or shoes). Classifiers, which are used for authentication purposes, are then trained on the images from the visually private domain. Based on our experiments, the method is robust against attacks and still provides meaningful utility.

Jan Zavřel

EIGRP, Simulation, Routing, OMNeT++

Modelování a simulace Počítačové sítě

This paper deals with the implementation and the evaluation of a simulation model of a modern dynamic routing protocol designed by Cisco Systems, Inc. called Enhanced Interior Gateway Routing Protocol (EIGRP) in a discrete simulator OMNeT++ implemented in C++. The resulting simulation model can be used to conduct various experiments which allow network designers and alike to explore the protocol's behavior in different situations inside a safe discrete environment. In order to produce a trustworthy simulation course, the protocol model must be as accurate as possible to the real implementation and thoroughly tested. This paper provides a basic overview of both protocol EIGRP and simulator OMNeT++. It also discusses the state of the model before and after the integration into a newer version of the INET framework, showcases improvements, and outlines the testing methodology.

Adam Grünwald

chytrá domácnost, chytrý bojler, chytrá zásuvka, internet věcí

Počítačová architektura a vestavěné systémy Robotika a umělá inteligence

Cílem této práce je rozšířit chytrou domácnost o chytrý bojler, který vznikne připojením stávajícího hloupého bojleru do chytré zásuvky se speciálním modulem pro připojení teplotních čidel, která slouží k monitoringu vývoje teplot v bojleru. Takto vzniklý chytrý bojler se dokáže přizpůsobit zvyklostem v domácnosti tak, aby výsledkem byla úspora elektrické energie. V rámci práce byl navržen a implementován učící se algoritmus, který vyhodnocuje nasbíraná data a na jejich základě řídí ohřívání. Vliv na ohřev vody v bojleru mají také speciálně vytvořené události v kalendáři Google, se kterým se program synchronizuje a v okamžiku, kdy je celá domácnost například na dovolené, se voda v bojleru neohřívá. Program pro sběr dat, jejich vyhodnocování a řízení ohřevu, je spuštěn v počítači připojeném v místní síti. V něm se také nachází databáze pro získaná data a nástroj, zajišťující přehled statistik bojleru jako je aktuální stav či spotřeba elektrické energie za týden. Hlavním přínosem této práce je úspora elektrické energie snížením tepelných ztrát, díky menší průměrné teplotě vody v bojleru. Ta může ročně činit až 30 % nákladů, což pro 80 litrový bojler představuje roční úsporu až 3500 Kč. Původní bojler navíc získá chytré funkce, které současné chytré bojlery nenabízejí, nebo nabízejí jen v omezené formě.

Dominik Harmim

Facebook Infer, Static Analysis, Abstract Interpretation, Atomicity Violation, Contracts for Concurrency, Concurrent Programs, Program Analysis, Atomicity, Atomer

Testování, analýza a verifikace

Atomer is a static analyser based on the idea that if some sequences of functions of a multi-threaded program are executed under locks in some runs, likely, they are always intended to execute atomically. Atomer thus strives to look for such sequences and then detects for which of them the atomicity may be broken in some other program runs. The first version of Atomer was proposed within the BSc thesis of the author of this paper and implemented as a plugin of the Facebook Infer framework. In this paper, a new and significantly improved version of Atomer is proposed. The improvements aim at both increasing scalability as well as precision. Moreover, support for several initially not supported programming features has been added (including, e.g., the possibility of analysing C++ and Java programs or support for re-entrant locks or lock guards). Through a number of experiments (including experiments with real-life code and real-life bugs), it is shown that the new version of Atomer is indeed much more general, scalable, and precise.

Šimon Stupinský

automated synthesis, probabilistic programs, Markov models, model checking

Testování, analýza a verifikace

Probabilistic programs play a key role in various engineering domains, including computer networks, embedded systems, power management policies, or software product lines. This paper presents PAYNT, a tool for the automatic synthesis of probabilistic programs satisfying the given specification. It supports the synthesis of finite-state probabilistic programs representing a finite family of candidate programs. PAYNT provides a novel integrated approach for probabilistic synthesis developed on the principles of abstraction refinement (AR) and counterexample-guided inductive synthesis (CEGIS) methods. PAYNT is able to efficiently synthesise the topology of the program as well as continuous parameters affecting the transition probabilities – this is a unique feature. Existing tools for topology synthesis implement only naive approaches and thus typically do not scale to practically relevant synthesis problems. Tools leveraging search-based techniques can handle both synthesis problems, but they do not ensure the complete exploration of the design space. For challenging synthesis problems, PAYNT is able to significantly decreases the run-time from days to minutes while ensuring the completeness of the synthesis process. We demonstrate the usefulness and performance of PAYNT on a wide range of benchmarks from different application domains. Our tool paper presenting PAYNT has been recently accepted at CAV’21, an A* conference.

Martin Dvořák

curtaining efekt, syntetické snímky curtaining efektu, konvoluční neuronová síť

Robotika a umělá inteligence

Tomografická 3D analýza v nanometrovém měřítku využívá snímky vzorků získané s využitím fokusovaného iontového svazku (FIB), při jejichž snímání ale dochází z fyzikálních důvodů k poškození "curtaining" efektem. Tento článek představuje nový přistup k odstranění curtaining efektu ze snímků pomocí strojového učení. Pro jeho odstranění je využita konvoluční neuronová síť (CNN) a technika učení s učitelem. Navržená síť pracuje s příznaky, které vytváří vlnková (Wavelet) transformace a jejím výstupem je vizuálně "vyčištěný" snímek. K učení sítě je využita syntetická datová sada poškozených snímků, které jsou vytvořeny generátorem simulujícím fyzikální proces tvorby reálného snímku. Simulace se skládá z "opotřebení" vzorku pomocí fokusovaného iontového svazku (FIB) a zobrazení povrchu pomocí skenovacího elektronového mikroskopu (SEM). Nově vytvořený přístup velmi dobře pracuje i s reálně pořízenými snímky. Kvalitativní vyhodnocení představeného řešení a srovnání s jiným řešením hodnotili laici i experti na tuto problematiku. Představené řešení představuje nový nadějný přístup k odstranění curtaining efektu a přispívá k lepšímu postupu zpracování i porozumění snímkům pořízeným při materiálové analýze.

Jakub Pojsl

Meal planner, Meal plan generator, Web application, Nutrition monitoring, Django, User interface

Uživatelská rozhraní Webové technologie

The aim of this work is design and implementation of a web-based application that helps its users to improve their eating habits and potentially contributes to the reduction of food waste. The app allows users to easily plan their meals, monitor nutrition in their diet, and automatically generate personalized meal plans according to their body predispositions, goals, and lifestyle. Most attention was given to the design and testing of a user interface that would allow users to effectively manage their meal plans.