Program

Petr Dobeš

3D Reconstruction, Structure from Motion, Traffic Surveillance, Traffic Analysis, Camera Calibration

Zpracování obrazových dat

This paper reports experiments focusing on 3D reconstruction of vehicles passing in front of a traffic surveillance camera. Calibration process of surveillance camera is first introduced and the relation of automatic calibration with 3D information about observed traffic is described. Afterwards, a set of experiments with feature matching and Structure from Motion algorithm are presented and their results on images of passing vehicles are examined. Modifications to the correspondence search stage of Structure from Motion pipeline are then proposed. Most importantly, instead of using SIFT features, DeepMatching algorithm (originally devised to find quasi-dense point matches in optical flow calculation) is used to obtain point correspondences for subsequent reconstruction phase. As a result of implemented modifications, the overall completeness of reconstructed point cloud model of passing vehicle has improved significantly.

Ondřej Valeš

digitální fotografie, rekonstrukce, hloubková mapa, deskriptor GIST, Poissonova rovnice, dataset, C++, OpenCV

Robotika a umělá inteligence

Cílem této práce je navrhnout postup, který bude provádět rekonstrukci digitálních fotografií na základě vyhledání podobných fotografií v datasetu, jejichž obsah je poté využit při rekonstrukci. K nalezení podobnosti je navrhnut deskriptor fotografií obohacený o informaci z hloubkové mapy, který umožňuje rychlé vyhledání fotografií v datasetu a nový postup vkládání dat do rekonstruované oblasti, která je na rozdíl od existujících přístupů nejprve rozdělena na podoblasti na základě analýzy hloubkové mapy. To umožňuje řešit rekonstrukci jednotlivých podoblastí zcela odděleně a přináší zlepšení výsledku rekonstrukce, protože podoblasti jsou menší a méně komplexní.

Viktor Malík

formal verification, 2LS, template-based analysis, shape analysis, linked lists, pointer access paths, abstract interpretation, SSA form, invariant inference

Formální metody

Many low-level programs work with dynamic data structures on the heap (such as linked lists), which are often a source of bugs. Formal analysis of the shape of these structures can help finding errors or, on the contrary, prove the correctness of a program. We present the main principles behind 2LS, a program analysis framework for C programs, which is based on automatic invariant inference using an SMT solver, and a sketch of a solution that we proposed to the integration of shape analysis into this framework. The proposed solution includes a way how the shape of a program heap can be described using logical formulae and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, such as the fact that the shape of a linked list does not change after performing an operation that traverses the list and writes data into each node.

Vojtěch Havlena

Automata reduction, Language distance, Finite automaton, Network traffic monitoring

Formální jazyky a automaty

The focus of this paper is the comparison of languages and reduction of automata used in network traffic monitoring. We propose several approaches for approximate (language non-preserving) reduction of automata and comparison of their languages. The reductions are based on either under-approximating the languages of automata by pruning their states, or over-approximating the language by introducing new self-loops (and pruning redundant states later). Our approximate reduction methods and the proposed probabilistic distance utilize information from a network traffic. We give formal guarantees with respect to a model of network traffic, represented using a probabilistic automaton. We implemented the methods and evaluated them on automata used in network traffic filtering.

Tomáš Vlk

Android, Firebase, Poloha, Geofence, Sdílení

Uživatelská rozhraní

Cílem této práce je vytvořit uživatelsky přívětivou mobilní aplikaci, díky níž bude snazší sdílet svoji polohu a zároveň zachovat své soukromí. Toho je dosaženo sdílením pouze informace o přítomnosti na místě místo GPS souřadnic aktuální polohy. Pro snazší sdílení nabízí aplikace automatickou detekci přítomnosti na určitém místě, řešenou pomocí GeofencingApi. Jako cílová platforma této aplikace byl zvolen systém Android. Ke komunikaci mezi zařízeními se využívá Firebase Cloud Messaging. Výsledkem práce je, že s mírnými úpravami funguje GeofencingApi spolehlivě a lze určit přítomnost zařízení na místě s poloměrem větším než 50 metrů. Zároveň ale nedochází k aktivnímu dotazování polohy. Podařilo se tak vytvořit aplikaci, která nemusí být vůbec spuštěna (ani žádná její služba na pozadí) a přitom dokáže detekovat přítomnost zařízení na určitém místě a přijímat zprávy od ostatních zařízení. Největší předností tohoto přístupu je velmi nízká spotřeba energie oproti jiným řešením.

Daniel Čejchan

programming language, CTFE, code hatching, compile time, metaprogramming, ctime, Beast

Programovací jazyky a překladače

This paper introduces a new compiled, imperative, object-oriented, C-family programming language, particularly inspired by C++ and D. Most notably, the language implements a new concept called code hatching (also a subject of this paper) that unifies templating, compile-time function execution, compile-time reflection and metaprogramming in general. The project also includes a proof-of-concept open-source compiler (more precisely transcompiler to C) called Dragon that demonstrates core elements of the language and the code hatching concept.

Lukáš Kraicinger, Libor Danda

CNC stroj, výroba ozubení, prototyp, frézování, elektronika, software

Počítačová architektura a vestavěné systémy

Projekt se zabývá návrhem a následnou tvorbou prototypu šestiosého multifunkčního zařízení na výrobu ozubení. Jedná se o komplexní týmový projekt rozdělený na dvě části, každá část je jedna diplomová práce. Jedna z pohledu konstrukce mechanické stránky stroje a druhá z pohledu elektroniky a řídícího softwaru. Konstrukce stroje je navržena kompletně od začátku Liborem Dandou z Fakulty strojního inženýrství (Ústav konstruování). Elektroniku a řídící software vytváří Lukáš Kraicinger z Fakulty informačních technologií. Řídící software v sobě integruje specifickým CAM (Computer Aided Manufacturing) systémem, což snižuje další náklady na obslužný software. Stroj je kompaktní automat (vše v jednom), který pro výrobu ozubení potřebuje pouze vhodný polotovar a základní parametry ozubení. Hodnoty se zadávají pomocí dotykového displeje přímo na stroji nebo lze výrobu připravit pomocí stejného softwaru na pracovním PC bez stroje. Hlavní výhodou stroje je zjednodušení a zrychlení výrobního procesu a trojnásobné zvětšení pracovního prostoru stroje oproti velikostně srovnatelným strojům na trhu. Další z výhod je snížení energetických nároků na výrobu.

Martin Vondráček

Man-in-the-Middle attack, accessing secured wireless networks, password cracking, dictionary personalization, tampering network topology, impersonation, phishing

Bezpečnost Počítačové sítě

Widely used network technologies and principles of wireless security suffer weaknesses that can be exploited to perform the Man-in-the-Middle attack, allowing to eavesdrop or to spoof the network communication. The work focuses on possibilities of automation of the attack with a utilization of available specialized tools. The outcome of the research is the wifimitm package and the wifimitmcli CLI tool, both implemented in Python. The emphasis was placed on possibilities of further incorporation of the developed tool. The package provides functionality for automated MitM attack and can be used by other software. The wifimitmcli tool is capable of performing a successful fully automated attack without any intervention from an attacker. This research can be used for automated penetration testing and forensic investigation. Finally, a popularization of the fact that such severe attacks can be successfully automated should be used to raise the public awareness about the information security. In these days, this issue involves almost every one of us.

Mário Kuka

DCPro, (D)DoS Protector, COMBO, CESNET, hardvérová akcelerácia, FPGA, vysokorýchlostné siete, 100 Gbps

Počítačová architektura a vestavěné systémy Počítačové sítě

Táto práca sa zaoberá vývojom firmvéru hardvérovej akcelerácie pre zariadenie na ochranu pred amplifikačnými (D)DoS útokmi. V dnešnej dobe sú útoky typu (D)DoS veľmi rozšírené a zapríčiňujú nemalé finančné škody. Cieľom je preto vytvoriť cenovo dostupné a ľahko nasaditeľné centralizované zariadenie na riešenie daného problému. K dosiahnutiu tohto cieľu využíva zariadenie hardvérový akcelerátor umožňujúci spracovávať vysoké dátové prenosy prostredníctvom jedného, bežne dostupného, serveru. Návrh a implementácia firmvéru je uskutočnená s ohľadom na použitie zariadenia v sieťach s rýchlosťami 100\,Gbps. Celý systém prešiel funkčnou verifikáciou a v rámci laboratórneho testovania bola overená jeho reálna priepustnosť. Vytvorené zariadenie je aktuálne nasadené v sieťovej infraštruktúre CESNET a testované sieťovými administrátormi. Na základe spätnej väzby bude na vytvorenom zariadený pokračovať ďalší vývoj zameraný na rozširovanie detekcie o ďalšie typy útokov. O zariadenie aktuálne prejavili záujem aj niektorí z českých komerčných poskytovateľov sieťových služieb.

Matěj Šoc

Spotřeba paliva, Průtokoměr, Arduino

Počítačová architektura a vestavěné systémy

Tato práce se zabývá návrhem a implementací systému pro měření a profilování spotřeby paliva motocyklu v závislosti na zeměpisné poloze. Systém byl implementován na desce Arduino MEGA 2560. K měření spotřeby je použit palivový průtokoměr, tudíž je navržený systém použitelný pro jakýkoli motocykl. Součástí systému je také aplikace, která uživateli nabízí přehlednou interpretaci naměřených dat. Navržený systém provádí přesná měření spotřeby paliva a rychlosti. S drobnými úpravami může být uveden do praxe.

Václav Stránský

detekce obsazenosti parkoviště, detekce automobilů, hluboké neuronové sítě, model pozadí

Zpracování obrazových dat

Práce se zabývá návrhem a implementací robustního systému pro analýzu obsazenosti jednotlivých parkovacích míst na parkovišti ze záznamů z více-kamerového systému s možností překryvu mezi kamerami. Systém je navržen a implementován v Robotickém operačním systému (ROS) a jeho jádro se skládá ze dvou oddělených klasifikátorů. Úspěšnější, avšak pomalejší, je detekce pomocí hluboké neuronové sítě. Rychlou interakci řeší méně přesný klasifikátor pohybu s modelem pozadí. Systém je schopen fungovat v reálném čase, a to na grafické kartě i na procesoru. Úspěšnost systému na testovací datové sadě z reálného provozu jednoho parkoviště přesahuje 93%. Ke konceptu chytrých měst neodmyslitelně patří efektivní parkovací řešení stavící na znalosti obsazenosti jednotlivých parkovacích míst. Tato práce popisuje právě takový systém, který výrazně usnadní orientaci na parkovišti, a to s velmi dobrou úspěšností.

Roman Andriushchenko

Markov models, probabilistic model checking, approximation techniques, adaptive aggregation

Modelování a simulace Formální metody

Markov models are widely used in many areas of science and engineering in order to evaluate the probability of certain events of interest. Quantitative analysis of such models typically proceeds through numerical methods or simulation-based evaluation. Since the state space of the models can often be large, several approximation techniques have been proposed. For various systems, level of precision affects the soundness of verification results, so accurate quantification of approximation error is crucial. In this work we focus on adaptively-driven aggregation technique and evaluate its key performance aspects. The key contribution of this work is improving aggregation strategy and the theoretical bounds on the approximation error. Our technique leads to up to 3 orders of magnitude precision improvement over existing methods and allows one to analyse larger models with a higher accuracy.