CHESS Students' Day 2025

Talks I

Martin Kurečka
Safe Reinforcement Learning: Preventing Rogue Agents
Abstract: Reinforcement learning (RL) is a branch of machine learning where agents learn to make decisions by interacting with an environment to maximize a given reward signal. A critical challenge in RL is objective under-specification, where a single reward often fails to fully capture the true goals the agent is meant to achieve. Such gaps can lead to reward hacking, where agents find loopholes or pursue unintended strategies while still maximizing the defined reward. The talk outlines how Safe RL methods address these challenges and offers a glimpse into our lab’s work on developing more reliable, goal-aligned agents.

Martin Skalský
One Brain, Many Bodies: Universal Control for Diverse Robots
Abstract: Today, a company aiming to build a custom robot needs to spend months teaching it even the most basic movements. Now imagine achieving the same result in just minutes. My research aims to make this possible by combining modern neural network architectures with large-scale reinforcement learning to create a universal controller adaptable to various robot morphologies a user might wish to control.

Vojtěch Kůr
Multiple Mean-Payoff Optimization under Local Stability Constraints.
Abstract: The long-run average payoff per transition (mean payoff) is the main tool for specifying the performance and dependability properties of discrete systems. The problem of constructing a controller (strategy) simultaneously optimizing several mean payoffs has been deeply studied for stochastic and game-theoretic models. One common issue of the constructed controllers is the instability of the mean payoffs, measured by the deviations of the average rewards per transition computed in a finite "window" sliding along a run. Unfortunately, the problem of simultaneously optimizing the mean payoffs under local stability constraints is computationally hard, and the existing works do not provide a practically usable algorithm even for non-stochastic models such as two-player games. In this paper, we design and evaluate the first efficient and scalable solution to this problem applicable to Markov decision processes.
The talk is based on a paper presented at AAAI 2025.

Talks II

Jan Mačák
Steady-State Strategy Synthesis for Swarms of Autonomous Agents.
Abstract: Steady-state synthesis aims to construct a policy for a given MDP D such that the long-run average frequencies of visits to the vertices of D satisfy given numerical constraints. This problem is solvable in polynomial time, and memoryless policies are sufficient for approximating an arbitrary frequency vector achievable by a general (infinite-memory) policy. We study the steady-state synthesis problem for multiagent systems, where multiple autonomous agents jointly strive to achieve a suitable frequency vector. We show that the problem for multiple agents is computationally hard (PSPACE or NP hard, depending on the variant), and memoryless strategy profiles are insufficient for approximating achievable frequency vectors. Furthermore, we prove that even evaluating the frequency vector achieved by a given memoryless profile is computationally hard. This reveals a severe barrier to constructing an efficient synthesis algorithm, even for memoryless profiles. Nevertheless, we design an efficient and scalable synthesis algorithm for a subclass of full memoryless profiles, and we evaluate this algorithm on a large class of randomly generated instances. The experimental results demonstrate a significant improvement against a naive algorithm based on strategy sharing.
The talk is based on a paper presented at IJCAI 2025.

David Klaška
Patrolling as an Optimization Problem.
Abstract: Patrolling games are a special type of security games where a mobile Defender moves among vulnerable targets and aims to detect possible ongoing intrusions initiated by an Attacker. The targets are modelled as vertices in a directed graph where the edges correspond to admissible Defender’s moves. At any moment, the Attacker may choose some target and initiate an intrusion (attack). The task is to design a moving strategy for the Defender maximizing the probability of discovering an ongoing attack. In the talk, we survey recent advances in the area of patrolling games and sketch the main ideas behind the recently discovered strategy synthesis algorithms.
The talk is based on the results presented at UAI 2021, UAI 2022, and IJCAI 2023 conferences.

Jonáš Rosecký
Randomized Patrolling in Practice
Abstract: In this presentation, we will demonstrate how we integrate theoretical results of the previous presentation into practical tools, making them readily deployable. We have developed a cell phone application for patrols and a commander's control portal. We also have prototypes for editing the environment and visualizing randomized strategies. Furthermore, we are testing everything practically in cooperation with the Regional Military Command Brno.

Talks III

Juraj Major
Complementation of Nondeterministic Finite Automata Without Determinization
Abstract: Complementation of nondeterministic finite automata (NFA) is a fundamental operation in automata theory with various applications. The classical approach relies on the powerset construction to first determinize the automaton, followed by swapping accepting and non-accepting states. However, determinization may cause an exponential blow-up of the state space. In this talk, we explore novel methods for complementing NFAs without determinization: a reverse powerset complementation supported by a heuristic that chooses between traditional and reverse complementation, as well as two additional techniques for specific subclasses of NFAs. We also present an experimental evaluation of the achieved results.
This talk is based on a paper presented at FCT 2025.

David Dokoupil
Complementation of Generalized Büchi Automata
Abstract: Generalized Büchi Automata (GBAs) are a class of automata over infinite words that offer a significant advantage over standard Büchi Automata (BAs): the ability to express languages using fewer states. However, utilizing this compactness during automata operations is non-trivial. In this talk, we introduce a method to extend a standard BA complementation construction to handle generalized acceptance conditions directly. We validate our approach by comparing its performance against state-of-the-art tools.

Lea Petřivalská
Complexity of Word-Level Model Checking with Arrays
Abstract: We study the computational complexity of deciding reachability in symbolic transition systems represented in quantifier-free first-order logic with bit-vectors and arrays. It is known that without arrays, the problem is PSPACE-complete (resp. EXPSPACE-complete) if the bit-widths are encoded in unary (resp. binary). We show that the problem becomes EXPSPACE-complete (resp. 2EXPSPACE-complete in the binary case) when arrays indexed by bit-vectors are present, even if array values are limited to bit-vector sorts. Further, we show that the problem is NONELEMENTARY if we allow arrays indexed by other arrays.

Ondřej Vašíček, Jakub Němec
Event Calculus and Answer Set Programming for Analysing High-Level Requirements on Safety-Critical Cyber-Physical Systems
Abstract: The talk will present ongoing research activities devoted to using answer set programming, a form of logical programming, for formalising and analysing high-level requirements on safety-critical cyber-physical systems such as medical devices or aircraft systems. The research is done in collaboration of a number of partners including Honeywell, UT Dallas, Uni Potsdam, or Universidad Rey Juan Carlos.

Antonín Kučera
Formela Lab - Ongoing and Future Research
Abstract: A short summary of ongoing Formela research activities. The results achieved, the plans for the near future, and the call for undergraduate/PhD students.

Lunch

Talks IV

Jan Strejček, Tomáš Vojnar
AVELAB - Fresh Wind at FI 
Abstract: We shortly present current research topics of our laboratory. The topics offer subjects for bachelor's, master's, and PhD theses.

Paulína Ayaziová
Software Verification Witnesses
Abstract: Producing witnesses alongside verification results is a valuable practice in software verification. This talk will focus on a standardized format for violation witnesses (also known as counterexamples), their role in debugging, and the process of witness validation, which can automatically rule out false alarms or confirm reported bugs, thereby increasing confidence in the verification verdict.

Jindřích Sedláček
Symbolic Execution with Implicit Predicate Abstraction
Abstract: Symbolic execution is an algorithm that systematically explores all feasible program paths using an SMT solver. Predicate abstraction is a model-reduction technique that represents a large system using a finite set of predicates over the variables of the system. My talk describes an approach that combines symbolic execution with predicate abstraction and its implementation into a real symbolic executor Slowbeast.

Adéla Štěpková
Reversing Programs for Reachability Analysis
Abstract: Reachability analysis is a way to check whether a program can ever reach a certain location during its execution. This typically means checking if a program can hit an error, such as an assertion that fails. Most existing techniques do this by exploring the program from the start. However, in some cases, it can be easier to work backward from the error instead. In this presentation, we show how to automatically reverse programs so that the existing forward techniques can explore them in the backward direction.

Jiří Pavela, Zuzana Schulmeisterová
Developing Safety-Critical Code Using Rule-Based Programming
Abstract: The talk will present a novel rule-based expert system ECLEAPS intended for implementing high-level reactive control systems for safety-critical systems, e.g., from the aerospace domain – indeed, the research is conducted in collaboration with Honeywell. Moreover, newly beginning research on analysing ECLEAPS programs will be presented too.

Talks V

David Kozák, Samuel Malec
Static Analysis for Compilers of Dynamic Languages
Abstract: The talk will present novel results on points-to analyses for use in ahead-of-time compilers of dynamic languages such as Java. The results were achieved in collaboration with Oracle Labs and some of them are nowadays in everyday use worldwide within the Native Image Java compiler. Moreover, beginning works on implementing an abstract interpretation framework with the Native Image environment will be briefly presented too.

Adam Kattan Rahmani, David Kozák
Static Analysis of Microservice Systems
Abstract: The talk will present past and ongoing research efforts on using static analyses available within the GraalVM/Native Image ecosystem for analysing and visualising software based on the microservice architecture. The work is a result of collaboration of multiple partners including Baylor Uni in Texas and Arizona Uni.

Robert Vašek, Jiří Pavela
Performance Analysis of System Code in Practice
Abstract: The talk presents the Perun toolkit for collecting, versioning, analysing, and visualising data about software performance. The tool started as an academic prototype and currently is in common use by the Red Hat kernel performance team. The talk will thus also mention experience from supporting real-life performance analysis of systems code.

Tomáš Dacík, Tomáš Brablec
Separation Logic: A Novel Decision Procedure and Its Applications in Memory Safety Program Analysis
Abstract: The talk will first briefly present a novel decision procedure of a rich fragment of separation logic based on small-model properties and translation to SMT solving. Then, its application in a new prototype tool for memory safety analysis of low-level code will be mentioned too.

Robert Konicar
Points-to Analysis Using Domain-Specific Dialects
Abstract: The goal of the ongoing research that will be presented in this talk is to develop new techniques for static analysis of programs by using domain-specific intermediate program representations. The idea is that combining domain-specific representations with techniques used for program optimisations can achieve better analysis performance without losing precision.