2009
  Joost-Pieter Katoen, and Ivan S. Zapreev. Simulation-based CTMC Model Checking: An Empirical Evaluation. In Quantitative Evaluation of Systems (QEST). IEEE CS Press, 2009.
 
Joost-Pieter Katoen, E. Moritz Hahn, Holger Hermanns, David N. Jansen, and Ivan S. Zapreev. The Ins and Outs of the Probabilistic Model Checker MRMC. In Quantitative Evaluation of Systems (QEST). IEEE CS Press, 2009.

2008
  David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Marielle Stoelinga, and Ivan S. Zapreev. How fast and fat is your probabilistic model checker? An experimental comparison. In Hardware and Software: Verification and Testing (Haifa Verification Conference, HVC). pages 69–85. Volume 4899 of LNCS. Springer, 2008.
 
Ivan S. Zapreev. Model Checking Markov Chains: Techniques and Tools. PhD Thesis, University of Twente, 2008.

2007
 
Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, and David N. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking.. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’07). pages 76–92. Volume 4424 of Lecture Notes in Computer Science. Springer Verlag, 2007.

2006
 
Joost-Pieter Katoen, and Ivan S. Zapreev. Safe on-the-fly steady-state detection for time-bounded reachability. In Quantitative Evaluation of Systems (QEST). pages 301–310. IEEE CS Press, 2006.

2005
 
Joost-Pieter Katoen, Maneesh Khattri, and Ivan S. Zapreev. A Markov reward model checker. In Quantitative Evaluation of Systems (QEST). pages 243–244. IEEE CS Press, 2005.
 
Joost-Pieter Katoen, and Ivan S. Zapreev. Safe on-the-fly steady-state detection for time-bounded reachability.. Technical Report TR-CTIT-05-52, CTIT, University of Twente, 2005.