09:00 - 10:00 Welcome and introduction of all participants
10:00 - 10:30 Tea break
10:30 - 11:20 Tutorial: Joost-Pieter Katoen, Probabilistic Programming: Semantics and Verification
11:20 - 11:30 Short break
11:30 - 11:55 Talk: Benjamin Kaminski, Fixed Points in Probabilistic Program Reasoning
11:55 - 13:45 Lunch
13:45 - 14:10 Talk: Mingshuai Chen, Reasoning about Loopy Probabilistic Programs
14:10 - 14:35 Talk: Lutz Klinkenberg, (probabilistic) Generating Functions for Probabilistic Programs
14:35 - 14:45 Short break
14:45 - 15:10 Talk: Kaushik Mallik, Decoupled Planning for Multiple Omega-Regular Objectives
15:10 - 15:35 Talk: Shibashis Guha, Sure-almost-sure and Sure-limit-sure Window Mean Payoff in Markov Decision Processes
15:35 - 16:10 Tea break
16:10 - 17:00 Tutorial: Petr Novotný, Formal Methods meet Reinforcement Learning: Gaps and Opportunities
17:00 - 17:45 Free time
18:00 - 20:00 Dinner
09:00 - 09:10 Planning
09:10 - 10:00 Tutorial: Jean-Francois Raskin, Probabilistic Model Checking: An Introduction
10:00 - 10:30 Tea break
10:30 - 10:55 Talk: Laurent Doyen, Sure-Almost-Sure Stochastic Parity Games
10:55 - 11:20 Talk: Djordje Zikelic, Distribution Transformer View of MDPs: Verification and Synthesis
11:20 - 11:30 Short break
11:30 - 11:55 Piyush Srivastava, Entropy Objectives in Markov Decision Processes
11:55 - 13:45 Lunch
13:45 - 14:10 Talk: Ichiro Hasuo, Categorical Abstraction for Probabilistic Model Checking
14:10 - 14:35 Talk: Joost-Pieter Katoen, Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams
14:35 - 14:45 Short break
14:45 - 15:10 Talk: Naijun Zhan, Verification of Stochastic Dynamical and Hybrid Systems
15:10 - 15:35 Talk: Bai Xue, Controlled Reach-Avoid Set Computation for Discrete-Time Polynomial Systems via Convex Optimization
15:35 - 16:10 Tea break
16:10 - 17:00 Open problems session
17:00 - 17:45 Free time
18:00 - 20:00 Dinner
09:00 - 09:10 Planning
09:10 - 10:00 Tutorial: Amir Goharshady, Parametrised Algorithms and Structural Properties of Programs
10:00 - 10:30 Tea break
10:30 - 11:55 Breakout discussions
11:55 - 13:45 Lunch
13:30 - 17:00 Excursion
17:00 - 17:45 Free time
18:00 - 20:00 Dinner
09:00 - 09:10 Planning
09:10 - 10:00 Tutorial: Anna Lukina, A Lifecycle of Neural Certificates for Probabilistic Systems
10:00 - 10:30 Tea break
10:30 - 10:55 Talk: Mirco Giacobbe, Omega-regular Supermartingale Certificates
10:55 - 11:20 Talk: Thom Badings, Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
11:20 - 11:55 Breakout discussions
11:55 - 13:45 Lunch
13:45 - 14:10 Talk: Blaise Genest, Neurosymbolic Techniques to Obtain Safe Controllers
14:10 - 14:35 Talk: Ashutosh Trivedi, Reinforcement Learning Beyond Finite MDPs: Recursive, Branching, and Regular Models
14:35 - 14:45 Short break
14:45 - 15:10 Talk: Mahsa Shirmohammadi, Orbit Closure in Program Invaraints
15:10 - 15:35 Talk: Tobias Meggendorfer, Entropic Risk and Multiplicative Reward
15:35 - 16:10 Tea break
16:10 - 17:00 Open problems session
17:00 - 17:45 Free time
18:00 - 20:00 Dinner
09:00 - 09:10 Planning
09:10 - 09:35 Talk: Jean-Francois Raskin
09:35 - 10:00 Talk: Masaki Waga, Probabilistic Black-Box Checking via Active MDP Learning
10:00 - 10:30 Tea break
10:30 - 10:55 Talk: Jingbo Wang, Reasoning About Uncertainty in Datalog
10:55 - 11:55 Breakout discussions
11:55 - 13:45 Lunch