Colloquium of Faculty of Informatics

The Informatics Colloquium takes place on Tuesday at 14:00 during the term time. The aim of the colloquia is to introduce state of the art research from all areas of computer science to the wide audience of the Faculty of Informatics.

Time and place

Tuesday 14:00–15:00, lecture hall D2, Faculty of Informatics Building

Spring 2022 – schedule overview

Feb 22 Vít Nováček (Masaryk University) A Journey in Biomedical Discovery Informatics: From Ontology Learning to Knowledge Graph Embeddings
Mar 1 Łukasz Chmielewski (Masaryk University and Radboud University) Practical Side-Channel Attacks on Public-Key Cryptosystems
Mar 15 Jan Strejček (Masaryk University) Binary decision diagrams for deciding satisfiability of bitvector formulae and DQBF
Mar 29 Jan Křetínský (TU Munich) A story of checking LTL models
Apr 5 Pavel Surynek (Czech Technical University) Multi-agent Path Finding: from Puzzles to Warehouse Logistics
Apr 12 Dan Sýkora (Czech Technical University) From 2D Sketch to 3D Animated Character via Quadratic Programming
Apr 19 Jan Šedivý (Czech Technical University) Alquist the social bot
Apr 26 Anton Nekrutenko (Penn State) Addressing computational challenges of global health emergencies with community supported systems
May 3 Stanislav Živný (Oxford) Power of convex relaxations in discrete optimisation
May 10 Stanislav Sobolevsky (Masaryk University) Urban Network Analysis: from Traditional Network Science to Graph Neural Networks

Vít Nováček (Masaryk University):
A Journey in Biomedical Discovery Informatics: From Ontology Learning to Knowledge Graph Embeddings

Tuesday, 22 February 2022, 14:00, lecture hall D2

The talk will offer a crash course in biomedical discovery informatics. By and large, discovery informatics is a research discipline that addresses the information overload problem in science. More specifically, discovery informatics tries to come up with efficient ways of acquiring, integrating, organising, augmenting and utilising information and knowledge from data sets that are typically large, heterogeneous, poorly structured, fast-evolving, unreliable—or, in other words, realistic.

The information overload is arguably relevant to virtually any human activity these days. However, it is particularly pertinent to life sciences. This motivates the specific instances of the information overload problem that will be addressed in the talk: 1) The vast breadth and depth of published life science articles that can hardly be utilised in a focused and exhaustive manner. 2) The largely untapped potential of networked biomedical data for making semi-automated discoveries.

The presented approach to tackling the first challenge is based on advances in ontology learning from text. The other group of approaches to be introduced addresses the second challenge by means of relational machine learning, applied to link prediction in networked biomedical data. The talk will then conclude with an overview of two ongoing projects that explore clinical applications of the presented techniques.

Łukasz Chmielewski (Masaryk University and Radboud University):
Practical Side-Channel Attacks on Public-Key Cryptosystems

Tuesday, 1 March 2022, 14:00, lecture hall D2

This presentation covers the topic of the side-channel analysis (SCA) of public-key cryptographic implementations, in particular Elliptic Curve Cryptography (ECC) and Rivest-Shamir-Adleman (RSA) schemes. SCA is a relatively new research area in applied cryptography that has continuously gained prominence since the late nineties. It considers adversaries leveraging the physical aspect of actual devices running cryptographic implementations.

The goal of the talk is to present how in the recent 20 years new public-key implementations protected with new SCA countermeasures lead to more sophisticated SCA attacks (and vice versa).

Firstly, I introduce how classical vertical attacks (for example, Simple Power Analysis and Differential Power Analysis) work against public-key implementations. Secondly, I explain the limitations of such attacks when applied to RSA (or ECC) implementations protected with various SCA countermeasures. Thirdly, I describe more modern attacks, in particular horizontal attacks, how they work and what are their limitations. Subsequently, we concentrate on the state-of-art attacks including both supervised approaches (like Template and Deep Learning Attacks) and unsupervised ones (based either on clustering or Deep Learning). All concepts are given in historical context and illustrated by practical examples. Finally, I am going to shortly talk about my current (and future) research on SCA.

Jan Strejček (Masaryk University):
Binary decision diagrams for deciding satisfiability of bitvector formulae and DQBF

Tuesday, 15 March 2022, 14:00, lecture hall D2

Many efficient methods and tools for analysis or synthesis of computer systems rely on satisfiability solvers for formulae of bitvector theory. We explain basics of this theory and sketch some applications of the corresponding satisfiability solvers. Then we recall the concept of binary decision diagrams (BDDs) and explain how BDDs can be used to decide satisfiability of bitvector formulae. Further, we present some techniques that improve the performance of our BDD-based satisfiability solver Q3B. Finally, we briefly present another BDD-based solver DQBDD, which can solves satisfiability of quantified Boolean formulas with explicit dependencies (DQBF).

Jan Křetínský (TU Munich):
A story of checking LTL models

Tuesday, 29 March 2022, 14:00, lecture hall D2

Linear temporal logic (LTL) belongs to the most popular formalisms for specification of dynamic systems. Assuring that a safety-critical system behaves correctly can thus be formalized as the problem of LTL model checking, i.e., deciding whether an LTL formula is satisfied by the given system. Both the satisfaction definition and the techniques used in model checking differ depending on the type of the system. Nevertheless, a surprising commonality of most of the solutions is resorting to automata theory. In this talk, we survey the LTL model checking problems, focusing on the automata-theoretic solution approach. In particular, we highlight some of the recent advances for more complex systems, where the notion of determinism of automata plays a crucial role.

Pavel Surynek (Czech Technical University):
Multi-agent Path Finding: from Puzzles to Warehouse Logistics

Tuesday, 5 Apr 2022, 14:00, lecture hall D2

The task in multi-agent path finding (MAPF) is to find discrete collision-free paths that navigate agents from their initial positions to the specified goal positions. A number of real-life problems can be modeled as MAPF, among which is probably the most prominent warehouse robotization, where agents are represented by mobile robots transporting goods within the warehouse. We will show possible approaches to solving the MAPF problem, especially approaches based on problem compilation into propositional logic and lazy compilation approaches. We will also discuss generalizations of the discrete variant of the MAPF problem, such as the variant with continuous time.

Dan Sýkora (Czech Technical University):
From 2D Sketch to 3D Animated Character via Quadratic Programming

Tuesday, 12 Apr 2022, 14:00, lecture hall D2

Creating 3D characters known from famous animated movies is a complex process requiring tedious modeling and a specification of animation rig. Skilled artists usually need several weeks to turn an initial sketch into an animation-ready 3D model. Their dream is to have a tool that will significantly speed up this workflow and allow rapid prototyping. In this talk, we present a brief survey of methods that try to fulfill this dream and describe a recently published algorithm called Monster Mash. Its key advantage is that it requires only one 2D sketch with depth ordering constraints from which it can instantly produce a consistent 3D model that is ready for animation. All this is feasible thanks to a novel rigidity-preserving layered deformation model formulated as a quadratic program that jointly inflates and deforms the 3D mesh to satisfy ordering and positional constraints. The benefits of this new model will be demonstrated in numerous practical examples.

Jan Šedivý (Czech Technical University):
Alquist the social bot

Tuesday, 19 Apr 2022, 14:00, lecture hall D2

Human-like dialogue with artificial intelligence is still elusive. Why? Simple. We’re not there yet. Fifty years after 2001: A Space Odyssey, and forty years after Star Wars, the gap between that level of dialogue and “Alexa - play Spotify” is still a quantum leap. But voice and speech remain the most natural prerequisites for human communication.

The presentation will describe the Alquist social chatbot designed by the Czech Technical University team of students. Alquist carries an engaging and entertaining conversation on popular topics such as sports, celebrities, movies, etc. Alquist relies on AI algorithms processing natural language. The presentation will explain the basics of Conversational AI architecture and technologies.

Anton Nekrutenko (Penn State):
Addressing computational challenges of global health emergencies with community supported systems

Tuesday, 26 Apr 2022, 14:00, lecture hall D2

COVID-19 pandemic is the first global infectious disease crisis coinciding with nearly universal availability of low cost sequencing resulting in ~10 million SARS-CoV2 viral genomes. While these numbers underscore the sheer scale of the worldwide biomedical research enterprise, they also expose scientific and infrastructural challenges in responding to global health emergencies. A closer look at the COVID-19 publications shows that there are no uniform practices for even foundational analyses, such as genome assembly or variant identification. The volume of existing sequence data is so massive that existing tools simply do not scale, even when deployed on the appropriate computational infrastructure, which, in turn, is only accessible to a small fraction of researchers at superbly resourced institutions. In this talk I will describe approaches that would address (1) lack of best practices for primary analyses, (2) limited scalability of analysis tools, and (3) sparse access to appropriate computational infrastructure.

Stanislav Živný (Oxford):
Power of convex relaxations in discrete optimisation

Tuesday, 3 May 2022, 14:00, lecture hall D2

Which discrete optimisation problems can be solved efficiently and why? My research is concerned with designing efficient algorithms and finding the exact borderline of tractability. For a broad class of computational problems, known as constraint satisfaction problems (CSPs), we now have a good understanding of this fundamental question.

In this talk I'll survey my work on the power of convex relaxations for constraint satisfaction problems.

Stanislav Sobolevsky (Masaryk University):
Urban Network Analysis: from Traditional Network Science to Graph Neural Networks

Tuesday, 10 May 2022, 14:00, lecture hall D2

This big urban data creates fresh opportunities to gain an unparalleled understanding of complex urban systems and respond to urban challenges, mitigating unwanted exposures and optimizing urban operation through smart digital solutions. While recent network analysis and AI techniques help address the complexity and interconnectedness of the urban data. I will introduce the spectrum of techniques from traditional network analysis to graph neural networks used by my teams at NYU and MIT to study the spatio-temporal transactional data on human mobility and interactions, as well as their applications to smart urban planning, transportation innovation, and urban analytics. We shall also discuss a concept of hierarchical graph neural networks – a novel fusion of network science and deep learning techniques our team at Masaryk University is developing, as well as its applications to predictive modeling and detection of patterns, impacts, and emergent phenomena in spatio-temporal networks of urban activity and/or quantifying populational exposure to urban stressors.

Past colloquia