Best Paper/Artifact Award Nominations

The following papers/artifacts have been nominated for the QEST+FORMATS 2026 Best Paper/Artifact Awards. These awards are sponsored by Springer and the winners will be announced at the social reception of CONFEST 2026 on Tuesday evening.

Best Paper Award Nominations

• Peter Buchholz. Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov Chains
• Mohamed Hamza Bandukara, Fredrik Dahlqvist and Niki Omidvari. Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition
• Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya. MightyPPL: Towards model checking MTL
• Fabian Michel. Wasserstein error bounds for aggregations of continuous-time Markov chains
• Julianna Bor, Giuliano Casale and Evgenia Smirni. The Component Queues Method for Quasi-Birth-Death Process Fitting and Analysis
• Juul Sanders, Sebastiaan Brand and Tim Coopmans. Faster algorithm for achieving minimal-size quantum decision diagrams

Best Artifact Award Nominations

• Pedro R. D’Argenio, Arnd Hartmanns, Patrick Wienhöft and Mark van Wijk. Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling
• Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya. MightyPPL: Towards model checking MTL
• Mario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin and Peter Csaba Ölveczky. LF-mc: An Efficient Verifier for Lingua Franca

Accepted papers

• Peter Buchholz. Stationary and Transient Bounds for Nearly Lumpable or Uncertain Markov Chains
• Mikael Bisgaard Dahlsen-Jensen, Jaco van de Pol and Laure Petrucci. State-Space Abstractions for Parametric Timed Games
• Nazareno Garagiola and Holger Hermanns. Facing the Core: State-Space Compression of Dynamic Fault Trees via PH-Distributions
• Eugene Asarin, Aldric Degorre, Catalin Dima and Bernardo Jacobo Inclán. Weighing Timed Regular Languages: The Final Step
• Mohamed Hamza Bandukara, Fredrik Dahlqvist and Niki Omidvari. Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition
• Mikkel Bjørn, Daniel Hansen, Grace Melchiors, Kim Guldstrand Larsen and Christian Schilling. Scalable Reachability Analysis of Linear Continuous Systems with Property-Driven Time-Step Adaptation
• Yannik Schnitzer, Alessandro Abate and David Parker. Robust Parameter Learning for Uncertain MDPs
• Pierre Fiorini. Stationary Analysis of Finite-Capacity M/M/1 Fork-Join Queues
• Kazuki Kinoshita and Masaki Waga. Learning Alternating Real-Time Automata
• Pedro R. D’Argenio, Arnd Hartmanns, Patrick Wienhöft and Mark van Wijk. Multi-Objective Statistical Model Checking using Lightweight Strategy Sampling
• Leonardo Paroli, Laura Carnevali and Enrico Vicario. Adaptive Importance Sampling for Static Fault Trees with Two-State Markovian Components
• [Tool paper] Hsi-Ming Ho, S Krishna, Khushraj Madnani, Rupak Majumdar and Paritosh Pandya. MightyPPL: Towards model checking MTL
• Sheryl Paul, Vidisha Kudalkar, Anand Balakrishnan, Tianhao Wu, Lars Lindemann and Jyotirmoy Deshmukh. Algebraic Robust Semantics for Signal Temporal Logic with Graph Operators
• Fabian Michel. Wasserstein error bounds for aggregations of continuous-time Markov chains
• Julianna Bor, Giuliano Casale and Evgenia Smirni. The Component Queues Method for Quasi-Birth-Death Process Fitting and Analysis
• Lena Becker and Holger Hermanns. Stability Checking of Markov Jump Linear Systems via Probabilistic Temporal Logic
• [Tool paper] Mario Reja, Mikheil Rukhaia, Kyungmin Bae, Mircea Marin and Peter Csaba Ölveczky. LF-mc: An Efficient Verifier for Lingua Franca
• Clemens Fruböse and Eva Hetzel. The Cost of Repetition: A Compositional Scalability Model for Attack Trees
• Alexander Lieb and Malte Lochau. Witnesses and Counterexamples for Timed Bisimulation
• Julia Klein and Tatjana Petrov. Collective Decision-Making Under Timing Constraints
• Annabell Petri, Arnd Hartmanns and Pedro D’Argenio. Effective Stochastic Automata Model Checking by Interval Abstraction
• Kevin van de Glind, Matthias Volk and Tim Willemse. Verification of parametric Markov Automata under time-bounded reachability
• Juul Sanders, Sebastiaan Brand and Tim Coopmans. Faster algorithm for achieving minimal-size quantum decision diagrams
• [Tool paper] Rayan Mazouz, Frederik Mathiesen, Luca Laurenti and Morteza Lahijanian. StochasticBarrier.jl: A Toolbox for Stochastic Barrier Function Synthesis