The Satisfiability Problem for Probabilistic CTL. by Brázdil, T, Forejt, V, Kretínský, J, Kucera, A

Enforcing ω-regular properties in Markov chains by restarting by Esparza, J, Kiefer, SM, Křetínský, J, Weininger, M

Continuous-Time Stochastic Games with Time-Bounded Reachability. by Brázdil, T, Forejt, V, Krcál, J, Kretínský, J, Kucera, A

Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games by Svorenova, M, Kretinsky, J, Chmelik, M, Chatterjee, K, Cerna, I, Belta, C

On correctness, precision, and performance in quantitative verification: QComp 2020 Competition Report by Budde, CE, Hartmanns, A, Klauck, M, Křetínský, J, Parker, D, Quatmann, T, Turrini, A, Zhang, Z

Tools at the frontiers of quantitative verification: QComp 2023 competition report by Andriushchenko, R, Bork, A, Budde, CE, Češka,, M, Grover, K, Hahn, EM, Hartmanns, A, Israelsen, B, Jansen, N, Jeppson, J, Junges, S, Köhl, MA, Könighofer, B, Křetínský, J, Meggendorfer, T, Parker, D, Pranger, S, Quatmann, T, Ruijters, E, Taylor, L, Volk, M, Weininger, M, Zhang, Z