Publications of the MOVES Group

Technical reports are listed separately.


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.
  Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, and Martin Leucker. Learning Communicating Automata from MSCs. IEEE Transactions on Software Engineering, , 2010.

2009
  Viet Yen Nguyen, and Theo C. Ruys. Memoised Garbage Collection for Software Model Checking. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS. Springer-Verlag, 2009.
  Niels H.M. Aan de Brugh, Viet Yen Nguyen, and Theo C. Ruys. MoonWalker: Verification of .NET Programs. In Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS. Springer-Verlag, 2009.
 
Martin R. Neuhäußer, Marielle Stoelinga, and Joost-Pieter Katoen. Delayed Nondeterminism in Continuous-Time Markov Decision Processes. In Foundations of Software Science and Computation Structures (FoSSaCS). pages 364–379. Volume 5504 of LNCS. Springer-Verlag, 2009.
 
Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik Bohnenkamp, and Joost-Pieter Katoen. Maximizing System Lifetime by Battery Scheduling. In Proc. DSN 2009, IEEE Computer Society, 2009.
  Ralf Mitsching, Carsten Weise, André Kolbe, Henrik Bohnenkamp, and Norbert Berzen. Towards an industrial strength process for timed testing. In Proc. IEEE ICSTW 2009. pages 29–38. IEEE Computer Society, 2009.
 
Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. In IEEE Symposium on Logic in Computer Science (LICS). IEEE CS Press, 2009.
 
Benedikt Bollig, Peter Habermehl, Carsten Kern, and Martin Leucker. Angluin-Style Learning of NFA. In Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI-09). pages 1004–1009. AAAI Press, 2009.
 
Tingting Han, Joost-Pieter Katoen, and Berteun Damman. Counterexample Generation in Probabilistic Model Checking. IEEE Transactions on Software Engineering, 35(2):241–257, 2009.
  Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, and Thomas Noll. Codesign of Dependable Systems: A Component-Based Modeling Language. In Proc. 7th ACM-IEEE Int. Conf. on Formal Methods and Models for Codesign (MEMOCODE 2009). ACM Press, 2009.
 
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, and Marco Roveri. The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. In 28th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP 2009). pages 173–186. Volume 5775 of LNCS. Springer, 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.
 
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, and Joost-Pieter Katoen. Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. 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.
 
Joost-Pieter Katoen, Daniel Klink, and Martin R. Neuhäußer. Compositional Abstraction of Stochastic Systems . In Formal Modeling and Analysis of Timed Systems (FORMATS). pages 195–211. Volume 5813 of LNCS. Springer, 2009.
  Jonathan Heinen, Thomas Noll, and Stefan Rieger. Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures. In Proc. 3rd Int. Workshop on Harnessing Theories for Tool Support in Software (TTSS’09). To be published in ENTCS. Elsevier, 2009.
 
Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. LTL model checking of time-inhomogeneous Markov chains. In 7th International Symposium on Automated Technology for Verification and Analysis (ATVA’09). pages 104–119. Volume 5799 of LNCS. 2009.
 
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, and Marco Roveri. Verification and Performance Evaluation of AADL Models (Tool Demonstration). In Proc. 7th Joint Meeting of European Software Engineering Conference and ACM SIGSOFT Symp. on the Foundations of Software Engineering (ESEC/FSE 2009). pages 285–286. ACM Press, 2009.
  Bastian Schlich, Thomas Noll, Jörg Brauer, and Lucas Brutschy. Reduction of Interrupt Handler Executions for Model Checking Embedded Software. In Proc. of Haifa Verification Conference 2009 (HVC 2009). LNCS. Springer, 2009.
  Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, and Marco Roveri. Model-Based Codesign of Critical Embedded Systems. In Proc. 2nd Int. Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB 2009). LNCS. Springer, 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.
 
Tingting Han. Diagnosis, Synthesis and Analysis of Probabilistic Models. PhD Thesis, University of Twente and RWTH Aachen University, 2009.
  Stefan Rieger. Verification of Pointer Programs. PhD Thesis, RWTH Aachen University, 2009.
  Erika Ábrahám, Immo Grabe, Andreas Grüner, and Martin Steffen. Behavioral interface description of an object-oriented language with futures and promises. Journal of Logic and Algebraic Programming, 78(7):491–518, 2009.
  Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fraenzle, and Christian Herde. Parallel SAT Solving in Bounded Model Checking. Journal of Logic and Computation, , 2009.
  Natalia Kalinnik, Tobias Schubert, Erika Ábrahám, Ralf Wimmer, and Bernd Becker. Picoso - A Parallel Interval Constraint Solver. In Proc. of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA’09). 2009.
  Carsten Kern. Learning Communicating and Nondeterministic Automata. PhD Thesis, RWTH Aachen University, 2009.

2008
 
Christel Baier, and Joost-Pieter Katoen. Principles of Model Checking, MIT Press, 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.
 
Thomas Noll, and Bastian Schlich. Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code. In Hardware and Software: Verification and Testing (Haifa Verification Conference, HVC). pages 185–201. Volume 4899 of LNCS. Springer, 2008.
 
Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains. In Hybrid Systems: Computation and Control (HSCC). pages 244–258. Volume 4981 of LNCS. Springer Verlag, 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.
 
Gerlind Herberich, Thomas Noll, Bastian Schlich, and Carsten Weise. Proving Correctness of an Efficient Abstraction for Interrupt Handling. In Proceedings 3rd International Workshop on Systems Software Verification (SSV). pages 133–150. Volume 217 of ENTCS. Elsevier, 2008.
 
Joost-Pieter Katoen. How to model and analyze gossiping protocols?. ACM Performance Evaluation Review, 36(3):3–6, 2008.
 
Lars Helge Haß, and Thomas Noll. Equational Abstractions for Reducing the State Space of Rewrite Theories. In Proc. of 7th Int. Workshop on Rewriting Logic and its Applications (WRLA 2008). pages 139–154. Volume 238 of ENTCS. Elsevier, 2008.
 
Thomas Noll, and Stefan Rieger. Verifying Dynamic Pointer Programs. In Proceedings 15th International Symposium on Formal Methods (FM). pages 84–99. Volume 5014 of LNCS. Springer, 2008.
 
Ivan S. Zapreev. Model Checking Markov Chains: Techniques and Tools. PhD Thesis, University of Twente, 2008.
 
Taolue Chen, Tingting Han, and Joost-Pieter Katoen. Time-Abstracting Bisimulation for Probabilistic Timed Automata. In 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). pages 177–184. IEEE CS Press, 2008.
 
Joost-Pieter Katoen. Perspectives in Probabilistic Verification. In 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE). pages 3–10. IEEE CS Press, 2008.
 
Mani Swaminathan, Martin Fraenzle, and Joost-Pieter Katoen. The Surprising Robustness of (Closed) Timed Automata against Clock-Drift. In 5th IFIP International Conference on Theoretical Computer Science (IFIP TCS). pages 537–553. Volume 273 of IFIP. Springer, 2008.
 
Stefan Rieger, and Thomas Noll. Abstracting Complex Data Structures by Hyperedge Replacement. In 4th Int. Conference on Graph Transformations (ICGT 2008). pages 69–83. Volume 5214 of LNCS. Springer, 2008.
 
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf. Abstraction for Stochastic Systems by Erlang’s Method of Stages. In 19th International Conference on Concurrency Theory (CONCUR’08). pages 279–294. Volume 5201 of LNCS. Springer, 2008.
 
Berteun Damman, Tingting Han, and Joost-Pieter Katoen. Regular Expressions for PCTL Counterexamples. In Proceedings 5th International Conference on Quantitative Evaluation of Systems (QEST). pages 179–188. IEEE CS Press, 2008.
 
Benedikt Bollig, Carsten Kern, Joost-Pieter Katoen, and Martin Leucker. Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning. In 19th International Conference on Concurrency Theory (CONCUR’08). pages 162–166. Volume 5201 of LNCS. Springer, 2008.
  Viet Yen Nguyen, and Theo C. Ruys. Incremental Hashing for SPIN. In Proceedings 15th International SPIN Workshop on Model Checking Software. pages 232–249. Volume 5156 of LNCS. 2008.
 
Joost-Pieter Katoen, and Alexandru Mereacre. Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains. In Formal Modeling and Analysis of Timed Systems (FORMATS). pages 203–217. Volume 5215 of LNCS. Springer-Verlag, 2008.
  Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, and Martin Leucker. SMA—The Smyle Modeling Approach. In Proceedings 3rd IFIP TC2 Central and East European Conference on Software Engineering Techniques (CEE-SET). LNCS. 2008.
  Henrik Bohnenkamp, and Marielle Stoelinga. Quantitative Testing. In Proceedings 8th ACMIEEE International Conference on Embedded Software (EMSOFT). pages 227–236. ACM 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.
 
Manuela Bujorianu, and Joost-Pieter Katoen. Symmetry reduction for stochastic hybrid systems. In Proceedings 47th IEEE Conference on Decision and Control (CDC). pages 233–238. IEEE Control Systems Society, 2008.
 
Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. Approximate parameter synthesis for probabilistic time-bounded reachability. In Proceedings of IEEE Real-Time Systems Symposium (RTSS). pages 173–182. IEEE CS Press, 2008.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A Deductive Proof System for Multithreaded Java with Exceptions. Fundamenta Informaticae, 82(4):391–463, 2008.
  Erika Ábrahám, Andreas Grüner, and Martin Steffen. Heap-Abstraction for an Object-Oriented Calculus with Thread Classes. Software and Systems Modeling, 7(2):177–208, 2008.
  Erika Ábrahám, Andreas Grüner, and Martin Steffen. Abstract Interace Behavior of Object-Oriented Languages with Monitors. Theory of Computing Systems, 43(3):322–361, 2008.
  Markus Geimer, Felix Wolf, Brian J. N. Wylie, Erika Ábrahám, Daniel Becker, and Bernd Mohr. The SCALASCA Performance Toolset Architecture. In Proc. of the International Workshop on Scalable Tools for High-End Computing (STHEC’08). pages 56–65. 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
 
Martin R. Neuhäußer, and Thomas Noll. Abstraction and Model Checking of Core Erlang Programs in Maude. In Proceedings of the 6th International Workshop on Rewriting Logic and its Applications. pages 147–163. Volume 176 of ENTCS. Elsevier, 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.
 
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, and Martin Leucker. Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’07). pages 435–450. Volume 4424 of Lecture Notes in Computer Science. Springer Verlag, 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.
 
Joost-Pieter Katoen, Thomas Noll, and Stefan Rieger. Verifying Concurrent List-Manipulating Programs by LTL Model Checking. In Workshop on Heap Analysis and Verification (HAV 2007). pages 94–113. 2007.
  Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, Michele Loreti, and Mieke Massink. Model checking mobile stochastic logic. Theoretical Computer Science, 382:42–70, 2007.
 
Tingting Han, and Joost-Pieter Katoen. Counterexamples in probabilistic model checking. In Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’07). pages 60–75. Volume 4424 of Lecture Notes in Computer Science. Springer Verlag, 2007.
 
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf. Three-valued abstraction for continuous-time Markov chains. In Proceedings of the 19th International Conference on Computer Aided Verification (CAV). pages 311–324. Volume 4590 of Lecture Notes in Computer Science. Springer Verlag, 2007.
 
Martin R. Neuhäußer, and Joost-Pieter Katoen. Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. In 18th International Conference on Concurrency Theory (CONCUR’07). pages 412–427. Volume 4703 of LNCS. 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.
 
Tingting Han, and Joost-Pieter Katoen. Providing evidence of likely being on time – Counterexample generation for CTMC model checking. In Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA’07). Lecture Notes in Computer Science. Springer Verlag, 2007.
  Joost-Pieter Katoen. Abstraction of Probabilistic Systems. In Formal Methods for Timed Systems (FORMATS’07). pages 1–3. Volume 4763 of LNCS. Springer-Verlag, 2007.
 
Thomas Noll, and Stefan Rieger. Composing Transformations to Optimize Linear Code. In Proc. 4th Int. Colloquium on Theoretical Aspects of Computing (ICTAC ’07). pages 425–439. Volume 4711 of LNCS. 2007.
  Henrik Bohnenkamp, and Axel Belinfante. Timed Model-Based Testing. In Jan Tretmans, editor, Tangram: Model-based integration and testing of complex high-tech systems. pages 115–128. Embedded Systems Institute, The Netherlands, 2007.
  Viet Yen Nguyen. Optimising Techniques for Model Checkers. Masters Thesis, University of Twente, 2007.
  Marc Herbstritt, Bernd Becker, Erika Ábrahám, and Christian Herde. On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata. In IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS’07). pages 391–396. IEEE Computer Society, 2007.
  Erika Ábrahám, Immo Grabe, Andreas Grüner, and Martin Steffen. Abstract Interface Behavior of an Object-Oriented Language with Futures and Promises. In Nordic Workshop on Programming Theory (NWPT’07). 2007.

2006
 
Benedikt Bollig, Carsten Kern, Markus Schlütter, and Volker Stolz. MSCan - A Tool for Analyzing MSC Specifications. In Proceedings of the 12th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’06). pages 455–458. Volume 3920 of Lecture Notes in Computer Science. Springer, 2006.
 
Jasper Berendsen, David N. Jansen, and Joost-Pieter Katoen. Probably on time and within budget – On reachability in priced probabilistic timed automata. In Quantitative Evaluation of Systems (QEST). IEEE CS Press, 2006.
  Joost-Pieter Katoen. Stochastic model checking. In Christos G. Cassandras, and John Lygeros, editors, Stochastic Hybrid Systems: Recent Developments and Research Trends. Taylor and Francis, 2006.
 
Dino Distefano, Joost-Pieter Katoen, and Arend Rensink. Safety and liveness in concurrent pointer programs. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and Willem-Paul de Roever, editors, Formal Methods for Components and Objects. pages 280–312. Volume 4111 of LNCS. Springer-Verlag, 2006.
 
Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, and Mieke Massink. Towards a logic for performance and mobility. Electronic Notes in Theoretical Computer Science, 153:161–175, 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.
  Klaus Indermark, and Thomas Noll. Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information. Acta Informatica, 43:1–43, 2006.
  Thomas Noll, and Chanchal Kumar Roy. Towards Automatic Verification of Erlang Programs by pi-Calculus Translation. In Proceedings of the ACM SIGPLAN 2006 Erlang Workshop. pages 38–50. ACM Press, 2006.
  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.
  Thomas Noll, and Stefan Rieger. Optimization of Straight-Line Code Revisited. Softwaretechnik-Trends, 26(2), 2006.
  Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fraenzle, and Christian Herde. Parallel SAT Solving in Bounded Model Checking. In Proc. of PDMC’06. 2006.
  Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen. Memory-Aware Bounded Model Checking for Linear Hybrid Systems. In Proceedings of the 9th. Workshop for Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV’06). 2006.
  Erika Ábrahám, Marc Herbstritt, Bernd Becker, and Martin Steffen. Bounded Model Checking mit Parametric Data Structures. In Proc. of the Fourth International Workshop on Bounded Model Checking (BMC’06). entcs. Elsevier, 2006.
  Erika Ábrahám, Andreas Grüner, and Martin Steffen. Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes. In Proc. of Logical Approaches to Computational Barriers: Second Conference on Computability in Europe (CiE’06). pages 1–10. 2006.
  Erika Ábrahám, Andreas Grüner, and Martin Steffen. Abstract Interface Behavior of Object-Oriented Languages with Monitors. In Proc. of the 8th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS’06). 2006.

2005
 
Henrik Bohnenkamp, and A. Belinfante. Timed Testing with TorX. In John Fitzgerald, Ian Hayes, and Andrzej Tarlecki, editors, Formal Methods 2005, Volume 3582 of LNCS. pages 173–188. Springer-Verlag, 2005.
 
Henrik Bohnenkamp, Johan Gorter, Jarno Guidi, and Joost-Pieter Katoen. Are you still there? — A Lightweight Algorithm To Monitor Node Presence in Self-Configuring Networks. In Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005), pages 704–709. IEEE Computer Society, 2005.
  Pedro R. D’Argenio, and Joost-Pieter Katoen. A theory of stochastic systems. Part I: Stochastic automata. Information and Computation, 203(1):1–38, 2005.
  Pedro R. D’Argenio, and Joost-Pieter Katoen. A theory of stochastic systems. Part II: Process algebra. Information and Computation, 203(1):39–74, 2005.
 
Carsten Kern. Analysis and Imlementations of MSC Specifications. In IFM2005 Doctoral Symposium on Integrated Formal Methods. pages 55–61. Technische universiteit eindhoven: Computer Science-Report 05-29. Judi Romijn, Graeme Smith, Jaco van de Pol, 2005.
  Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and Alexander Pretschner, editors, Model-Based Testing of Reactive Systems (Advanced Lectures), Volume 3472 of Lecture Notes in Computer Science. Springer-Verlag, 2005.
 
Lucia Cloth, Joost-Pieter Katoen, Maneesh Khattri, and Reza Pulungan. Model checking Markov reward models with impulse rewards. In Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005), pages 722–731. IEEE Computer Society, 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.
  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.
  Thomas Noll. Equational Abstractions for Model Checking Erlang Programs. In Proceedings of the International Workshop on Software Verification and Validation (SVV’03). Elsevier, 2005.
  Martin Leucker, Thomas Noll, Perdita Stevens, and Michael Weber. Functional Programming Languages for Verification Tools: A Comparison of ML and Haskell. Software Tools for Technology Transfer, 7(2):184–194, 2005.
  Thomas Noll, and Chanchal Kumar Roy. Modeling Erlang in the pi-Calculus. In Proceedings of the ACM SIGPLAN 2005 Erlang Workshop. pages 72–77. ACM Press, 2005.
  Carsten Kern. MSCan - Ein Tool zur Analyse von Message Sequence Charts. Diploma Thesis, Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2005.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. An Assertion-Based Proof System for Multithreaded Java. Theoretical Computer Science, 331(2-3):251–290, 2005.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Inductive Proof Outlines for Exceptions in Multithreaded Java. In Foundations of Software Engineering (Theory and Practice) (FSEN’05). pages 281–297. Volume 159 of entcs. Elsevier Science Publishers, 2005.
  Erika Ábrahám, Bernd Becker, Felix Klaedke, and Martin Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems. In Verification, Model Checking, and Abstract Interpretation (VMCAI’05). pages 396–412. Volume 3385 of LNCS. Springer-Verlag, 2005.
  Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, and Martin Steffen. Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes. In Theoretical Aspects of Computing (ICTAC’04). pages 37–51. Volume 3407 of LNC. Springer-Verlag, 2005.
  Erika Ábrahám, Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, and Martin Steffen. Observability, Connectivity, and Replay in a Sequential Calculus of Classes. In Formal Methods for Components and Objects (FMCO’04). pages 296–316. Volume 3657 of LNCS. Springer-Verlag, 2005.
  Frank S. de Boer, Marcello M. Bonsangue, Martin Steffen, and Erika Ábrahám. A Fully Abstract Trace Semantics for UML Components. In Formal Methods for Components and Objects (FMCO’04). pages 49–69. Volume 3657 of LNCS. Springer-Verlag, 2005.
  Erika Ábrahám, Andreas Grüner, and Martin Steffen. Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes. Workshop Proceedings of Cosmicah’05, Queen Mary Technical Report RR-05-04, 2005.

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.
  Dino Distefano, Joost-Pieter Katoen, and Arend Rensink. Who is pointing when to whom? – On the automated verification of linked list structures. In Kamal Lodaya, and Meena Mahajan, editors, Foundations of Software Technology and Theoretical Computer Science (FSTTCS). pages 250–262. LNCS vol. 3328, Springer-Verlag, 2004.
  Mieke Massink, Joost-Pieter Katoen, and Diego Latella. Model checking dependability attributes of wireless group communication. In Dependable Systems and Networks (DSN). pages 711–720. IEEE Computer Society, 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.
  Giuliana Franceschinis, Boudewijn R. Haverkort, Joost-Pieter Katoen, and Murray Woodside, editors, Proceedings of the First Int. Conf. on Quantitative Evaluation of Systems (QEST), IEEE CS Press, 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.
  Erika Ábrahám. An Assertional Proof System for Multithreaded Java — Theory and Tool Support. PhD Thesis, University of Leiden, 2004.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A Compositional Operational Semantics for JavaMT. In Verification: Theory and Practice, Celebrating Zohar Manna’s 64th Birthday. pages 290–303. Volume 2772 of lncs. Springer-Verlag, 2004.
  Erika Ábrahám, Marcello M. Bonsangue, Frank S. de Boer, and Martin Steffen. Classes, Object Connectivity, and Observability (Extended abstract). In 12. Kolloquium Programmiersprachen und Grundlagen der Programmierung. University Freiburg, 2004.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Inductive Proof Outlines for Multithreaded Java with Exceptions. In 12. Kolloquium Programmiersprachen und Grundlagen der Programmierung. 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.
  Lars-Ĺke Fredlund, Dilian Gurov, Thomas Noll, Mads Dam, Thomas Arts, and Gennady Chugunov. A Verification Tool for Erlang. Software Tools for Technology Transfer, 4(4):405–420, 2003.
  Thomas Noll. Term Rewriting Models of Concurrency: Foundations and Applications, Habilitation Thesis. RWTH Aachen University, 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.
  Peter Buchholz, Joost-Pieter Katoen, Peter Kemper, and Carsten Tepper. Model-checking large structured Markov chains. J. Log. Algebr. Program, 56(1-2):69–97, 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.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Inductive Proof-Outlines for Monitors in Java. In Formal Methods for Open Object-Based Distributed Systems (FMOODS’03). pages 155–169. Volume 2884 of LNCS. Springer-Verlag, 2003.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A Tool-supported Assertional Proof System for Multithreaded Java. In Workshop on Formal Techniques for Java-like Programs (FTfJP’03). Appeared as technical report 408 from the ETH Zürich, 2003.

2002
  Henrik Bohnenkamp. Compositional Solution of Stochastic Process Algebra Models. PhD Thesis, Department of Computer Science, Rheinisch-Westfälische Technische Hochschule Aachen, Germany, 2002.
  Henrik Bohnenkamp, and Boudewijn R. Haverkort. The Mean Value of the Maximum. In Holger Hermanns, and Roberto Segala, editors, Process Algebra and Probabilistic Methods (PAPM-ProbmiV 2002), Volume 2399 of Lecture Notes in Computer Science. pages 37–56. Springer Verlag, 2002.
  Benedikt Bollig, Martin Leucker, and Thomas Noll. Generalized Regular MSC Languages. In Proceedings 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’02). pages 52–66. Springer-Verlag, 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.
  Dino Distefano, Arend Rensink, and Joost-Pieter Katoen. Model checking birth and death. In Ricardo A. Baeza-Yates, Ugo Montanari, and Nicola Santoro, editors, IFIP Working Conference on Theoretical Computer Science (TCS). pages 435–447. IFIP Proceedings vol. 223, Kluwer Academic Publishers, 2002.
  Holger Hermanns, Ulrich Herzog, and Joost-Pieter Katoen. Process algebra for performance evaluation. Theor. Comput. Sci, 274(1-2):43–87, 2002.
  Joost-Pieter Katoen, and Perdita Stevens, editors, Tools and Algorithms for the Construction and Analysis of Computer Systems (TACAS), LNCS vol. 2280, Springer-Verlag, 2002.

2001
  Lucia Cloth, Henrik Bohnenkamp, and Boudewijn R. Haverkort. Using Max-Plus Algebra for the Evaluation of Stochastic Process Algebra Prefixes. In Luca de Alfaro, and Stephen Gilmore, editors, Process Algebra and Probabilistic Methods (PAPM-ProbmiV 2001), Volume 2165 of Lecture Notes in Computer Science. Springer Verlag, 2001.
  Lars-Ĺke Fredlund, Dilian Gurov, and Thomas Noll. Semi-Automated Verification of Erlang Code. In Proc. 16th IEEE International Conference on Automated Software Engineering (ASE’01). pages 319–323. IEEE Computer Society Press, 2001.
  Martin Leucker, and Thomas Noll. Truth/SLC – A Parallel Verification Platform for Concurrent Systems (tool description). In Proceedings 13th Conference on Computer Aided Verification (CAV’01). pages 255–259. Springer-Verlag, 2001.
  Thomas Noll. A Rewriting Logic Implementation of Erlang. In Didier Parigot, and Mark van den Brand, editors, Proceedings of First Workshop on Language Descriptions, Tools and Applications (ETAPS/LDTA’01). Elsevier Science Publishers, 2001.
  Thomas Noll, Lars-Ĺke Fredlund, and Dilian Gurov. The Erlang Verification Tool (tool description). In Proceedings 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’01). pages 582–585. Volume 2031 of Lecture Notes in Computer Science. 2001.
  Thomas Arts, and Thomas Noll. Verifying Generic Erlang Client–Server Implementations. In Selected Papers of the 12th International Workshop on the Implementation of Functional Languages (IFL’00). pages 37–52. 2001.
  Martin Leucker, and Thomas Noll. Rewriting Logic as a Framework for Generic Verification Tools. In Proceedings of Third International Workshop on Rewriting Logic and Its Applications (WRLA’00). Elsevier, 2001.
  Theo C. Ruys, Rom Langerak, Joost-Pieter Katoen, Diego Latella, and Mieke Massink. First passage time analysis of stochastic process algebra using partial orders. In Tiziana Margaria, and Wang Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 220–236. LNCS vol. 2031, Springer-Verlag, 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.
  Joost-Pieter Katoen, Marta Kwiatkowska, Gethin Norman, and David Parker. Faster and Symbolic CTMC Model Checking. In Luca de Alfaro, and Stephen Gilmore, editors, Process Algebra and Probabilistic Methods (PAPM-Probmiv). pages 23–38. LNCS vol. 2165, Springer-Verlag, 2001.
  Joost-Pieter Katoen, Christel Baier, and Diego Latella. Metric semantics for true concurrent real time. Theor. Comput. Sci, 254(1-2):501–542, 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.
  Erika Ábrahám, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Proof Outlines for Threads in Java. In 11th Kolloquium Programmiersprachen und Grundlagen der Programmierung. 2001.

2000
  Boudewijn R. Haverkort, Henrik C. Bohnenkamp, and Connie U. Smith, editors, Computer Performance Evaluation—Modelling Techniques and Tools (Proceedings TOOLS 2000), Springer Verlag, 2000.
  Thomas Noll, and Heiko Vogler. The Universality of Higher-Order Attributed Tree Transducers. Theory of Computing Systems, :45–75, 2000.
  Thomas Arts, and Thomas Noll. Verifying Generic Erlang Client-Server Implementations. In Proceedings of the 12th International Workshop on Implementation of Functional Languages (IFL’00). pages 387–402. RWTH Aachen University, 2000.
  Martin Leucker, and Thomas Noll. Truth – A Real-World Application in Haskell. In Proceedings of the 12th International Workshop on Implementation of Functional Languages (IFL’00). pages 363–380. RWTH Aachen University, 2000.
  Mads Dam, and Thomas Noll. Context–Representable Processes (abstract). In Proceedings of Dagstuhl Seminar on Verification of Infinite–State Systems. pages 19–22. Schloß Dagstuhl, 2000.
  Dino Distefano, Joost-Pieter Katoen, and Arend Rensink. A temporal logic for object-based systems. In Scott F. Smith, and Carolyn L. Talcott, editors, Formal Methods for Open Object-based Distributed Systems IV (FMOODS). pages 305–326. IFIP Proceedings vol. 177, Kluwer Academic Publishers, 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.
  Joost-Pieter Katoen, and Albert Nymeyer. Pattern-matching algorithms based on term rewrite systems. Theor. Comput. Sci, 238(1-2):439–464, 2000.
  Dino Distefano, Joost-Pieter Katoen, and Arend Rensink. Towards model checking OCL. In A. Moreira, J.-M. Bruel, R. France, and S. Kent, editors, ECOOP-Workshop on Defining Precise Semantics for UML. Sophia-Antipolis, France, 10 pages. 2000.

1999
  Boudewijn R. Haverkort, Alexander Bell, and Henrik Bohnenkamp. On the efficient sequential and distributed Evaluation of very large stochastic Petri nets. In Peter Buchholz, and Manuel Silva, editors, Proceedings of the Eighth International Workshop on Petri Nets and Performance Models, pages 12–21. IEEE Computer Society Press, 1999.
  Henrik Bohnenkamp, and Boudewijn R. Haverkort. Stochastic event structures for the decomposition of stochastic process algebra models. In Jane Hillston, and Manuel Silva, editors, Proceedings of the Seventh International Workshop on Process Algebras and Performance Modelling (PAPM ’99), pages 25–39. Prensas Universitarias de Zaragoza, 1999.
  Henrik C. Bohnenkamp, and Boudewijn R. Haverkort. Semi-Numerical Solution of Stochastic Process Algebra Models. In Joost-Pieter Katoen, editor, Proceedings of the 5th International AMAST Workshop, ARTS ’99, Volume 1601 of Lecture Notes in Computer Science. pages 228–243. Springer-Verlag, 1999.
  Joost-Pieter Katoen, editor, Proceedings of the 5th International AMAST Workshop, ARTS ’99, Volume 1601 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
  Thomas Noll. Kohärenzeigenschaften in termersetzungsbasierten Modellen für verteilte Systeme (abstract). In F. Otto, and Gundula Niemann, editors, 9. Theorietag der GI-Fachgruppe 0.1.5 “Automaten und Formale Sprachen”. pages 52–52. University of Kassel, 1999.
  Thomas Noll. On Coherence Properties in Term Rewriting Models of Concurrency. In Proceedings of the 10th International Conference on Concurrency Theory (CONCUR’99). pages 478–493. Springer-Verlag, 1999.
  Martin Leucker, and Thomas Noll. Rapid Prototyping of Specification Language Implementations. In Proceedings of the 10th IEEE International Workshop on Rapid System Prototyping (RSP’99). pages 60–65. IEEE Computer Society Press, 1999.
  Martin Lange, Martin Leucker, Thomas Noll, and Stephan Tobies. Truth – A Verification Platform for Concurrent Systems. In Tool Support for System Specification, Development, and Verification. pages 150–159. Springer-Verlag Wien, 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, Joost-Pieter Katoen, and Ed Brinksma. Specification and analysis of soft real-time systems: quality and quantity. In IEEE Real-Time Systems Symposium (RTSS). pages 104–114. IEEE Computer Society Press, 1999.
  Pedro R. D’Argenio, Holger Hermanns, and Joost-Pieter Katoen. On Generative Parallel Composition. Electronic Notes in Theoretical Computer Science, 22, 1999.

1998
  Thomas Noll. Rewriting Logic als Grundlage für einen Prozeßalgebra–Compiler (abstract). In Helmut Seidl, editor, 8. Theorietag der GI-Fachgruppe 0.1.5 Äutomaten und Formale Sprachen". pages 46–46. University of Trier, 1998.
  Martin Lange, Martin Leucker, Thomas Noll, and Stephan Tobies. Truth – A Verification Platform for Concurrent Systems (extended abstract). In Proceedings of Tools’98. pages 21–26. Christian-Albrechts University of Kiel, 1998.
  Can Adam Albayrak, and Thomas Noll. The WHILE Hierarchy of Program Schemes is Infinite. In Maurice Nivat, editor, Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS’98). pages 35–47. Springer-Verlag, 1998.
  Joost-Pieter Katoen, Rom Langerak, Ed Brinksma, Diego Latella, and Tommaso Bolognesi. A Consistent Causality-Based View on a Timed Process Algebra Including Urgent Interactions. Formal Methods in System Design, 12(2):189–216, 1998.
  Joost-Pieter Katoen, and Lennard Lambert. Pomsets for message sequence charts. In Hartmut König, and Peter Langendörfer, editors, Formale Beschreibungstechniken für verteilte Systeme (FBT). pages 197–208. Shaker Verlag, 1998.
  Howard Bowman, and Joost-Pieter Katoen. A True Concurrency Semantics for ET-LOTOS. In International IEEE Conference on Applications of Concurrency to System Design (CSD). pages 228–239. IEEE Computer Society Press, 1998.
  Pedro R. D’Argenio, Joost-Pieter Katoen, and Ed Brinksma. An algebraic approach to the specification of stochastic systems (extended abstract). In David Gries, and Willem-Paul de Roever, editors, IFIP Working Conference on Programming Concepts and Methods (PROCOMET). pages 126–148. Chapman & Hall, 1998.
  Howard Bowman, Giorgio P. Faconti, Joost-Pieter Katoen, Diego Latella, and Mieke Massink. Automatic Verification of a Lip-Synchronisation Protocol Using Uppaal (Extended version). Formal Aspects of Computing, 10(5-6):550–575, 1998.
  Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, and Diego Latella. Partial-order models for quantitative extensions of LOTOS. Computer Networks & ISDN Systems, 30(9-10):925–950, 1998.
  Christel Baier, Joost-Pieter Katoen, and Diego Latella. Metric Semantics for True Concurrent Real Time. In Kim G. Larsen, S. Skyum, and G. Winskel, editors, Automata, Languages, and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science. pages 568–580. Springer, 1998.
  Pedro R. D’Argenio, Joost-Pieter Katoen, and Ed Brinksma. General purpose discrete-event simulation using SPADES. In C. Priami, editor, 6th International Workshop on Process Algebra and Performance Modelling (PAPM). pages 85–103. 1998.
  Pedro R. D’Argenio, Joost-Pieter Katoen, and Ed Brinksma. A compositional approach to generalised semi-Markov processes. In 4th Int. Workshop on Discrete-Event Systems (WODES). pages 391–397. IEE Press, 1998.

1997
  Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, and Jan Tretmans. The Bounded Retransmission Protocol Must Be on Time!. In Ed Brinksma, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1217 of Lecture Notes in Computer Science. pages 416–432. Springer-Verlag, 1997.
  Rom Langerak, Ed Brinksma, and Joost-Pieter Katoen. Causal ambiguity and partial orders. In Antoni Mazurkiewicz, and Józef Winkowski, editors, Concurrency Theory (CONCUR), volume 1243 of Lecture Notes in Computer Science. pages 317–332. Springer-Verlag, 1997.
  Albert Nymeyer, and Joost-Pieter Katoen. Code generation based on formal bottom-up rewrite systems theory and heuristic search. Acta Informatica, 34(4):597–635, 1997.
  Pedro R. D’Argenio, Joost-Pieter Katoen, and Ed Brinksma. A stochastic automata model and its algebraic approach. In Ed Brinksma, and Albert Nymeyer, editors, 5th International Workshop on Process Algebra and Performance Modelling (PAPM) CTIT Technical Report 97-14. pages 1–16. 1997.

1996
  Thomas Noll, and Stefan Roßmanith. Parallel Evaluation of LR-Attributed Grammars. In Peter Fritzson, editor, Proceedings of the Poster Session of CC’96. pages 105–112. Linköping University, 1996.
  Joost-Pieter Katoen, and Berry Schoenmakers. Systolic arrays for the recognition of permutation-invariant segments. Science of Computer Programming, 27(2):119–137, 1996.
  G. Karagiannis, Joost-Pieter Katoen, and I.G.M.M. Niemegeers. B-ISDN to the cell site switch versus B-ISDN to the mobile terminal. In IEEE International Conference on Communicating Systems (ICCS). pages 629–633. IEEE Press, 1996.
  Joost-Pieter Katoen. Quantitative and qualitative extensions of event structures. PhD Thesis, University of Twente, 1996.
  Jacob Brunekreef, Joost-Pieter Katoen, Ron Koymans, and Sjouke Mauw. Design and Analysis of Dynamic Leader Election Protocols in Broadcast Networks. Distributed Computing, 9(4):157–171, 1996.
  Joost-Pieter Katoen, Rom Langerak, Diego Latella, and Ed Brinksma. On specifying realtime systems in a causality-based setting. In Bengt Jonsson, and Joachim Parrow, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), volume 1135 of Lecture Notes in Computer Science. pages 385–405. Springer, 1996.
  Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, and Jan Tretmans. Modelling and verifying a bounded retransmission protocol using Uppaal. In Z. Brezocnik, and T. Kapus, editors, COST 247 Int. Workshop on Applied Formal Methods in System Design. pages 114–128. 1996.
  Joost-Pieter Katoen, Diego Latella, Ed Brinksma, and Rom Langerak. Stochastic simulation of event structures. In M. Ribaudo, editor, 4th International Workshop on Process Algebra and Performance Modelling (PAPM). pages 21–40. CLUT Press, 1996.
  Albert Nymeyer, Joost-Pieter Katoen, Ymte Westra, and Henk Alblas. Code generation = A* + BURS. In Tibor Gyimothy, editor, Compiler Construction (CC), volume 1060 of Lecture Notes in Computer Science. pages 160–177. Springer-Verlag, 1996.

1995
  Thomas Noll. Klassen applikativer Programmschemata und ihre Berechnungsstärke. PhD Thesis, RWTH Aachen University, 1995.
  Joost-Pieter Katoen. Functional integration of B-ISDN and UMTS. In 45th IEEE Vehicular Technology Conference (VTC). pages 163–168. IEEE Press (extended version as Technical Report 95-02, University of Twente), 1995.
  Joost-Pieter Katoen. Causal behaviours and nets. In Giorgio De Michelis, and Michel Diaz, editors, Application and Theory of Petri Nets 1995 (ATPN), volume 935 of Lecture Notes in Computer Science. pages 258–277. Springer, 1995.
  Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, and Diego Latella. A stochastic causality-based process algebra. The Computer Journal, 38(7):552–565, 1995.
  Marten Sinderen van, Luís Ferreira Pires, Chris A. Vissers, and Joost-Pieter Katoen. A design model for open distributed processing systems. Computer NetworksISDN Systems, 27(6):1263–1285, 1995.

1994
  Thomas Noll. On the First-Order Equivalence of Call-by-Name and Call-by-Value. In Sophie Tison, editor, Proceedings of CAAP’94. pages 246–260. Springer-Verlag, 1994.
  Thomas Noll, and Heiko Vogler. Top-Down Parsing with Simultaneous Evaluation of Noncircular Attribute Grammars. Fundamenta Informaticae, 20:285–332, 1994.
  Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, and Diego Latella. Performance analysis and true concurrency semantics. Theories and Experiences for Real-Time System Development, chapter 12, AMAST Series in Computing, 2:309–337, 1994.
  Jacob Brunekreef, Joost-Pieter Katoen, Ron Koymans, and Sjouke Mauw. Algebraic specification of dynamic leader election protocols in broadcast networks. In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Algebra of Communicating Processes (ACP), Workshops in Computing. pages 338–357. Springer-Verlag, 1994.
  Joost-Pieter Katoen, Rom Langerak, Diego Latella, and Ed Brinksma. Performance analysis and true concurrency semantics (extended abstract). In Ulrich Herzog, and M. Rettelbach, editors, 2nd Workshop on Process Algebra and Performance Modelling (PAPM), Band 27(4) of Arbeitsberichte des Instituts für Mathematische Maschinen und Datenverarbeitung. pages 157–174. 1994.
  Joost-Pieter Katoen, Rom Langerak, and Diego Latella. Modelling systems by probabilistic process algebra: an event structures approach. In Richard L. Tenney, Paul D. Amer, and Ümit M. Uyar, editors, Formal Description Techniques VI (FORTE), volume C–22 in IFIP Transactions. pages 253–268. North-Holland, 1994.

1993
  Andrea Kindler, Thomas Noll, and Bernhard Steffen. Hierarchical Parallelization of Imperative Programs. In Peter Milligan, and Antonio Nunez, editors, Proceedings of Euromicro Workshop on Parallel and Distributed Processing. pages 178–184. IEEE Computer Society Press, 1993.
  Joost-Pieter Katoen, and M. Rem. Recognizing K-rotated segments. International Journal of High Speed Computing, 5(2):293–305, 1993.
  Joost-Pieter Katoen. A semi-Markov model of a home network access protocol. In Herbert D. Schwetman, Jean C. Walrand, Kallol Kumar Bagchi, and Doug DeGroot, editors, Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS), vol. 25 of Simulation Series. pages 293–299. 1993.

1992
  Joost-Pieter Katoen, and Berry Schoenmakers. A parallel program for recognizing P-invariant segments. In Patrice Quinton, and Yves Robert, editors, Algorithms and Parallel VLSI Architectures II. pages 79–85. North-Holland, 1992.

1991
  Thomas Noll. Verbesserung des Kennedy-Warren-Auswertungsalgorithmus für attributierte Grammatiken durch Graphreduktion, Master’s Thesis. RWTH Aachen University, 1991.

1989
  C. Hemerik, and Joost-Pieter Katoen. Bottom-up tree acceptors. Science of Computer Programming, 13(1):51–72, 1989.