Colloquium of Faculty of Informatics
The Informatics Colloquium takes place on Tuesday at 14:30 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:30–15:30, lecture hall A217, Faculty of Informatics Building
(informal discussion with the speaker in A220 since around 14:00)
Spring 2023 - schedule overview
On Tuesday March 28, there will be PhD Fest - a series of talks given by PhD students.
Jan Vykopal
Interactive Environments for Cybersecurity Training
Tuesday 14 February 2023, 14:30, lecture hall A217
Cybersecurity training environments enable students to complete hands-on tasks involving computer systems and networks. The design and features of the environments play a crucial role in training delivery and efficiency. In this talk, I will present the challenges of designing and using learning environments, our research effort, and practical experience in this area. In particular, I will introduce two open-source environments, KYPO Cyber Range Platform and Cyber Sandbox Creator, and their use cases for efficient student training and assessment.
Tomáš Foltýnek
Artificial Intelligence and Academic Integrity
Tuesday 21 February 2023, 14:30, lecture hall A217
The lecture touches on three areas: General ethical issues of artificial intelligence, artificial intelligence supporting academic integrity, and artificial intelligence threats to academic integrity. AI has a huge potential to detect academic misconduct, like ghostwriting, machine paraphrasing, exam impersonation, etc. On the other hand, recent advancements in language modelling, specifically GPT-3 model and its successors, allow for generating arbitrarily large texts, almost indistinguishable from texts generated by humans. Some educators perceive these technologies as a threat to essay-based student assessment. AI can produce not only natural text, but also pieces of art, or even programming assignment solutions. Academic integrity research shows that 5 - 10% of students routinely outsource their homework from their peers, relatives or even professional companies. This phenomenon, known as "contract cheating", is much more accessible with GPT. As we can’t prevent students from using them, generative pre-trained models are certainly a threat to some kinds of assessment tasks. On the other hand, it is also an opportunity to move education forward - to rethink our assessment strategies, and incorporate AI into our classes. Students should know the limits of AI-based technologies and learn how to use them ethically, in a way that improves their learning outcomes. The aim of the lecture is to initiate discussion among FI MU academics about these issues and encourage experience exchange that maintains high-quality education provided by the faculty in new circumstances.
Adam Herout
Self-Supervised Learning for Sports Pose Recognition/Classification
Tuesday 28 February 2023, 14:30, lecture hall A217
TWe intend to help athletes with correct practice in sports poses. For that, we are developing algorithms of efficient/cheap classification of sports poses in real time on mobile devices. The poses should be learned in a few-shot manner. This leads to exploration of self-supervised learning methods and specific datasets and their processing. The talk might be interesting not only for someone interested in sports data processing, but for anyone interested in deep learning, few-shot learning and self-supervised learning.
Nysret Musliu
Machine Learning for Automated Algorithm Design and Selection
Tuesday 7 March 2023, 14:30, lecture hall A217
Solving techniques usually give different results for different classes of optimization problems. The Algorithm Selection Problem addresses the problem of determining which of the available algorithms is most appropriate to solving a particular problem instance. Hyper-heuristics are an example of a high-level problem-independent approach. The aim of hyper-heuristics is to automate the design of heuristic methods based on combination and selection of low-level heuristics.
Recently, several methods have been proposed that use machine learning techniques for automated algorithm selection and heuristic algorithm design. In this talk, we will present our work on algorithm selection for various problem domains, including scheduling, tree decomposition, and other optimization problems. We will also discuss recent advances in automated heuristic algorithm design and present the successful application of novel hyper-heuristic approaches.
Jana Tůmová
Formal methods for robot planning
Tuesday 14 March 2023, 14:30, lecture hall A217
As autonomous robots move from enclosed, controlled environment to our everyday lives, we ask: How can we ensure that they work as expected and how can we even specify what it means to work as expected? Formal methods have shown to be useful in addressing these questions; temporal logics provide rich, rigorous, yet user-friendly specification formalism and formal synthesis offers a way to automatically generate a plan or a controller that provably satisfies the specification (or satisfies it to some guaranteed extent).
This talk will introduce the basic principles of formal methods for robot planning, discuss its benefits, and outline open challenges. We will discuss how to express sophisticated motion planning goal and constraints in temporal logics, and how to integrate them into sampling-based motion planning algorithms. We will specifically focus on using Signal Temporal Logic (STL) as a powerful specification language with quantitative semantics and discuss what provable guarantees the planning algorithms can provide. Throughout the talk, we will showcase robotics applications, such as autonomous driving and exploration of unknown environments with UAVs.
Dirk Beyer
Benchmarking in Computer Science and Competition on Software Verification
Tuesday 21 March 2023, 14:30, lecture hall A217
This lecture will cover two topics, benchmarking and SV-COMP. Benchmarking is a widely used method in experimental computer science, in particular, for the comparative evaluation of tools and algorithms. As a consequence, a number of questions need to be answered in order to ensure proper benchmarking, resource measurement, and presentation of results, all of which is essential for researchers, tool developers, and users, as well as for tool competitions. We identify a set of requirements that are indispensable for reliable benchmarking and resource measurement of time and memory usage of automatic solvers, verifiers, and similar tools, and discuss limitations of existing methods and benchmarking tools. Fulfilling these requirements in a benchmarking framework can (on Linux systems) currently only be done by using the cgroup and namespace features of the kernel. We developed BenchExec, a ready-to-use, tool-independent, and open-source implementation of a benchmarking framework that fulfills all presented requirements, making reliable benchmarking and resource measurement easy. Our framework is able to work with a wide range of different tools, has proven its reliability and usefulness in the International Competition on Software Verification, and is used by several research groups worldwide to ensure reliable benchmarking. Finally, we present guidelines on how to present measurement results in a scientifically valid and comprehensible way.
The second part of the lecture will give an overview of the competition on software verification, including itssetup and execution,as well as its effort to standardize the process of software verification. Results of the verification processare written in a standard exchange format for verification witnesses. We present the idea of witness-based result validation, and a few other applications for which verification witnesses are a useful exchange format.
Ján Jančár
Securing cryptographic implementations against advanced attackers
Tuesday 28 March 2023, 14:30, lecture hall A217
Cryptography secures critical aspects of society. Whether used by a whistle-blower under a repressive regime in an end-to-end encrypted messaging application or a user paying for a product online. Both of these users have assumptions of confidentiality, integrity, and authenticity, which are provided in part by cryptography implemented in software and hardware. Cryptography is complicated, combining aspects of information theory, algebra, and number theory to form primitives, protocols, and systems. Cryptographic primitives rarely break in theory, with the security of the RSA cryptosystem still strong against classical computers decades after its introduction, while their implementations break much more often.
In this talk, we will look at several examples of vulnerabilities in cryptographic implementations from a high-level standpoint. I will present a discovery of a group of timing attack vulnerabilities in implementations of ECDSA signing. We will study primality testing on black-box devices in an adversarial setting. We will unify several side-channel attacks on ECDH, which allows us to mount them more generally. Finally, I will present a study on the views and experiences of cryptographic library developers towards timing attacks and tools for verification of constant-timeness.
Kristýna Pekárková
Preconditioners for Matrix Sparsity
Tuesday 28 March 2023, 15:00, lecture hall A217
Integer programming (IP) is a fundamental problem of discrete optimization. The problem is both of theoretical and practical importance -- its notable applications can be found, for example, in scheduling, string algorithms and computational social choice. Integer programming is one of Karp's original 21 NP-complete problems, however, there exist cases for which the problem becomes efficiently solvable. Recent research in the area of combinatorial optimization and parameterized complexity shows that integer programming is tractable when the input instance has a certain block structure or the constraint matrix is sparse. However, most existing IP algorithms require the constraint matrix to already be in a block-like or sparse form, which is limiting for instances that are not initially sparse but can be transformed to an equivalent sparser form. The procedure of transforming a given instance to a more tractable instance is called a preconditioner. In this talk, we will discuss the existence and efficient computability of preconditioners to matrix sparsity.
Lukáš Holík
String Constraint Solving via Automata
Tuesday 4 April 2023, 14:30, lecture hall A217
String constraint solving has most applications in verifications of programs manipulating strings, e.g., in analysing security of web applications or of access policies of cloud service providers. In the last two decades, string solving has evolved into a highly competitive area, with dozens of competing approaches and tools, dominated by industrial grade SMT solvers such as Z3 or CVC5.
In the talk, I will overview the field and present some of our recent results on making string solving efficient with finite automata, achieved as a part of a broader effort directed towards showing that finite automata technology can be practical.
Petr Novotný
Static Analysis of Termination and Safety Properties in Probabilistic Programs
Tuesday 11 April 2023, 14:30, lecture hall A217
String constraint solving has most applications in verifications of programs manipulating strings, e.g., in analysing security of web applications or of access policies of cloud service providers. In this talk, we will explore the intersection of formal methods and probabilistic programing, focusing on proving temporal properties of probabilistic programs. To establish the context for our investigation, we will begin with a brief historical overview of termination proving for non-probabilistic programs, tracing its roots back to the foundational work of Turing. We will then introduce probabilistic programs and discuss their growing range of applications in computer science, ranging from computational finance and cybersecurity to various areas of machine learning and AI.
The core of the talk will be a presentation of the speaker's research contributions to formal analysis of probabilistic programs. These revolve around the usage of martingales, a powerful concept from probability theory. We will present the contributions within a broader context, highlighting the challenges that differentiate the probabilistic setting from the non-probabilistic one. Finally, we will explore potential future directions for formal reasoning about probabilistic programs, such as the application of program analysis techniques for better understanding of models employed in machine learning.
Radu-Cristian Curticapean
Counting (with) homomorphisms
Tuesday 18 April 2023, 14:30, lecture hall A217
n recent years, homomorphism counts between graphs were studied in different subfields within theoretical computer science: From a complexity theoretic point of view, it was shown that various counting problems can be understood well by expressing them as linear combinations of homomorphism counts. Such linear combinations enjoy the exceptional and very useful "monotonicity property" of being exactly as hard to compute as their hardest terms. Since the complexity of computing the individual terms, i.e., of counting homomorphisms, is reasonably well understood, this strategy allowed the community to make significant progress in the study of the complexity of various counting problems arising in database theory and network sciences.
From a more abstract perspective, the numbers of homomorphisms between graphs encode valuable information. For example, a classical result by Lovász shows that homomorphism counts from all graphs into a given graph G identify G up to isomorphism. Restricting the class of graphs from which homomorphisms are counted gives rise to natural relaxations of graph isomorphism that are connected to the expressiveness of logics.
In this self-contained talk, we survey recent developments in the study of computational and abstract properties of homomorphism counts.
Piotr Sankowski
Optimizing IVF Treatment with AI
Tuesday 25 April 2023, 14:30, lecture hall A217
AI-powered applications have the potential to vastly improve medical care. The path to this revolution is still rather long and still has some obstacles. However, one of the areas of medicine that sees more and more progress with respect to application of AI is IVF treatment. This follows as the IVF process offers unique, controllable and reputable conditions. These opportunities are further strengthened by the fact that over 10% of the human population will encounter reproduction problems, thus In Vitro Fertilization is becoming one of the fastest growing areas of healthcare. In this talk, I will present our deep learning tools that support doctors in IVF treatment. First, I will talk about EMBRYOAID: an analytical and predictive system based on deep learning computer vision algorithms. This tool aims for fully automated identification of the highest quality embryos based on a large collection of time-lapse photos of human embryos. Second, I will talk about FOLLISCAN which is an analytical and predictive system supporting healthcare practitioners in ovarian monitoring ultrasound. Identifying, calculating and measuring of follicles is of major importance for IVF, e.g., it helps estimate the ovarian reserve as well as the timing of the whole process.
Both tools are designed for fertility clinics, diagnostic centers and hospitals and will respond to their well-identified needs. In this talk, we will describe the process of building these AI-driven solutions and show the most important issues for creating a solution based on deep learning in a medical context. Finally, I will talk about deployment of these tools in fertility clinics in Poland and abroad.
Matěj Lexa
How sequence repeats in genomes complicate life - solutions out in the wild, in biology and bioinformatics
Tuesday 2 May 2023, 14:30, lecture hall A217
The fact that genomes of higher organisms contain thousands, or even millions of copies of essentially the same elements is increasingly becoming a topic in modern biology. Their presence has initially been underrated, the sequences being at times dismissed as “junk DNA”. While everyone, even the biggest skeptics had to acknowledge their presence and deal with them in the age of genomics and massive DNA sequencing, the organisms themselves have been evolving for hundreds of millions of years to deal with what was at the same time a curse and a blessing. Some repetitive sequences served as an evolutionary building material for what later became crucial components of living systems, such as chromosome structure, vivipary, molecules of the vertebrate immune system, or gene regulatory molecules and sequences. Others were silenced to form less active domains of the cell nucleus.
The branch of bioinformatics that studies DNA sequence analysis and methods for genome assembly and annotation has been particularly affected by repetitive sequences. Almost all of the missing patches in published reference genomes today are due to the presence of repeated sequences and the difficulty of assembling them properly from genomic data. Even when identified, the sequence repeats are notoriously difficult to classify and organize for further use or visualization.
In my talk, I will present some of the historical and biological context for the most interesting research on repeats in genomics and bioinformatics. I will also present some of my own research in this area, culminating in the development of computational tools (TE-greedy nester or HiC-TE) to better deal with the complexity of repetitive sequences.
Kamila Urban
Metacognition within self-regulated learning
Tuesday 9 May 2023, 14:30, lecture hall A217
Self-regulated learning (SRL) has become one of the most important areas within educational psychology research. In SRL, the learner becomes an active actor in their own learning process. The student sets their own learning goals, directs their own cognitive effort, applies specific learning strategies to the learning context, and metacognitively monitors and regulates their learning process. SRL includes cognitive, metacognitive, motivational, and emotional components. In my talk, I will specifically focus on metacognition, which is one of the key facets in predicting effective learning. Metacognition refers to knowledge of one's own cognitive processes and the monitoring and regulation of those processes. Although in SRL the student takes control of their own learning, a teacher is still required to help students develop their skills and adopt efficient learning strategies, modelling the proper strategy use and providing feedback. Therefore, the lecture will focus on the role of metacognitive skills in SRL, the effective use of learning strategies in students, and the support that teachers can provide in SRL settings.
Past colloquia
Spring 2022
Autumn 2021
Spring 2021
Autumn 2020
Spring 2020
Autumn 2019
Spring 2019
Autumn 2018
Spring 2018
Autumn 2017
Spring 2017
Autumn 2016
Autumn 2015
Spring 2015
Autumn 2014
Spring 2014
Autumn 2013
Spring 2013
Autumn 2012
Spring 2012
Autumn 2011
Spring 2011
Autumn 2010
Spring 2010