QEST+FORMATS Program

I0		Wednesday		Thursday		Friday

8:30	Live Registration & Coffee	Live Registration & Coffee	Live Registration & Coffee





9:00	Live QEST+FORMATS Opening Q+F	Live Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A	Live Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
	Live QEST+FORMATS Opening Q+F
9:10	Live Monitoring of Timed and Quantitative Systems Kim G. Larsen Q+F









10:00		Live Coffee Break	Live Coffee Break

10:10	Live Coffee Break



10:30	Q+F Session 1 - Markov Models under Uncertainty Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov ChainsPeter Buchholz Wasserstein error bounds for aggregations of continuous-time Markov chainsFabian Michel Robust Parameter Learning for Uncertain MDPsYannik Schnitzer, Alessandro Abate, David Parker	Q+F Session 4 - Stochastic Model Checking Multi-Objective Statistical Model Checking using Lightweight Strategy SamplingPedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk Effective Stochastic Automata Model Checking by Interval AbstractionAnnabell Petri, Arnd Hartmanns, Pedro D'Argenio Collective Decision-Making Under Timing ConstraintsJulia Klein, Tatjana Petrov	Q+F Session 7 - Dependability and Security Analysis Facing the Core: State-Space Compression of Dynamic Fault Trees via PH-DistributionsNazareno Garagiola, Holger Hermanns Adaptive Importance Sampling for Static Fault Trees with Two-State Markovian ComponentsLeonardo Paroli, Laura Carnevali, Enrico Vicario The Cost of Repetition: A Compositional Scalability Model for Attack TreesClemens Fruböse, Eva Hetzel

















12:00	Live Lunch	Live Lunch	Live Lunch

















13:30	Live Supporting Older Adults Living Independently Jane Hillston Q+F	Q+F Session 5 - Probabilistic and Temporal Logic Semantics Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic DecompositionMohamed Hamza Bandukara, Fredrik Dahlqvist, Niki Omidvari Algebraic Robust Semantics for Signal Temporal Logic with Graph OperatorsSheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann, Jyotirmoy Deshmukh	Q+F Session 8 - Queueing and Performance Models Stationary Analysis of Finite-Capacity M/M/1 Fork-Join QueuesPierre Fiorini The Component Queues Method for Quasi-Birth-Death Process Fitting and AnalysisJulianna Bor, Giuliano Casale, Evgenia Smirni













14:40	Live Coffee Break	Live Coffee Break	Live Coffee Break



15:00	Q+F Session 2 - Parametric Games and Automata State-Space Abstractions for Parametric Timed GamesMikael Bisgaard Dahlsen-Jensen, Jaco van de Pol, Laure Petrucci Verification of parametric Markov Automata under time-bounded reachabilityKevin van de Glind, Matthias Volk, Tim Willemse	Q+F Session 6 - Continuous and Hybrid Systems Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step AdaptationMikkel Bjørn, Daniel Hansen, Grace Melchiors, Kim Guldstrand Larsen, Christian Schilling Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal LogicLena Becker, Holger Hermanns	Q+F Session 9 - Timed Automata and Languages Weighing Timed Regular Languages: The Final StepEugene Asarin, Aldric Degorre, Catalin Dima, Bernardo Jacobo Inclán Witnesses and Counterexamples for Timed BisimulationAlexander Lieb, Malte Lochau













16:10	Live Coffee Break		Live Coffee Break



16:30	Q+F Session 3 - Learning and Quantum Systems Learning Alternating Real-Time AutomataKazuki Kinoshita, Masaki Waga Faster algorithm for achieving minimal-size quantum decision diagramsJuul Sanders, Sebastiaan Brand, Tim Coopmans		Q+F Session 10 - Verification Tools MightyPPL: Towards model checking MTLHsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh Pandya LF-mc: An Efficient Verifier for Lingua FrancaMario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function SynthesisRayan Mazouz, Frederik Mathiesen, Luca Laurenti, Morteza Lahijanian

















18:00			Live Football











19:00		Live Boat Tour / Dinner (Boarding at 7:15pm)

Wednesday

8:30	Live Registration & Coffee
9:00	Live QEST+FORMATS Opening Q+F
9:10	Live Monitoring of Timed and Quantitative Systems Kim G. Larsen Q+F
10:10	Live Coffee Break
10:30	Q+F Session 1 - Markov Models under Uncertainty Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov Chains Peter Buchholz Wasserstein error bounds for aggregations of continuous-time Markov chains Fabian Michel Robust Parameter Learning for Uncertain MDPs Yannik Schnitzer, Alessandro Abate, David Parker
12:00	Live Lunch
13:30	Live Supporting Older Adults Living Independently Jane Hillston Q+F
14:40	Live Coffee Break
15:00	Q+F Session 2 - Parametric Games and Automata State-Space Abstractions for Parametric Timed Games Mikael Bisgaard Dahlsen-Jensen, Jaco van de Pol, Laure Petrucci Verification of parametric Markov Automata under time-bounded reachability Kevin van de Glind, Matthias Volk, Tim Willemse
16:10	Live Coffee Break
16:30	Q+F Session 3 - Learning and Quantum Systems Learning Alternating Real-Time Automata Kazuki Kinoshita, Masaki Waga Faster algorithm for achieving minimal-size quantum decision diagrams Juul Sanders, Sebastiaan Brand, Tim Coopmans

Thursday

8:30	Live Registration & Coffee
9:00	Live Reasoning About Probabilistic Loops, Moment by Moment Session chair: Max Tschaikowski Ezio Bartocci Joint Room A
10:00	Live Coffee Break
10:30	Q+F Session 4 - Stochastic Model Checking Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling Pedro R. D'Argenio, Arnd Hartmanns, Patrick Wienhöft, Mark van Wijk Effective Stochastic Automata Model Checking by Interval Abstraction Annabell Petri, Arnd Hartmanns, Pedro D'Argenio Collective Decision-Making Under Timing Constraints Julia Klein, Tatjana Petrov
12:00	Live Lunch
13:30	Q+F Session 5 - Probabilistic and Temporal Logic Semantics Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition Mohamed Hamza Bandukara, Fredrik Dahlqvist, Niki Omidvari Algebraic Robust Semantics for Signal Temporal Logic with Graph Operators Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann, Jyotirmoy Deshmukh
14:40	Live Coffee Break
15:00	Q+F Session 6 - Continuous and Hybrid Systems Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation Mikkel Bjørn, Daniel Hansen, Grace Melchiors, Kim Guldstrand Larsen, Christian Schilling Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic Lena Becker, Holger Hermanns
19:00	Live Boat Tour / Dinner (Boarding at 7:15pm)

Friday

8:30	Live Registration & Coffee
9:00	Live Category Theory for Fast Model Checking Algorithms Session chair: Ana Sokolova Ichiro Hasuo Joint Room A
10:00	Live Coffee Break
10:30	Q+F Session 7 - Dependability and Security Analysis Facing the Core: State-Space Compression of Dynamic Fault Trees via PH-Distributions Nazareno Garagiola, Holger Hermanns Adaptive Importance Sampling for Static Fault Trees with Two-State Markovian Components Leonardo Paroli, Laura Carnevali, Enrico Vicario The Cost of Repetition: A Compositional Scalability Model for Attack Trees Clemens Fruböse, Eva Hetzel
12:00	Live Lunch
13:30	Q+F Session 8 - Queueing and Performance Models Stationary Analysis of Finite-Capacity M/M/1 Fork-Join Queues Pierre Fiorini The Component Queues Method for Quasi-Birth-Death Process Fitting and Analysis Julianna Bor, Giuliano Casale, Evgenia Smirni
14:40	Live Coffee Break
15:00	Q+F Session 9 - Timed Automata and Languages Weighing Timed Regular Languages: The Final Step Eugene Asarin, Aldric Degorre, Catalin Dima, Bernardo Jacobo Inclán Witnesses and Counterexamples for Timed Bisimulation Alexander Lieb, Malte Lochau
16:10	Live Coffee Break
16:30	Q+F Session 10 - Verification Tools MightyPPL: Towards model checking MTL Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar, Paritosh Pandya LF-mc: An Efficient Verifier for Lingua Franca Mario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin, Peter Csaba Ölveczky StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis Rayan Mazouz, Frederik Mathiesen, Luca Laurenti, Morteza Lahijanian
18:00	Live Football

Caption

Invited

Q+F