Keynote: Joost-Pieter Katoen (joint with all conferences)
(09:00-10:00 CEST)

Coffee Break
(10:00-10:20 CEST)

Session: Machine Learning
(10:20-12:20 CEST)

• Symbolic Semantics for Probabilistic Programs
  Erik Voogd, Einar Broch Johnsen, Alexandra Silva, Zachary J. Susag and Andrzej Wasowski
  (full paper)
• Data-driven Inference of Chemical Reaction Networks via Graph-based Variational Autoencoders
  Luca Bortolussi, Francesca Cairoli, Julia Klein and Tatjana Petrov
  (work in progress paper)
• On the Trade-off Between Efficiency and Precision of Neural Abstraction
  Alec Edwards, Mirco Giacobbe and Alessandro Abate
  (full paper)
• Probabilistic Counterexample Guidance for Safer Reinforcement Learning
  Xiaotong Ji and Antonio Filieri
  (full paper)
• Model Abstraction and Conditional Sampling with Score-Based Diffusion Model
  Davide Scassola, Francesca Cairoli, Francesco Giacomarra and Luca Bortolussi
  (work in progress paper)

Lunch Break
(12:20-13:45 CEST)

Boat trip on Scheldt river
(13:45-18:00 CEST)

Conference Dinner
(18:00-20:00 CEST)

Keynote: Jaco van de Pol (joint with all conferences)
(09:00-10:00 CEST)

Coffee Break
(10:00-10:20 CEST)

Session: Performance
(10:20-12:20 CEST)

• Skipping and Fetching: Insights on Non-Conventional Product-Form Solutions
  Diletta Olliaro, Andrea Marin, Gianfranco Balbo and Matteo Sereno
  (full paper)
• Analysis of an epoch commit protocol for distributed processing systems
  Paul Ezhilchelvan, Isi Mitrani and Jim Webber
  (full paper)
• Causal Reversibility Implies Time Reversibility
  Marco Bernardo, Ivan Lanese, Andrea Marin, Claudio Antares Mezzina, Sabina Rossi and Claudio Sacerdoti Coen
  (full paper)
• Quasi-Deterministic Burstiness Bound for Aggregate of Independent, Periodic Flows
  Seyed Mohammadhossein Tabatabaee, Anne Bouillard and Jean-Yves Le Boudec
  (full paper)

Lunch Break
(12:20-13:45 CEST)

Session: Markov Chains
(13:45-15:45 CEST)

• An MM Algorithm to Estimate Parameters in Continuous-time Markov Chains
  Giovanni Bacci, Anna Ingolfsdottir, Kim Guldstrand Larsen and Raphaël Reynouard
  (full paper)
• Matching Distributions under Structural Constraints
  Aaron Bies, Holger Hermanns, Maximilian Alexander Köhl and Andreas Schmidt
  (full paper)
• Equilibrium Analysis of Markov Regenerative Processes
  András Horváth, Marco Paolieri and Enrico Vicario
  (full paper)
• On the Maximum Queue Length of the Hyper Scalable Load Balancing Push Strategy
  Benny Van Houdt
  (full paper)

Coffee Break
(15:45-16:00 CEST)

Keynote: David Parker
Multi-Agent Verification and Control with Probabilistic Model Checking (PDF)
(16:00-17:00 CEST)

Session: Systems Biology
(17:00-17:15 CEST)

• Modeling uncertain biomass composition in genome-scale metabolic models with Flexible Nets
  Teresa Joven, Jorge Lázaro, and Jorge Júlvez
  (work in progress paper)

Keynote: Ahmed Bouajjani (joint with CONCUR)
(09:00-10:00 CEST)

Coffee Break
(10:00-10:20 CEST)

Session: Verification I
(10:20-12:20 CEST)

• Deductive Controller Synthesis for Probabilistic Hyperproperties
  Roman Andriushchenko, Ezio Bartocci, Milan Češka, Francesco Pontiggia and Sarah Sallinger
  (full paper)
• Introducing Asynchronicity to Probabilistic Hyperproperties
  Carolina Gerlach, Oyendrila Dobe, Erika Ábrahám, Ezio Bartocci and Borzoo Bonakdarpour
  (full paper)
• Jajapy: a learning library for stochastic models
  Raphaël Reynouard, Anna Ingolfsdottir and Giovanni Bacci
  (full paper)
• STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker
  Joshua Jeppson, Matthias Volk, Bryant Israelsen, Riley Roberts, Andrew Williams, Lukas Buecherl, Chris Myers, Hao Zheng, Chris Winstead and Zhen Zhang
  (short paper)
• Extracting individual characteristics from population data reveals a negative social effect during honeybee defence
  Tatjana Petrov, Matej Hajnal, Julia Klein, David Šafránek and Morgane Nouvian
  (journal-first presentation)

Lunch Break
(12:20-13:45 CEST)

Keynote: Frans A. Oliehoek
(13:45-14:45 CEST)

Session: Verification II
(14:45-15:45 CEST)

• Verification of Quantum Systems using Barrier Certificates
  Marco Lewis, Paolo Zuliani and Sadegh Soudjani
  (full paper)
• A Bounded Model Checking Technique for Discrete-Time Nonlinear Systems
  YoungMin Kwon, Eunhee Kim and Gul Agha
  (full paper)

Coffee Break
(15:45-16:00 CEST)

Session: Automata
(16:00-17:30 CEST)

• Max-entropy sampling for deterministic timed automata under linear duration constraints
  Nicolas Basset and Benoit Barbot
  (full paper)
• Comparing Two Approaches to Include Stochasticity in Hybrid Automata
  Lisa Willemsen, Anne Remke and Erika Ábrahám
  (full paper)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics
  Luke Rickard, Thom Badings, Licio Romao and Alessandro Abate
  (full paper)