In this habilitation lecture, we will be looking at a historical overview of software reliability engineering. While reliability is a key quality of software systems, in recent years there has been a focus shift towards software resilience. In this lecture, we will delve into three main areas. First, we will discuss software reliability growth models, historical models to predict software failures based on testing efforts. Next, we will discuss software quality models proposed over time to control and reduce software defects, leading to fewer failures. Finally, we will explore current trends for building resilient software systems capable of withstanding failures and providing self-healing capabilities.

In this talk, I will demonstrate the importance of code transformations focusing on decreasing its runtime by better hardware utilization. We start with the naive C implementation of an algorithm used in scientific computing, which does not take into account the properties of modern hardware. Then, I introduce some features of modern processors (caches, vector instructions, limitations of multithreading) and make changes in the code to reflect those features. Finally, I will show how to transform the code to GPUs and get even more performance, presenting our work pushing the state-of-the-art.

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.

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.

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.

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.

The live stream will be broadcasted here.

Now that we’re putting software and network connections into durable safety-critical goods such as cars and medical devices, we’ll have to patch vulnerabilities, as we do with phones and laptops. But we can't let vendors stop patching after three years! So last year, the EU passed Directive 2019/771, which gives the right to software updates for goods with digital elements, for the time period the consumer might reasonably expect. In my talk, I'll describe the background, including a study we did for the European Commission in 2016, and the likely future effects. As sustainable safety, security and privacy become a legal mandate, this will create real tension with existing business models and supply chains. It will also pose a grand challenge for computer scientists. What sort of tools and methodologies should you use to write software for a car that will go on sale in 2023, if you have to support security patches and safety upgrades till 2043?

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.

The live stream will be broadcasted here.

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).

The live stream will be broadcasted here.

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.

The live stream will be broadcasted here.

Human motion can be digitized using various capturing technologies into a discrete sequence of 3D skeleton configurations. Recognizing the type of performed actions in such spatio-temporal data is a desired task for a wide range of application domains. However, solving this task is difficult as the actions of the same type can be performed by different subjects in various styles, speeds, and initial body postures. In this talk, we will present fundamental action-recognition principles based on nearest-neighbor and deep-learning classifiers and discuss their advantages and disadvantages.

The live stream will be broadcasted here.

We discuss the expressivity of finite automata whose transition diagram contains no nontrivial cycles, show their relationship to the Straubing-Therien concatenation hierarchy, and discuss the complexity of related problems, including universality, inclusion, and equivalence.

The live stream will be broadcasted here.