[KatoenZHHJ09] The Ins and Outs of the Probabilistic Model Checker MRMC Katoen, J.-P.; Zapreev, I. S.; Hahn, E. M.; Hermanns, H. and Jansen, D. N. In Sixth International Conference on the Quantitative Evaluation of Systems (QEST), pages 167-176, IEEE Computer Society, 2009.Downloads: pdf, bibURL: Abstract. The Markov reward model checker (MRMC) is a software tool for verifying properties over probabilistic models. It supports PCTL and CSL model checking, and their reward extensions. Distinguishing features of MRMC are its support for computing time- and reward-bounded reachability probabilities, (property-driven) bisimulation minimization, and precise on-the-fly steady-state detection. Recent tool features include time-bounded reachability analysis for uniform CTMDPs and CSL model checking by discrete-event simulation. This paper presents the tool's current status and its implementation details.