A Markov Reward Model Checker. - Joost-Pieter Katoen; Maneesh Khattri; Ivan S. Zapreev (QEST, 2005)

Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. - Joost-Pieter Katoen; Ivan S. Zapreev (QEST, 2006)

How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. - David N. Jansen; Joost-Pieter Katoen; Marcel Oldenkamp; Mariëlle Stoelinga; Ivan S. Zapreev (Haifa Verification Conference, 2007)

Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. - Joost-Pieter Katoen; Tim Kemna; Ivan S. Zapreev; David N. Jansen (TACAS, 2007)

Model checking Markov chains : techniques and tools. - Ivan S. Zapreev (2008)

Simulation-Based CTMC Model Checking: An Empirical Evaluation. - Joost-Pieter Katoen; Ivan S. Zapreev (QEST, 2009)

Computable CTL* for Discrete-Time and Continuous-Space Dynamic Systems. - Pieter Collins; Ivan S. Zapreev (RP, 2009)

Computable Semantics for CTL* on Discrete-Time and Continuous-Space Dynamic Systems. - Pieter Collins; Ivan S. Zapreev (Int. J. Found. Comput. Sci., 2011)

The ins and outs of the probabilistic model checker MRMC. - Joost-Pieter Katoen; Ivan S. Zapreev; Ernst Moritz Hahn; Holger Hermanns; David N. Jansen (Perform. Evaluation, 2011)

Optimal Symbolic Controllers Determinization for BDD storage. - Ivan S. Zapreev; Cees Verdier; Manuel Mazo Jr. 002 (ADHS, 2018)