Program
Awards
Same as in the 2024 edition, we have 3 awards, each worth 500 EUR, kindly supported by Springer!
- QEST Best Paper Award
- FORMATS Best Paper Award
- QEST+FORMATS Best Artifact Award
They will be announced during the social dinner!
Sessions
| Date | Time | Session | Description | Chair |
|---|---|---|---|---|
| 2025-08-26 | 08:30 - 09:00 | Opening | Coffee/registration | |
| 09:00 - 09:50 | Invited talk by Christoph Matheja | QEST+FORMATS invited talk shared with CONFEST | Andrea Vandin | |
| 09:50 - 10:20 | Coffee Break | coffee break | ||
| 10:20 - 12:00 | Statistical Model Checking | 4 presentations | Pedro Ruben D’argenio | |
| 12:00 - 13:30 | Lunch Break | lunch | ||
| 13:30 - 14:20 | Timed Automata | 2 presentations | Frits W. Vaandrager | |
| 14:20 - 14:40 | Coffee Break | coffee break | ||
| 14:40 - 15:55 | Dynamical Systems | 3 presentations | Paolo Ballarini | |
| 15:55 - 16:15 | Coffee Break | coffee break | ||
| 16:15 - 17:30 | Queuing theory | 3 presentations | Laura Carnevali | |
| 18:30 - 21:00 | Welcome reception | |||
| 2025-08-27 | 08:30 - 09:00 | Opening | Coffee/registration | |
| 09:00 - 09:50 | FMICS Invited talk | FMICS invited talk shared with CONFEST | ||
| 09:50 - 10:20 | Coffee Break | coffee break | ||
| 10:20 - 12:00 | Games and Control | 4 presentations | Oliver Schoen | |
| 12:00 - 13:30 | Lunch Break | lunch | ||
| 13:30 - 14:20 | Invited talk by Alessandro Abate | QEST+FORMATS invited talk shared with CONFEST | Pavithra Prabhakar | |
| 14:20 - 14:40 | Coffee Break | coffee break | ||
| 14:40 - 15:55 | Probabilistic Systems Analysis | 3 presentations | Arnd Hartmanns | |
| 15:55 - 16:15 | Coffee Break | coffee break | ||
| 16:15 - 17:30 | Learning and inference | 3 presentations | Benoit Barbot | |
| 2025-08-28 | 08:30 - 09:00 | Opening | Coffee/registration | |
| 09:00 - 09:50 | Security | 2 presentations | Carlos E. Budde | |
| 09:50 - 10:10 | Coffee Break | coffee break | ||
| 10:10 - 11:00 | Invited talk by Lu Feng | QEST+FORMATS invited talk | Pavithra Prabhakar | |
| 11:00 - 11:20 | Coffee Break | coffee break | ||
| 11:20 - 12:10 | Termination and Decidability | 2 presentations | Marco Bernardo | |
| 12:10 - 13:30 | Lunch Break | lunch | ||
| 13:30 - 14:30 | SC meeting | Free time for meetings | ||
| 15:30 - 21:00 | Social event + Dinner |
QEST+FORMATS presentations will be held in the "M2" room.
Talks
Statistical Model Checking and Statistical Approximations
- Timo P. Gros, Arnd Hartmanns, Ivo Hoese, Joshua Meyer, Nicola J. Müller and Verena Wolf PyDSMC: Statistical Model Checking for Neural Agents Using the Gymnasium Interface (Tool paper)
- Patrick Wienhöft, Tobias Meggendorfer and Maximilian Weininger What Are the Odds? Improving Statistical Model Checking of Markov Decision Processes
- Gabriel Dengler, Carlos E. Budde, Laura Carnevali and Arnd Hartmanns Time-Sensitive Importance Splitting
- Olivier Bouët-Willaumez, Adrien Le Coënt, Benoit Barbot and Nihal Pekergin Conservation Analysis and Discrete Probabilistic Approximations for Parameter Estimation of Biochemical Networks
Timed Automata
- Abhinav Garg, Madhavan Mukund, Adwitee Roy, B Srivathsan and Gautham Viswanathan Using Communication to Bound Clock Drift in Local-Timed Negotiations
- Benoit Barbot, Nicolas Basset, Thao Dang, Alexandre Donzé, Marco Esposito and Dejan Nickovic Signal Sampling and Optimisation under Symbolic Timed Automata Constraints
Dynamical Systems
- Xavier Allamigeon, Pascal Capetillo and Stéphane Gaubert Computing the Congestion Phases of Dynamical Systems with Priorities and Application to Emergency Departments
- Pauline Blohm, Felix Schulz, Lisa Willemsen, Anne Remke and Paula Herber Modeling Uncertainty: From Simulink to Stochastic Hybrid Automata
- Jun Liu and Maxwell Fitzsimmons Symbolic Reduction for Formal Synthesis of Global Lyapunov Functions
Queueing Theory
- Lukas Wildberger, Anja Hamscher and Jens B. Schmitt Minimal Per-Flow Backlog Bounds at an Aggregate FIFO Server under Piecewise-Linear Arrival Curves
- Fabian Michel and Markus Siegle Formal Approximations of the Transient Distributions of the M/G/1 Workload Process
- Andrea Marin, Diletta Olliaro, Sabina Rossi and Daniel Sadoc Menasche A Product-Form Model for Systems with Aging Objects and Similarities
Games and Control
- Lina Gerlach, Christof Löding and Erika Abraham A Hyperlogic for Strategies in Stochastic Games
- Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Jaco van de Pol and Laure Petrucci Controller Synthesis for Parametric Timed Games
- Oliver Schön, Sofie Haesaert and Sadegh Soudjani Formal Control for Uncertain Systems via Contract-Based Probabilistic Surrogates
- Alireza Nadali, Ashutosh Trivedi and Majid Zamani On Choice of Loss Functions for Neural Control Barrier Certificates
Probabilistic Systems Analysis
- Tobias Gürtler and Benjamin Lucien Kaminski Programming and Reasoning in Partially Observable Probabilistic Environments
- Carlos E. Budde, Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger and Patrick Wienhöft Statistical Model Checking Beyond Means: Quantiles, CVaR, and the DKW Inequality
- Sebastiaan Brand, Arend-Jan Quist, Richard M.K. van Dijk and Alfons Laarman Numerical Errors in Quantitative System Analysis With Decision Diagrams
Learning and Inference
- Véronique Bruyère, Bharat Garhewal, Guillermo Perez, Gaëtan Staquet and Frits Vaandrager Active Learning of Mealy Machines with Timers
- Wolffhardt Schwabe, Paul Kogel and Sabine Glesner Learning Mealy Machines with Sparse Observation Tables
- Paolo Ballarini, Pierre Cry, Andras Horvath and Pascale Legall Statistical Bayesian Inference for Stochastic Process Discovery
Security
- Thi Kim Nhung Dang, Benedikt Peterseim, Milan Lopuhaä-Zwakenberg and Mariëlle Stoelinga Fuzzy Fault Trees: the Fast and the Formal
- Andrea Esposito, Alessandro Aldini and Marco Bernardo Noninterference Analysis of Deterministically Timed Reversible Systems
Termination and Decidability
- Gaspard Fougea, Serge Haddad, Lina Ye, Shreyas Jain and Alain Finkel Tightening the Frontier of Decidability for Decisiveness
- Lorenz Winkler and Laura Kovács *Positive Almost-Sure Termination of Polynomial Random Walks