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.

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.

TBA.

TBA: TBA

Safe Reinforcement Learning Using Shield Synthesis for LTL Modulo Theories

In recent years, machine learning models and in particular reinforcement learning (RL) have achieved remarkable success in various domains, including sequential decision makers. However, these models tend to exhibit unsafe behaviors, precluding their deployment in safety-critical systems. To cope with this issue, considerable research focuses on developing methods that guarantee the safe behavior of a given RL model, also referred to as "Safe Reinforcement Learning".

A prominent approach to safe RL is shielding which incorporates an external component generated using formal methods, called a shield, that blocks or corrects unwanted behavior. Despite significant progress, shielding suffers from a major setback: classical shielding starts from properties in propositional temporal logics, typically LTL, and is unsuitable for richer logics. This, in turn, limits the widespread applicability of shielding in many real-world systems where the dynamics are complex.

In this work, we address this gap, and extend shielding to LTL modulo theories, by building upon recent advances in reactive synthesis modulo theories. LTL modulo theories allows the use of both temporal modalities and literals for arbitrary theories. This has allowed us to develop a novel approach for generating shields conforming to

complex safety specifications in these more expressive, logics.

This is a "neurosymbolic" solution, in the sense that we build a system that combines the complex goals and behaviors of RL with the safety guarantees of formal synthesis.

The roadmap of the talk is to (1) motivate safe reinforcement learning (2) introduce temporal logic and reactive synthesis (3) present our work on synthesis modulo theories, (4) describe how to extend synthesis modulo theories for shielding.

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

TBA

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.

TBA

TBA

TBA

TBA: TBA