2010
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Performance Evaluation and Model Checking Join Forces. Communications of the ACM, , 2010.
  Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Performability Assessment by Model Checking of Markov Reward Models. Formal Methods in Systems Design, , 2010.

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.
  Angelika Mader, Henrik Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann Hurink, and Holger Hermanns. Synthesis and Stochastic Assessment of Cost-Optimal Schedules. Software Tools for Technology Transfer, to appear, 2009.

2008
 
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Reachability in continuous-time Markov reward decision processes. In Erich Graedel, Joerg Flum, and Thomas Wilke, editors, Logic and Automata: History and Perspectives. pages 53–72. Volume 2 of Texts in Logics and Games. Amsterdam University Press, 2008.
  Lijun Zhang, Friedrich Eisenbrand, Holger Hermanns, and David N. Jansen. Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. Logical Methods in Computer Science, 4(4), 2008.
  Felix Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, Wolfgang Frings, Karl Fürlinger, Markus Geimer, Marc-Andre Hermanns, Bernd Mohr, Shirley Moore, Matthias Pfeifer, and Zoltan Szebenyi. Usage of the SCALASCA Toolset for Scalable Performance Analysis of Large-Scale Parallel Applications. In Proc. of the 2nd HLRS Parallel Tools Workshop. pages 157–167. 2008.

2007
 
Henrik Bohnenkamp, Holger Hermanns, and Joost-Pieter Katoen. Motor: The MoDeST Tool Environment. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’07). pages 500–504. Volume 4424 of Lecture Notes in Computer Science. Springer-Verlag, 2007.
  Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, and David N. Jansen. Flow faster: efficient decision algorithms for probabilistic simulations. In Orna Grumberg, and Michael Huth, editors, Tools and algorithms for the construction and analysis of systems. pages 155–169. Volume 4424 of Lecture notes in computer science. Springer, 2007.

2006
 
Angelika Mader, Henrik Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann Hurink, and Holger Hermanns. Synthesis and Stochastic Assessment of Cost-Optimal Schedules. Technical Report 06-14, University of Twente, 2006. ISSN 1381-3625.
  Henrik Bohnenkamp, Pedro R. D’Argenio, Holger Hermanns, and Joost-Pieter Katoen. MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Transactions on Software Engineering, 32(10):812–830, 2006.
  Mario Bravetti, Holger Hermanns, and Joost-Pieter Katoen. YMCA: Why Markov Chain Algebra?. Electronic Notes in Theoretical Computer Science, 162:107–112, 2006.

2005
  Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Verena Wolf. Comparative branching-time semantics for Markov chains. Information and Computation, 200(2):149–214, 2005.
 
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking meets performance evaluation. SIGMETRICS Performance Evaluation Review, 32(4):10–15, 2005.
  Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Boudewijn R. Haverkort. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science, 345(1):2–26, 2005.

2004
 
Henrik C. Bohnenkamp, Pedro R. D’Argenio, Holger Hermanns, and Joost-Pieter Katoen. MoDeST: A compositional modeling formalism for real-time and stochastic systems. Technical Report TR-CTIT-04-46, Centre for Telematics and Information Technology, University of Twente, 2004.
 
Joost-Pieter Katoen, Henrik Bohnenkamp, Ric Klaren, and Holger Hermanns. Embedded software analysis with MOTOR. In Marco Bernardo, and Flavio Corradini, editors, Formal Methods for the Design of Real-Time Systems (SFM-RT 2004). pages 268–294. LNCS vol. 3185, Springer-Verlag, 2004.
 
Henrik Bohnenkamp, Holger Hermanns, Ric Klaren, Angelika Mader, and Yaroslav Usenko. Synthesis and stochastic assessment of schedules for lacquer production. In Quantitative Evaluation of Systems (QEST 2004). pages 28–37. IEEE Computer Society Press, 2004.
  Christel Baier, Holger Hermanns, and Joost-Pieter Katoen. Probabilistic weak simulation is decidable in polynomial time. Information Processing Letters, 89(3):123–130, 2004.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen, and Markus Siegle. Validation of Stochastic Systems. Lecture Notes in Computer Science, 465 pages, 2925, 2004.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Efficient computation of maximal timed reachability probabilities in uniform continuous-time Markov decision processes. In K. Jensen, and A. Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 61–76. LNCS vol. 2988, Springer-Verlag, 2004.

2003
 
Henrik Bohnenkamp, Peter van der Stok, Holger Hermanns, and Frits Vaandrager. Cost-optimization of the IPv4 Zeroconf protocol. In Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), pages 531–540. IEEE Computer Society Press, 2003.
  Henrik Bohnenkamp, Tod Courtney, David Daly, Salem Derisavi, Holger Hermanns, Joost-Pieter Katoen, Vinh Vi Lam, and Bill Sanders. On integrating the Möbius and MoDeST modeling tools. In Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), pages 671–671. IEEE Computer Society Press, 2003.
 
Henrik Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen, and Ric Klaren. The MoDeST Modeling Tool and its implementation. In Computer Performance Evaluation—Modelling Techniques and Tools (TOOLS 2003). Volume 2794 of LNCS. Springer-Verlag, 2003.
  David N. Jansen, Holger Hermanns, and Joost-Pieter Katoen. A QoS-Oriented Extension of UML Statecharts. In Perdita Stevens, Jon Whittle, and Grady Booch, editors, The Unified Modeling Language (UML). pages 76–92. LNCS vol. 2863, Springer-Verlag, 2003.
  Suzana Andova, Holger Hermanns, and Joost-Pieter Katoen. Discrete-time rewards model-checked. In Kim G. Larsen, and Peter Niebert, editors, Formal Methods for Timed Systems (FORMATS). pages 88–104. LNCS vol. 2791, Springer-Verlag, 2003.
  Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Verena Wolf. Comparative branching-time semantics for Markov chains. In Roberto M. Amadio, and Denis Lugiez, editors, Concurrency Theory (CONCUR). pages 492–508. LNCS vol. 2761, Springer-Verlag, 2003.
  Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, and Markus Siegle. A tool for model-checking Markov chains. STTT, 4(2):153–172, 2003.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 29(6):524–541, 2003.

2002
  Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, and Christel Baier. Model checking performability properties. In Dependable Systems and Networks (DSN). pages 103–113. IEEE CS Press, 2002.
  David N. Jansen, Holger Hermanns, and Joost-Pieter Katoen. A probabilistic extension of UML statecharts – specification and verification. In Werner Damm, and Ernst-Rüdiger Olderog, editors, Formal Techniques for Real-Time and Fault-Tolerant systems (FTRTFT). pages 355–374. LNCS vol. 2469, Springer-Verlag, 2002.
  Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Boudewijn R. Haverkort. Simulation for continuous-time Markov chains. In Lubos Brim, Petr Jancar, Mojmír Kretínský, and Antonín Kucera, editors, Concurrency Theory (CONCUR). pages 338–354. LNCS vol. 2421, Springer-Verlag, 2002.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Automated performance and dependability evaluation using model checking. In Mariacarla Calzarossa, and Salvatore Tucci, editors, Computer Performance Evaluation. pages 261–289. LNCS vol. 2459, Springer-Verlag, 2002.
  Holger Hermanns, Ulrich Herzog, and Joost-Pieter Katoen. Process algebra for performance evaluation. Theor. Comput. Sci, 274(1-2):43–87, 2002.

2001
  Gabriel Infante G. López, Holger Hermanns, and Joost-Pieter Katoen. Beyond memoryless distributions: model checking semi-Markov chains. In Luca de Alfaro, and Stephen Gilmore, editors, Process Algebra and Probabilistic Methods (PAPM-Probmiv). pages 57–70. LNCS vol. 2165, Springer-Verlag, 2001.
  Ed Brinksma, Holger Hermanns, and Joost-Pieter Katoen. Lectures on Formal Methods and Performance Analysis. Lecture Notes in Computer Science, 430 pages, 2090, 2001.
  Holger Hermanns, and Joost-Pieter Katoen. Performance analysis := (process algebra + model checking) × Markov chains. In Kim G. Larsen, and Mogens Nielsen, editors, Concurrency Theory (CONCUR), volume 2154 of Lecture Notes in Computer Science. pages 59–82. 2001.
  Joost-Pieter Katoen, and Pedro R. D’Argenio. General distributions in process algebra. In Ed Brinksma, Holger Hermanns, and Joost-Pieter Katoen, editors, Lectures on Formal Methods and Performance Analysis (FMPA). pages 375–429. LNCS vol. 2090, Springer-Verlag, 2001.

2000
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. On the logical characterisation of performability properties. In Ugo Montanari, José D.P. Rolim, and Emo Welzl, editors, Automata, Languages and Programming (ICALP). pages 780–792. LNCS vol. 1853, Springer-Verlag, 2000.
  Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, and Markus Siegle. A Markov chain model checker. In Susanne Graf, and Michael I. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 357–373. LNCS vol. 1785, Springer, 2000.
  Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. The use of model checking techniques for quantitative dependability evaluation. In IEEE Symposium on Reliable Distributed Systems (SRDS). pages 228–238. IEEE CS Press, 2000.
  Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, and Markus Siegle. Towards model checking stochastic process algebra. In Wolfgang Grieskamp, Thomas Santen, and Bill Stoddart, editors, Integrated Formal Methods (IFM). pages 420–439. LNCS vol. 1945, Springer, 2000.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking continuous-time Markov chains by transient analysis. In Allen E. Emerson, and Prasad A. Sistla, editors, Computer-Aided Verification (CAV). pages 358–372. LNCS vol. 1855, Springer, 2000.
  Holger Hermanns, and Joost-Pieter Katoen. Automated compositional Markov chain generation for a plain-old telephone system. Sci. Comput. Program, 36(1):97–127, 2000.

1999
  Christel Baier, Joost-Pieter Katoen, and Holger Hermanns. Approximate Symbolic Model Checking of Continuous-Time Markov Chains. In Jos C.M. Baeten, and Sjouke Mauw, editors, Concurrency Theory (CONCUR), volume 1664 of Lecture Notes in Computer Science, pages. pages 146–162. Springer, 1999.
  Pedro R. D’Argenio, Holger Hermanns, and Joost-Pieter Katoen. On Generative Parallel Composition. Electronic Notes in Theoretical Computer Science, 22, 1999.