Open Science: From Principles to Daily Research Practice

This session briefly introduces key elements of open science in everyday research practice, including open licenses, trusted repositories, and the main differences between institutional and disciplinary repositories. It also addresses research data management, with a focus on data management plans and practical support through tools such as the Data Stewardship Wizard. The session concludes by outlining the types of open science support available at university and faculty level and where researchers can seek practical guidance.

The slides from the talk are available at https://is.muni.cz/auth/el/fi/jaro2026/IA067/um/slides/ (after aunthentication in IS).

The Lab Fest, held as part of the Informatics Colloquium, aims to provide the academic community with an overview of the activities of research groups at the Faculty, specifically their staffing, areas of interest, involvement in grants, ongoing collaborations at the University, in the Czech Republic or internationally; future directions and current research or development results.

AGDM: Studio of Graphic Design and Multimedia

EMLAB: The Design and Architecture of Digital Systems Laboratory

How Algorithm Design Can Save Participatory Budgeting

In a participatory budgeting election, the goal is to choose which projects among those submitted by the citizens should be implemented in a given city. The city fixes some budget, people submit project ideas---such as building bike paths, running various festivals, or offering language classes---each with a different cost, and eventually the citizens vote on which of these projects are carried out. While many cities implement participatory budgeting, most of them use very basic voting rules that do not ensure proportional representation of the voters and that have a number of drawbacks. For example, a fairly small, coordinated group of citizens can hijack the whole budget. In this talk I will present Method of Equal Shares---a voting rule recently proposed by Pierczynski, Peters and Skowron---that has strong proportionality guarantees, and I will tell the story of how this rule moved from a theoretical concept to being applied in practice. This story includes a number of algorithmic and computational complexity developments that were needed to make it feasible (in particular, to explain the sometimes surprising results that the rule can provide). During the talk I will also discuss several other participatory budgeting rules and compare them to Method of Equal Shares.

Challenges in Data Visualizations and Building Trust in Them

Data visualization is a very powerful tool when analyzing and understanding complex data. However, there are many aspects that play a crucial role in this process. Among these belong not only the size and dimensionality of the data, but also the design decisions behind the appropriate visual representations and interactions with them, perceptual limitations of human cognitive system, and capabilities of diverse target audiences to properly interpret the representations. All these aspects highly influence the trust of the stakeholders in the visualization. In this talk, I will present the main aspects and challenges accompanying data visualization, connected to the three main pillars: data, users, and visuals enabling insight. The talk will conclude with several observations and recommendations for interdisciplinary collaboration aiming to build mutual trust between the project partners.

This talk is a part of the process of application for professorship.

Learning to Work with AI: Lessons from a US Tech Startup

The way knowledge workers operate has fundamentally changed in the last three years. In software engineering, AI coding tools have gone from curiosity to daily infrastructure - and AI skills are increasingly expected and tested in interviews. But what does this actually look like in practice, and what should it mean for how we teach computer science?

Drawing on the experience of adopting AI tools at a US fintech startup over the past two years, I'll share some lessons my company learned the hard way: why adoption is harder than it looks, how documentation debt becomes your AI's blind spot, and why some languages and frameworks lend themselves to AI-assisted development far better than others. Nobody knows what's coming next, but I'll share my perspective on what it takes to be an effective software engineer in this new world.

TBA

CoFI break

Neural Networks as Parameterized Gradient-based Solvers

Neural networks were long viewed primarily as pattern recognition systems which are effective at detecting statistical regularities in data, but ill suited to problems that require reasoning. When they did appear to solve such tasks, a common explanation was that they were simply memorizing the training set. The recent success of large language models challenged this view as these models can solve difficult and novel mathematical problems. Yet we still understand surprisingly little about how they do so.

In this talk, I present a mechanistic perspective on neural reasoning through the lens of graph neural networks (GNNs). Specifically, I show how GNNs trained for Boolean satisfiability (SAT) can be interpreted as parameterized primal-dual algorithms that optimize a Lagrangian relaxation of a SAT instance. This viewpoint links learned message-passing dynamics to classical optimization and provides a concrete framework for analyzing when and why these models find satisfying assignments in constraint satisfaction problems. I conclude by discussing what this perspective suggests for the design of more efficient language models.

Verse - designing a new programming language for the Metaverse

Verse is a new programming language being developed at Epic Games for building interactive experiences in the metaverse. Unlike traditional scripting languages for game engines, Verse is designed as a functional logic programming language with a rigorous theoretical foundation-the Verse calculus (VC), a core calculus for deterministic functional logic programming published at ICFP 2023. In this talk, I will discuss the design philosophy behind Verse and the key challenges of creating a language for a future where code runs in a single global simulation. Verse combines ideas from functional programming (immutability, higher-order functions, strong typing), logic programming (unification, choice, backtracking), and introduces novel features such as failable expressions, speculative execution with transactional rollback, and language-level concurrency. The language aims to be "metaverse first," with strong compatibility guarantees and an effect system that tracks side effects to ensure safe concurrent execution. I will explain how these theoretical concepts translate into practical language features and discuss the trade-offs we faced in designing a language that must be both accessible to game developers and capable of expressing complex concurrent and reactive systems. The talk will also touch on our experience deploying Verse in Fortnite's Unreal Editor and our vision for making Verse an open standard for metaverse development.

Towards Verification via Transformation

After a short account of the history of software model checking, we come to the conclusion that we moved from a lack of tools to an abundance of tools in the past 25 years. Our vision is to use existing tools for verification as components or libraries, just as we nowadays use SMT solvers. New (meta) verification tools should form a new layer on top of the existing architectural layers. This requires clear interfaces and separation of concerns, as well as exchange formats for verification artifacts such as intermediate or partial results. Only via the combination of verification tools and their technology, we can leverage all power we have available. We outline a few existing transformation approaches to illustrate that achieving the goal is possible in the near future.

TBA

Jan Jedelský: Transductions between sparse graph classes

The first-order (FO) model-checking problem asks, given a graph G and an FO formula 𝜙, whether G is a model of 𝜙. Using FO logic, one may express the problems of asking if G contains a clique of size k, a distance-independent set of size k, or a subgraph isomorphic to a graph H; and even whether the tree-depth of G is at most k.

An FO transduction is a notion of non-deterministic reduction for this problem. Informally speaking, a transduction from a graph class 𝒞 to a graph class 𝒟 witnesses that every graph G∈𝒟 can be obtained from some coloring of some graph H∈𝒞 using FO logic. Hence, solving the FO model-checking problem restricted to inputs from 𝒞 is not easier than solving the same problem restricted to inputs from 𝒟.

In this talk, we characterize transductions between sparse graph classes in purely combinatorial terms. As a corollary of our characterization, for every k∈ℕ, we prove that the class of all graphs of tree-width ≤k+1 is not transducible from the class of all graphs of tree-width ≤k.

Anna Řechtáčková: Code Quality Defects and How to Find Them Automatically

The ability to write code is not the same as the ability to write it well. I study code quality defects found in code written by novice programmers and explore ways to detect them automatically -- be it by using static analysis or large language models.

In the talk, I will first define code quality defects and present our catalog of over 100 specific defects. I will then share results from a survey of teachers at FI and abroad on how they perceive the severity of these defects. Next, I will introduce EduLint, an educational linter I have developed, and describe its integration into the CS1 course IB111 taught at FI MU. I will outline our research into detecting poor identifiers using large language models and compare their performance with that of human evaluators. And finally, I will describe our efforts to detect duplicate code using both static analysis and LLM-based methods.