Opening
(08:55-09:00 CEST)

Keynote: Marta Kwiatkowska (PDF)
(09:00-10:00 CEST)

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

Session: Program Analysis
(10:30-12:00 CEST)
Chair: Joost-Pieter Katoen

• Moment-based Invariants for Probabilistic Loops with non-polynomial assignments (PDF)
  Andrey Kofnov, Marcel Moosbrugger, Miroslav Stankovič, Ezio Bartocci and Efstathia Bura
  (best paper award)
• Distribution Estimation for Probabilistic Loops (PDF)
  Ahmad Karimi, Marcel Moosbrugger, Miroslav Stankovič, Laura Kovács, Ezio Bartocci and Efstathia Bura
• An Automated Quantitative Information Flow Analysis for Concurrent Programs (PDF)
  Khayyam Salehi, Ali A. Noroozi, Sepehr Amir-Mohammadian and Mohammadsadegh Mohagheghi

Lunch Break
(12:00-14:00 CEST)

Session: Parameter Synthesis
(14:00-15:30 CEST)
Chair: Marta Kwiatkowska

• Rate Lifting for Stochastic Process Algebra - Exploiting Structural Properties (PDF)
  Markus Siegle and Amin Soltanieh
• End-to-end Statistical Model Checking for Parametric ODE Models (PDF)
  David Julien, Guillaume Cantin and Benoît Delahaye
• POMDP Controllers With Optimal Budget (PDF)
  Jip Spel, Svenja Stein and Joost-Pieter Katoen

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

Session: Markovian Agents and Population Models
(16:00-17:00 CEST)
Chair: Giuliano Casale

• A Logical Framework for Reasoning about Local and Global Properties of Collective Systems (PDF)
  Michele Loreti and Aniqa Rehman
• Jump Longer to Jump Less: Improving Dynamic Boundary Projection with h-scaling (PDF)
  Francesca Randone, Luca Bortolussi and Mirco Tribastone

Session: Dynamical Systems
(17:00-18:00 CEST)
Chair: Giuliano Casale

• An Algorithm for the Formal Reduction of Differential Equations as Over-approximations (PDF)
  Giuseppe Squillace, Mirco Tribastone, Max Tschaikowski and Andrea Vandin
• Stability Analysis of Planar Probabilistic Piecewise Constant Derivative Systems (PDF)
  Spandan Das (remote) and Pavithra Prabhakar

Reception
(18:00-20:00 CEST)

Keynote: Pedro R. D'Argenio
(09:00-10:00 CEST)

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

Session: Tools
(10:30-12:00 CEST)
Chair: Arnd Hartmanns

• LN: a Meta-Solver for Layered Queueing Network Analysis (PDF)
  Giuliano Casale, Yicheng Gao, Zifeng Niu and Lulai Zhu
• LCRL: Certified Policy Synthesis via Logically-Constrained Reinforcement Learning (PDF)
  Mohammadhosein Hasanbeig (remote), Daniel Kroening and Alessandro Abate
• Eulero: A Tool for Quantitative Modeling and Evaluation of Complex Workflows (PDF)
  Laura Carnevali, Riccardo Reali (remote) and Enrico Vicario

Lunch Break
(12:00-14:00 CEST)

Session: Applications
(14:00-16:00 CEST)
Chair: Markus Siegle

• Analysis of an Electric Vehicle Charging System along a Highway (PDF)
  Davide Cerotti, Simona Mancini, Marco Gribaudo and Andrea Bobbio
• Verifier's Dilemma in Ethereum Blockchain: A Quantitative Analysis (PDF)
  Daria Smuseva, Ivan Malakhov, Andrea Marin, Aad van Moorsel and Sabina Rossi
• Comparing Statistical and Analytical Routing Approaches for Delay-Tolerant Networks (PDF)
  Pedro R. D'Argenio, Juan A. Fraire, Arnd Hartmanns and Fernando Raverta
• Preference-Aware Computation Offloading for IoT in Multi-Access Edge Computing Using Probabilistic Model Checking (PDF)
  Kaustabha Ray (remote) and Ansuman Banerjee

Excursion
(16:00-19:00 CEST)

Banquet
(19:00 CEST)

Session: Automata Theory and Applications
(10:30-11:30 CEST)
Chair: Pedro D'Argenio

• Mirrors and Memory in Quantum Automata (PDF)
  Carla Piazza and Riccardo Romanello
• Monte Carlo Tree Search for Priced Timed Automata (PDF)
  Peter Gjøl Jensen, Andrej Kiviriga, Kim Guldstrand Larsen, Ulrik Nyman, Adriana Mijacika and Jeppe Høiriis Mortensen

Best Paper Award and Closing Remarks
(11:30-11:50 CEST)