Dr. Ivan S. Zapreev

 

Room: 4203

E-mail: zapreevis [at] cs.rwth-aachen.de

Phone: +49 (0)241 80 21206

 

I work on a tool named MRMC which stands for Markov Reward Model Checker, here is the link to its official web-page.

 


Publications / Talks

2011
 
Joost-Pieter Katoen, Ivan S. Zapreev, E. Moritz Hahn, Holger Hermanns, and David N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC. Performance Evaluation, 68(2):90–104, 2011.

2009
 
Joost-Pieter Katoen, and Ivan S. Zapreev. Simulation-based CTMC Model Checking: An Empirical Evaluation. In Quantitative Evaluation of Systems (QEST). pages 31–40. IEEE CS Press, 2009.
 
Joost-Pieter Katoen, Ivan S. Zapreev, E. Moritz Hahn, Holger Hermanns, and David N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC. In Quantitative Evaluation of Systems (QEST). pages 167–176. 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.
 
Ivan S. Zapreev. Bisimulation minimisation mostly speeds up probabilistic model checking. Talk. TACAS’07, Braga, Portugal, 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.
  Ivan S. Zapreev. On-the-fly Steady-state detection. Talk. University of Freiburg, Germany, 2006. Invited Presentation.
 
Ivan S. Zapreev. Safe On-The-Fly Steady-State Detection for Time-Bounded Reachability. Talk. QEST’06, Riverside, CA, USA, 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.
 
Ivan S. Zapreev. A Markov reward model checker. Talk. QEST’05, Torino, Italy, 2005.