Publications of the MOVES Group

Technical reports are listed separately.


2012
  Christel Baier, E. Moritz Hahn, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model Checking for Performability. Mathematical Structures in Computer Science, :1–42, 2012.
  Kamal Barakat, and Thomas Noll. A Native Approach to Modeling Timed Behavior in the Pi-Calculus (short paper). In Proc. of 6th IEEE Int. Symp. on Theoretical Aspects of Software Engineering (TASE 2012). 2012.
  Alessandro D’Innocenzo, Alessandro Abate, and Joost-Pieter Katoen. Robust PCTL Model Checking. In Hybrid Systems: Computation and Control (HSCC). ACM Press, 2012.
 
Marie-Aude Esteve, Joost-Pieter Katoen, Viet Yen Nguyen, Bart Postma, and Yuri Yushtein. Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite. In 34th Int. Conf. on Software Engineering (ICSE 2012). ACM and IEEE CS Press, 2012.
  Muhammad Fadlisyah, Peter Csaba Ölveczky, and Erika Abraham. Some Like It Very Hot: Formal Modeling and Analysis of Extreme Heat Exposure to the Human Body in HI-Maude. In Proc. of the 9th International Workshop on Rewriting Logic and its Applications (WRLA’12). LNCS. Springer-Verlag, 2012.
 
Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuhäußer. Quantitative Timed Analysis of Interactive Markov Chains. In NASA Formal Methods Symposium (NFM). pages 8–23. Volume 7226 of Lecture Notes in Computer Science. Springer-Verlag, 2012.
  E. Moritz Hahn, Arnd Hartmanns, Holger Hermanns, and Joost-Pieter Katoen. A Compositional Modeling and Analysis Framework for Stochastic Hybrid Systems. Formal Methods in System Design, , 2012.
 
Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga, and Mark Timmer. A linear process-algebraic format with data for probabilistic automata. Theoretical Computer Science, 413:36–57, 2012.
 
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, and Verena Wolf. Three-Valued Abstraction for Probabilistic Systems. Journal on Logic and Algebraic Programming, :1–55, 2012.
 
Joost-Pieter Katoen. Model Checking: One Can Do Much More Than You Think!. In Fundamentals of Software Engineering (FSEN). pages 1–14. Volume 7141 of LNCS. Springer-Verlag, 2012.
  Daniela Lepri, Erika Abraham, and Peter Csaba Ölveczky. Timed CTL Model Checking in Real-Time Maude. In Proc. of the 9th International Workshop on Rewriting Logic and its Applications (WRLA’12). LNCS. Springer-Verlag, 2012.
  Etienne Lozes, Florent Jacquemard, Jules Villard, and Ralf Treinen. Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus. In Theory of Security and Applications (TOSCA 2011). pages 166–185. Volume 6993 of LNCS. 2012.
 
Johanna Nellen, and Erika Abraham. Hybrid Sequential Function Charts. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV’12). 2012.
  Arpit Sharma, and Joost-Pieter Katoen. Weighted Lumpability on Markov Chains. In 8th Ershov Informatics Conference (PSI 2011) . Volume 7162 of LNCS. Springer Verlag, 2012.
  Arpit Sharma. Weighted Probabilistic Equivalence Preserves omega-Regular Properties. In 16th Measurement, Modeling, and Evaluation of Computing Systems and Dependability and Fault Tolerance Conference (MMB/DFT). Volume 7201 of LNCS. Springer Verlag, 2012.
  Bart Theelen, Joost-Pieter Katoen, and Hao Wu. Model Checking of Scenario-Aware Dataflow with CADP. In Design, Automation, and Test in Europe (DATE) . ACM Press, 2012.
 
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, and Bernd Becker. Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV’12). 2012.
 
Ralf Wimmer, Nils Jansen, Erika Abraham, Bernd Becker, and Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS’12). pages 299–314. Volume 7214 of LNCS . Springer, 2012.

2011
 
Alessandro Abate, Joost-Pieter Katoen, and Alexandru Mereacre. Quantitative Automata Model Checking of Autonomous Stochastic Hybrid Systems. In 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC). pages 83–92. ACM Press, 2011.
 
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. A two-step scheme for approximate model checking of stochastic hybrid systems. In Proceedings 18th IFAC World Congress 2011. Volume 18 of IFAC-PapersOnLine. Elsevier, 2011.
 
Erika Abraham, Tobias Schubert, Bernd Becker, Martin Fraenzle, and Christian Herde. Parallel SAT Solving in Bounded Model Checking. Journal of Logic and Computation, 21(1):5–21, 2011.
 
Erika Abraham, Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, and Ulrik Schroeder. On Collaboratively Conveying Computer Science to Pupils. In Proc. of the 11th Koli Calling Int. Conf. on Computing Education Research (KOLI’11). 2011.
 
Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. Efficient CTMC Model Checking of Linear Real-Time Objectives. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 128–142. Volume 6605 of LNCS. 2011.
 
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 2008). pages 103–117. Volume 4980 of LNCS. 2011.
 
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, and Erika Abraham. SMT-based Counterexample Generation for Markov Chains. In Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV). 2011.
 
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, and Erika Abraham. Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking. In Formal Techniques for Distributed Systems (FMOODS/FORTE’11). pages 75–89. Volume 6722 of LNCS. Springer-Verlag, 2011.
 
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, and Erika Abraham. SMT-based Counterexample Generation for Discrete-Time Markov Chains. In Workshop on Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems (ROCKS’11). 2011.
 
Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. Logical Methods in Computer Science, 7(1-2):1–34, 2011.
 
Xin Chen, and Erika Abraham. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems. In 13th Int. Conf. on Computer Aided Systems Theory (EUROCAST’11). LNCS. Springer-Verlag, 2011.
 
Xin Chen, Erika Abraham, and Goran Frehse. Efficient Bounded Reachability Computation for Rectangular Automata. In 5th Workshop on Reachability Problems (RP’11). pages 139–152. Volume 6945 of LNCS. Springer-Verlag, 2011.
 
Taolue Chen, Tingting Han, Joost-Pieter Katoen, and Alexandru Mereacre. Observing Continuous-Time MDPs by 1-Clock Timed Automata. In Workshop on Reachability Problems (RP). pages 2–25. Volume 6945 of LNCS. Springer-Verlag, 2011.
 
Florian Corzilius, and Erika Abraham. Virtual Substitution for SMT Solving. In 18th Int. Symp. on Fundamentals of Computation Theory (FCT’11). pages 360–371. Volume 6914 of LNCS. Springer-Verlag, 2011.
 
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, and Andrzej Wasowski. Abstract Probabilistic Automata. In Verification, Model Checking and Abstract Interpretation (VMCAI). pages 324–339. Volume 6538 of LNCS. Springer-Verlag, 2011.
  Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, and Andrzej Wasowski. New Results on Abstract Probabilistic Automata. In Applications of Concurrency to System Design (ACSD). pages 118–127. IEEE CS Press, 2011.
 
Muhammad Fadlisyah, Peter Csaba Ölveczky, and Erika Abraham. Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems. In Int. Workshop on Harnessing Theories for Tool Support in Software (TTSS’10). pages 17–32. Volume 274 of ENTCS. Elsevier Science Publishers, 2011.
 
Muhammad Fadlisyah, Peter Csaba Ölveczky, and Erika Abraham. Formal Modeling and Analysis of Hybrid Systems in Rewriting Logic using Higher-Order Numerical Methods and Discrete-Event Detection. In Int. Symposium on Computer Science and Software Engineering (CSSE’11). pages 1–8. IEEE, 2011.
 
Muhammad Fadlisyah, Peter Csaba Ölveczky, and Erika Abraham. Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude. In 9th Int. Conf. on Software Engineering and Formal Methods (SEFM’11). pages 415–430. Volume 7041 of LNCS. Springer-Verlag, 2011.
  Hongfei Fu. Model Checking EGF on Basic Parallel Processes. In 9th International Symposium on Automated Technology for Verification and Analysis (ATVA). pages 120–134. Volume 6996 of LNCS. Springer, 2011.
 
Hongfei Fu, and Joost-Pieter Katoen. Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems. In Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LIPIcs. Schloss Dagstuhl, 2011.
  E. Moritz Hahn, Tingting Han, and Lijun Zhang. Synthesis for PCTL in Parametric Markov Decision Processes. In NASA Formal Methods - Third International Symposium (NFM). pages 146–161. Volume 6617 of LNCS. 2011.
 
Jonathan Heinen, and Christina Jansen. Juggrnaut - An Abstract JVM. In Formal Verification of Object-Oriented Software. Papers presented at the 2nd International Conference, October 5-7, 2011, Turin, Italy. pages 226–243. Volume 2011 of Karlsruhe Reports in Informatics. Karlsruhe, 2011.
 
Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, and Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars. In 5th Int. Conf. on Language and Automata Theory and Applications (LATA 2011). pages 323–335. Volume 6638 of LNCS. Springer-Verlag, 2011.
 
Nils Jansen, Erika Abraham, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker. Hierarchical Counterexamples for Discrete-Time Markov Chains. In 9th Int. Symp. on Automated Technology for Verification and Analysis (ATVA’11). pages 443–452. Volume 6996 of LNCS. Springer-Verlag, 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.
 
Joost-Pieter Katoen. Towards Trustworthy Aerospace Systems: An Experience Report. In 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS). pages 1–4. Volume 6959 of LNCS. Springer-Verlag, 2011.
  Joost-Pieter Katoen, and Thomas Noll. Trustworthy Aerospace Systems. Public Service Review: European Science and Technology, 11:204–205, 2011.
  Joost-Pieter Katoen, and Barbara König, editors, 22nd Conference on Concurrency Theory (CONCUR), Volume 6901 of LNCS. Springer-Verlag, 2011.
 
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, and Joost-Pieter Katoen. Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. Performance Evaluation, 68(2):105–125, 2011.
 
Ulrich Loup, and Erika Abraham. GiNaCRA: A C++ Library for Real Algebraic Computations. In 3rd NASA Formal Methods Symposium (NFM’11). pages 512–517. Volume 6617 of LNCS. Springer-Verlag, 2011.
 
Ulrich Loup, and Erika Abraham. I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra. In 4th Int. Conf. on Algebraic Informatics (CAI’11). pages 230–246. Volume 6742 of LNCS. Springer-Verlag, 2011.
  Alexandru Mereacre. Verification of Continuous-Space Stochastic Systems. PhD Thesis, RWTH Aachen University, 2011.
  Ralf Mitsching, Frank Fiedler, Henrik Bohnenkamp, Carsten Weise, and Stefan Kowalewski. TripleT: Improving Test Responsiveness for High Performance Embedded Systems. In Proc. 4th IEEE International Conference on Software Testing, Verification, and Validation (ICSTW). pages 67–74. IEEE, 2011.
  Thomas Noll. Analyzing Reconfigurable Component-Based Systems Using Attribute Grammars. In Proc. 8th Int. Symp. on Formal Aspects of Component Software (FACS). LNCS. Springer, 2011.
 
Pascal Richter, Erika Abraham, and Gabriel Morin. Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks. In Int. Conf. on Adaptive and Natural Computing Algorithms (ICANNGA’11). pages 190–199. Volume 6593 of LNCS. Springer-Verlag, 2011.
 
Bastian Schlich, Thomas Noll, Jörg Brauer, and Lucas Brutschy. Reduction of Interrupt Handler Executions for Model Checking Embedded Software. In Proc. of 5th Int. Haifa Verification Conference (HVC 2009). pages 5–20. Volume 6405 of LNCS. Springer, 2011.
  Arpit Sharma. Weighted Lumpability on Markov Chains.. PSI Conference, Novosibirsk, Russia, 2011. Conference presentation.
  Sabrina von Styp, Liyong Yu, and Gustavo Quirós. Automatic Test-Case Derivation and Execution in Industrial Control. In iATPA 2011: First Workshop on Industrial Automation Tool Integration for Engineering Project Automation. CEUR-WS, 2011.
 
Haidi Yue, Henrik Bohnenkamp, Malte Kampschulte, and Joost-Pieter Katoen. Analysing and Improving Energy Efficiency of Distributed Slotted Aloha. In 11th Int. Conf. on Next Generation Wired/Wireless Advanced Networking (NEW2AN). pages 197–208. Volume 6869 of LNCS. Springer-Verlag, 2011.
 
Yuri Yushtein, Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive, and Marco Roveri. System-Software Co-Engineering: Dependability and Safety Perspective. In 4th IEEE Int. Conf. on Space Mission Challenges in Information Technology (SMC-IT 2011). pages 18–25. IEEE CS Press, 2011.

2010
 
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, and Maria Prandini. Approximate model checking of stochastic hybrid systems. European Journal of Control, 16(6):624–641, 2010.
 
Erika Abraham, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, and Bernd Becker. DTMC Model Checking by SCC Reduction . In 7th Int. Conf. on Quantitative Evaluation of Systems (QEST’10). pages 37–46. IEEE CS Press, 2010.
 
Erika Abraham, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, and Ulrik Schroeder. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik. In Interaktive Kulturen - Die 8. E-Learning Fachtagung Informatik (DeLFI’10). pages 239–251. Volume 169 of LNI. Gesellschaft für Informatik, 2010.
 
Erika Abraham, Ulrich Loup, Florian Corzilius, and Thomas Sturm. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra. 8th Int. Workshop on Satisfiability Modulo Theories (SMT’10), 2010.
 
Erika Abraham, Ulrich Loup, Ralf Wimmer, and Joost-Pieter Katoen. On the Minimization of Hybrid Automata. In Nordic Workshop on Programming Theory (NWPT’10). 2010.
 
Erika Abraham, Ulrich Loup, Florian Corzilius, and Thomas Sturm. SMT-Solving in the Analysis and Synthesis of Hybrid Systems. In Verification over Discrete-Continuous Boundaries, Dagstuhl Seminar. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 2010.
  Erika Abraham. Tutorial on Satisfiability Checking. Tutorial, AlgoSyn meeting, Rolduc, Germany, 2010.
 
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Performance Evaluation and Model Checking Join Forces. Communications of the ACM, 53(9):76–85, 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, 36(1):1–36, 2010.
 
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, and Martin Leucker. Learning Communicating Automata from MSCs. IEEE Transactions on Software Engineering, 36(3):390–408, 2010.
 
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, and Martin Leucker. SMA: The Smyle Modeling Approach. Computing and Informatics, 29:45–72, 2010.
 
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, and David Piegdon. libalf: the Automata Learning Framework. In Computer-Aided Verification (CAV). pages 360–364. Volume 6174 of LNCS. Springer-Verlag, 2010.
 
Kai Bollue, Michaela Slaats, Erika Abraham, Wolfgang Thomas, and Dirk Abel. Synthesis of Behavioral Controllers for DES: Increasing Efficiency. In 10th Int. Workshop on Discrete-Event Systems (WODES’10). pages 30–37. IFAC, 2010.
  Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, and Xavier Olive. Formal Verification and Validation of AADL Models. In Proc. of Embedded Real Time Software and Systems Conf. (ERTS2 2010). 2010.
  Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, and Marco Roveri. Safety, Dependability, and Performance Analysis of Extended AADL Models. The Computer Journal, doi: 10.1093/com, 2010.
 
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, and Ralf Wimmer. A Model Checker for AADL. In Proc. of 22nd Int. Conf. on Computer Aided Verification (CAV 2010). pages 562–565. Volume 6174 of LNCS. Springer, 2010.
  Jörg Brauer, Thomas Noll, and Bastian Schlich. Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software. In Proc. 13th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2010). Digital Library. ACM, 2010.
  Jörg Brauer, Volker Kamin, Stefan Kowalewski, and Thomas Noll. Loop Refinement Using Octagons and Satisfiability. In Proc. of 5th International Workshop on Systems Software Verification (SSV 2010). 2010.
 
Falko Dulat, Joost-Pieter Katoen, and Viet Yen Nguyen. Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report. In Proceedings of 7th European Performance Engineering Workshop (EPEW 2010). pages 115–130. Volume 6342 of LNCS. Springer, 2010.
 
Muhammad Fadlisyah, Erika Abraham, Daniela Lepri, and Peter Csaba Ölveczky. A Rewriting-Logic-Based Technique for Modeling Thermal Systems. In 1st Int. Workshop on Rewriting Techniques for Real-Time Systems (RTRTS’10). pages 82–100. Volume 36 of Electronic Proceedings in Theoretical Computer Science. 2010.
 
Muhammad Fadlisyah, Erika Abraham, and Peter Csaba Ölveczky. Rewriting-Logic-Based Formal Modeling and Analysis of Interacting Hybrid Systems. In Nordic Workshop on Programming Theory (NWPT’10). 2010.
  Markus Geimer, Felix Wolf, Brian J. N. Wylie, Erika Abraham, Daniel Becker, and Bernd Mohr. The Scalasca Performance Toolset Architecture. Concurrency and Computation: Practice and Experience, 22(6):702–719, 2010.
  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 2009). pages 93–107. Volume 266 of ENTCS. Elsevier, 2010.
 
Holger Hermanns, and Joost-Pieter Katoen. The How and Why of Interactive Markov Chains. In Formal Methods for Components and Objects (FMCO). pages 311–337. Volume 6286 of LNCS. Springer-Verlag, 2010.
 
Marijn R. Jongerden, Alexandru Mereacre, Henrik Bohnenkamp, Boudewijn R. Haverkort, and Joost-Pieter Katoen. Computing Optimal Schedules for Battery Usage in Embedded Systems. IEEE Transactions on Industrial Informatics, 6(3):276–286, 2010.
  Natalia Kalinnik, Erika Abraham, Tobias Schubert, Ralf Wimmer, and Bernd Becker. Exploiting Different Strategies for the Parallelization of an SMT Solver. In 13. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV’10). pages 97–106. Fraunhofer Verlag, 2010.
 
Joost-Pieter Katoen. Advances in Probabilistic Model Checking. In Verification, Model Checking, and Abstract Interpretation (VMCAI). pages 25–25. Volume 5944 of Lecture Notes in Computer Science. Springer-Verlag, 2010.
 
Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga, and Mark Timmer. A Linear Process Algebraic Format for Probabilistic Systems with Data. In Applications of Concurrency to System Design (ACSD). IEEE CS Press, 2010.
 
Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll Morgan. Linear-Invariant Generation for Probabilistic Programs. In Static Analysis Symposium (SAS). pages 390–406. Volume 6337 of LNCS. Springer-Verlag, 2010.
 
Daniel Klink. Three-Valued Abstraction for Stochastic Systems. PhD Thesis, RWTH Aachen University, 2010.
 
Daniela Lepri, Peter Csaba Ölveczky, and Erika Abraham. Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications. In 1st Int. Workshop on Rewriting Techniques for Real-Time Systems (RTRTS’10). pages 117–136. Volume 36 of Electronic Proceedings in Theoretical Computer Science. 2010.
  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, 12(5):305–318, 2010.
 
Martin R. Neuhäußer. Model Checking Nondeterministic and Randomly Timed Systems. PhD Thesis, RWTH Aachen University and University of Twente, 2010.
 
Martin R. Neuhäußer, and Lijun Zhang. Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes. In Quantitative Evaluation of Systems (QEST). IEEE CS Press, 2010.
 
Maximilian R. Odenbrett, Viet Yen Nguyen, and Thomas Noll. Slicing AADL Specifications for Model Checking. In Proc. of the 2nd NASA Formal Methods Symp. (NFM 2010). pages 217–221. NASA Conference Proceedings. 2010.
  Sabrina von Styp, Henrik Bohnenkamp, and Julien Schmaltz. A Conformance Testing Relation for Symbolic Timed Automata. In Proc. FORMATS 2010. pages 243–255. Volume 6246 of LNCS. Springer-Verlag, 2010.
 
Haidi Yue, Henrik Bohnenkamp, and Joost-Pieter Katoen. Analyzing Energy Consumption in a Gossiping MAC Protocol. In Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB/DFT). pages 107–119. Volume 5987 of LNCS. Springer-Verlag, 2010.
 
Haidi Yue, and Joost-Pieter Katoen. Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption. In 17th International Conference on Analytical and Stochastic Modelling Techniques and Applications (ASMTA). pages 247–261. Volume 6148 of LNCS. 2010.
 
Lijun Zhang, and Martin R. Neuhäußer. Model Checking Interactive Markov Chains. In Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 53–68. Volume 6015 of Lecture Notes in Computer Science. Springer, 2010.

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.
  Erika Abraham, 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 Abraham, and Ulrich Loup. SMT-Solving for the First-Order Theory of the Reals. In Algorithms and Applications for Next Generation SAT Solvers, Dagstuhl Seminar. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany, 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.
  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). pages 121–130. IEEE CS 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 Proc. 28th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP 2009). pages 173–186. Volume 5775 of LNCS. Springer, 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 Conf. and ACM SIGSOFT Symp. on the Foundations of Software Engineering (ESEC/FSE 2009). pages 285–286. ACM Press, 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). pages 87–91. Volume 507 of CEUR Workshop Proceedings. 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.
 
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.
  Hongfei Fu. Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable. In 7th Asian Symposium on Programming Languages and Systems (APLAS). pages 327–342. Volume 5904 of LNCS. Springer, 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.
 
Tingting Han. Diagnosis, Synthesis and Analysis of Probabilistic Models. PhD Thesis, University of Twente and RWTH Aachen University, 2009.
 
Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik Bohnenkamp, and Joost-Pieter Katoen. Maximizing System Lifetime by Battery Scheduling. In Proc. DSN 2009, pages 63–72. IEEE Computer Society, 2009.
 
Natalia Kalinnik, Tobias Schubert, Erika Abraham, Ralf Wimmer, and Bernd Becker. Picoso - A Parallel Interval Constraint Solver. In Int. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA’09). pages 473–479. CSREA Press, 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.
 
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.
 
Carsten Kern. Learning Communicating and Nondeterministic Automata. PhD Thesis, RWTH Aachen University, 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). pages 133–142. IEEE CS Press, 2009.
  Ralf Mitsching, Carsten Weise, André Kolbe, Henrik Bohnenkamp, and Norbert Berzen. Towards an industrial strength process for timed testing. In IEEE International Conference on Software Testing, Verification, and Validation. pages 29–38. IEEE Computer Society, 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.
 
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.
  Viet Yen Nguyen. Verification and Performance Evaluation of AADL Models. Demonstration at ESEC/FSE 2009, Amsterdam, Netherlands, 2009.
  Stefan Rieger. Verification of Pointer Programs. PhD Thesis, RWTH Aachen University, 2009.
  Sabrina von Styp. Towards a theory for timed symbolic testing. In Proceedings of Formal Methods 2009 Doctoral Symposium. pages 39–45. Volume 09-15 of CS-Report . Technical University Eindhoven, 2009.

2008
  Erika Abraham, 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 Abraham, 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 Abraham, Andreas Grüner, and Martin Steffen. Abstract Interace Behavior of Object-Oriented Languages with Monitors. Theory of Computing Systems, 43(3):322–361, 2008.
 
Christel Baier, and Joost-Pieter Katoen. Principles of Model Checking, MIT Press, 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.
  Henrik Bohnenkamp, and Marielle Stoelinga. Quantitative Testing. In Proceedings 8th ACMIEEE International Conference on Embedded Software (EMSOFT). pages 227–236. ACM 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.
 
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.
 
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.
 
Xin Chen, and Yuxin Deng. Game Characterizations of Process Equivalences. In Proceedings of the 6th Asian Symposium on Programming Languages and Systems (APLAS’08). pages 107–121. Volume 5356 of Lecture Notes in Computer Science. Springer Verlag, 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.
  Markus Geimer, Felix Wolf, Brian J. N. Wylie, Erika Abraham, Daniel Becker, and Bernd Mohr. The SCALASCA Performance Toolset Architecture. In Int. Workshop on Scalable Tools for High-End Computing (STHEC’08). pages 56–65. 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.
 
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.
 
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.
 
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 2008). pages 133–150. Volume 217 of ENTCS. Elsevier, 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.
 
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.
 
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.
 
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.
 
Joost-Pieter Katoen. How to model and analyze gossiping protocols?. ACM Performance Evaluation Review, 36(3):3–6, 2008.
 
Joost-Pieter Katoen. Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques. In Design, Automation and Test in Europe (DATE). pages 86–87. IEEE CS Press, 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.
 
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 2007). pages 185–201. Volume 4899 of LNCS. Springer, 2008.
 
Thomas Noll, and Stefan Rieger. Verifying Dynamic Pointer-Manipulating Threads. In Proceedings 15th International Symposium on Formal Methods (FM 2008). pages 84–99. Volume 5014 of LNCS. 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.
 
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.
  Felix Wolf, Brian J. N. Wylie, Erika Abraham, 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 2nd HLRS Parallel Tools Workshop. pages 157–167. 2008.
 
Ivan S. Zapreev. Model Checking Markov Chains: Techniques and Tools. PhD Thesis, University of Twente, 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.

2007
  Erika Abraham, Marc Herbstritt, Bernd Becker, and Martin Steffen. Bounded Model Checking with Parametric Data Structures. In Int. Workshop on Bounded Model Checking (BMC’06). pages 3–16. Volume 174 (3) of ENTCS. Elsevier Science Publishers, 2007.
  Erika Abraham, 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.
 
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.
  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.
 
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.
 
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.
 
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.
  Marc Herbstritt, Bernd Becker, Erika Abraham, 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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
Thomas Noll, and Stefan Rieger. Composing Transformations to Optimize Linear Code. In Proc. 4th Int. Colloquium on Theoretical Aspects of Computing (ICTAC 2007). pages 425–439. Volume 4711 of LNCS. 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
  Erika Abraham, Tobias Schubert, Bernd Becker, Martin Fraenzle, and Christian Herde. Parallel SAT Solving in Bounded Model Checking. In Parallel and Distributed Methods in Verification (PDMC’06). pages 301–315. Volume 4346 of LNCS. Springer-Verlag, 2006.
  Erika Abraham, Marc Herbstritt, Bernd Becker, and Martin Steffen. Memory-Aware Bounded Model Checking for Linear Hybrid Systems. In 9th. Workshop for Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV’06). pages 153–162. 2006.
  Erika Abraham, Andreas Grüner, and Martin Steffen. Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes. In Logical Approaches to Computational Barriers: 2nd Conf. on Computability in Europe (CiE’06). pages 1–10. Volume 3988 of LNCS. Springer-Verlag, 2006.
  Erika Abraham, Andreas Grüner, and Martin Steffen. Abstract Interface Behavior of Object-Oriented Languages with Monitors. In 8th IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS’06). pages 218–232. Volume 4037 of LNCS. Springer-Verlag, 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.
 
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.
 
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.
 
Mario Bravetti, Holger Hermanns, and Joost-Pieter Katoen. YMCA: Why Markov Chain Algebra?. Electronic Notes in Theoretical Computer Science, 162:107–112, 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.
 
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.
  Tingting Han. Counterexamples in probabilistic model checking. IPA Herfstdagen on Stochastic systems (Bergen, NL), 2006.
  Klaus Indermark, and Thomas Noll. Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information. Acta Informatica, 43:1–43, 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.
 
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.
  Thomas Noll, and Stefan Rieger. Optimization of Straight-Line Code Revisited. Softwaretechnik-Trends, 26(2), 2006.
  Chanchal Kumar Roy, Thomas Noll, Banani Roy, and James R. Cordy. 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.

2005
 
Erika Abraham, 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 Abraham, 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 Abraham, 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 Abraham, 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 LNCS. Springer-Verlag, 2005.
  Erika Abraham, 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.
  Erika Abraham, 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.
 
Erika Abraham. An Assertional Proof System for Multithreaded Java — Theory and Tool Support. PhD Thesis, University of Leiden, 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.
 
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.
  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.
 
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.
  Frank S. de Boer, Marcello M. Bonsangue, Martin Steffen, and Erika Abraham. 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.
  John Fitzgerald, Ian Hayes, and Andrzej Tarlecki, editors, Formal Methods 2005, Volume 3582 of LNCS. Springer-Verlag, 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.
 
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.
  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. Equational Abstractions for Model Checking Erlang Programs. In Proceedings of the International Workshop on Software Verification and Validation (SVV 2003). pages 145–162. Volume 118 of ENTCS. Elsevier, 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.

2004
  Erika Abraham, 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 Abraham, 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 Abraham, 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.
  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, editors, Validation of Stochastic Systems, Volume 2925 of LNCS. Springer-Verlag, 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 Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pages 61–76. LNCS vol. 2988, 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 Foundations of Software Technology and Theoretical Computer Science (FSTTCS). pages 250–262. LNCS vol. 3328, Springer-Verlag, 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.
 
Joost-Pieter Katoen, Henrik Bohnenkamp, Ric Klaren, and Holger Hermanns. Embedded software analysis with MOTOR. In Formal Methods for the Design of Real-Time Systems (SFM-RT 2004). pages 268–294. Volume 3185 of LNCS. 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.

2003
  Erika Abraham, 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 Abraham, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. A Tool-Supported Proof System for Multithreaded Java. In Formal Methods for Components and Objects (FMCO’02). pages 1–32. Volume 2852 of LNCS. Springer-Verlag, 2003.
  Erika Abraham, 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.
  Suzana Andova, Holger Hermanns, and Joost-Pieter Katoen. Discrete-time rewards model-checked. In Formal Methods for Timed Systems (FORMATS). pages 88–104. Volume 2791 of LNCS. Springer-Verlag, 2003.
  Christel Baier, Holger Hermanns, Joost-Pieter Katoen, and Verena Wolf. Comparative branching-time semantics for Markov chains. In Concurrency Theory (CONCUR). pages 492–508. Volume 2761 of LNCS. Springer-Verlag, 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.
 
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.
  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.
  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.
  Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, and Markus Siegle. A tool for model-checking Markov chains. STTT, 4(2):153–172, 2003.
  David N. Jansen, Holger Hermanns, and Joost-Pieter Katoen. A QoS-Oriented Extension of UML Statecharts. In The Unified Modeling Language (UML). pages 76–92. Volume 2853 of LNCS. Springer-Verlag, 2003.
  Thomas Noll. Term Rewriting Models of Concurrency: Foundations and Applications, Habilitation Thesis. RWTH Aachen University, 2003.

2002
  Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Verification for Java’s Reentrant Multithreading Concept. In Foundations of Software Science and Computation Structures (FoSSaCS’02). pages 5–20. Volume 2303 of LNCS. Springer-Verlag, 2002.
  Christel Baier, Joost-Pieter Katoen, Holger Hermanns, and Boudewijn R. Haverkort. Simulation for continuous-time Markov chains. In Concurrency Theory (CONCUR). pages 338–354. Volume 2421 of LNCS. Springer-Verlag, 2002.
  Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Automated performance and dependability evaluation using model checking. In Computer Performance Evaluation. pages 261–289. Volume 2459 of LNCS. Springer-Verlag, 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 2002). pages 52–66. Springer-Verlag, 2002.
  Dino Distefano, Arend Rensink, and Joost-Pieter Katoen. Model checking birth and death. In IFIP Working Conference on Theoretical Computer Science (TCS). pages 435–447. Volume 223 of IFIP Proceedings. Kluwer Academic Publishers, 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.
  Holger Hermanns, and Roberto Segala, editors, Process Algebra and Probabilistic Methods (PAPM-ProbmiV 2002), Volume 2399 of Lecture Notes in Computer Science. 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.
  David N. Jansen, Holger Hermanns, and Joost-Pieter Katoen. A probabilistic extension of UML statecharts – specification and verification. In Formal Techniques for Real-Time and Fault-Tolerant systems (FTRTFT). pages 355–374. Volume 2469 of LNCS. Springer-Verlag, 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
  Erika Abraham, Ulrich Hannemann, and Martin Steffen. Verification of Hybrid Systems: Formalization and Proof Rules in PVS. In IEEE Engineering of Complex Computer Systems (ICECCS’01). pages 48–57. IEEE Computer Society Press, 2001.
  Erika Abraham, Ulrich Hannemann, and Martin Steffen. Assertion-Based Analysis of Hybrid Systems with PVS. In Computer Aided Systems Theory (EUROCAST’01). pages 94–109. Volume 2178 of LNCS. Springer-Verlag, 2001.
  Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, and Martin Steffen. Deductive Verification for Multithreaded Java. In 11. Kolloquium Programmiersprachen und Grundlagen der Programmierung. pages 121–126. 2001.
  Erika Abraham, 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.
  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 2000). pages 37–52. 2001.
  Ed Brinksma, Holger Hermanns, and Joost-Pieter Katoen, editors, Lectures on Formal Methods and Performance Analysis, Volume 2090 of LNCS. Springer-Verlag, 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.
  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.
 
Pedro R. D’Argenio, Holger Hermanns, Joost-Pieter Katoen, and Ric Klaren. MoDeST: A Modelling language for Stochastic Timed systems. In Luca de Alfaro, and Stephen Gilmore, editors, Process Algebra and Probabilistic Methods (PAPM-Probmiv). pages 87–104. LNCS vol. 2165, 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 2001). pages 319–323. IEEE Computer Society Press, 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, 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.
  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.
  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 2001). pages 255–259. Springer-Verlag, 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 2000). Elsevier, 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 2001). 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 2001). pages 582–585. Volume 2031 of Lecture Notes in Computer Science. 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.

2000
  Erika Abraham, and Frank S. de Boer. Proof-Outlines for Threads in Java. In Concurrency Theory (CONCUR’00). pages 229–242. Volume 1877 of LNCS. Springer-Verlag, 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 2000). pages 387–402. RWTH Aachen University, 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.
  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.
  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.
  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.
  Boudewijn R. Haverkort, Henrik Bohnenkamp, and Connie U. Smith, editors, Computer Performance Evaluation—Modelling Techniques and Tools (Proceedings TOOLS 2000), Springer Verlag, 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. 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.
  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.
  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.
  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 2000). pages 363–380. RWTH Aachen University, 2000.
  Jan B. de Meer, and Erika Abraham. Formal Methods for Reflective System Specification. In Formale Beschreibungstechniken für verteilte Systeme. pages 51–57. Shaker Verlag, 2000.
  Thomas Noll, and Heiko Vogler. The Universality of Higher-Order Attributed Tree Transducers. Theory of Computing Systems, 34:45–75, 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.
  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 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.
  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.
  Pedro R. D’Argenio. Algebras and Automata for Timed and Stochastic Systems. PhD Thesis, Department of Computer Science, University of Twente, 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.
  Joost-Pieter Katoen, editor, Proceedings of the 5th International AMAST Workshop, ARTS ’99, Volume 1601 of Lecture Notes in Computer Science. Springer-Verlag, 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.
  Martin Leucker, and Thomas Noll. Rapid Prototyping of Specification Language Implementations. In Proceedings of the 10th IEEE International Workshop on Rapid System Prototyping (RSP 1999). pages 60–65. IEEE Computer Society Press, 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 1999). pages 478–493. Springer-Verlag, 1999.

1998
  Erika Abraham. Bestimmung der Gesichtspose mit künstlichen neuronalen Netzen. Masters Thesis, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu 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 1998). pages 35–47. Springer-Verlag, 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.
  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.
  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.
  J. Bruske, Erika Abraham, J. Pauli, and G. Sommer. Head-pose estimation from facial images with Subspace Neural Networks. In Neural Network and Brain (ICNN&B’98). pages 528–530. Publishing House of Electronics Industry, 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.
  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.
  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.
  Martin Lange, Martin Leucker, Thomas Noll, and Stephan Tobies. Truth – A Verification Platform for Concurrent Systems (extended abstract). In Proceedings of Tools 1998. pages 21–26. Christian-Albrechts University of Kiel, 1998.

1997
  J. Bruske, Erika Abraham, and G. Sommer. Visuomotorische Koordination eines Roboterarmes mit Kohonen-Karten, Neuronalem Gas und Dynamischen Zellstrukturen - Ein Vergleich. In Selbstorganisation von Adaptivem Verhalten (SOAVE’97). pages 203–211. Fortschrittsberichte VDI, Reihe 8, Nr. 663. VDI Verlag, 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.
  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.
  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.

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.
  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.
  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, 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.
  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.
 
Joost-Pieter Katoen, and Berry Schoenmakers. Systolic arrays for the recognition of permutation-invariant segments. Science of Computer Programming, 27(2):119–137, 1996.
  Thomas Noll, and Stefan Roßmanith. Parallel Evaluation of LR-Attributed Grammars. In Peter Fritzson, editor, Proceedings of the Poster Session of CC 1996. pages 105–112. Linköping University, 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
 
Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, and Diego Latella. A stochastic causality-based process algebra. The Computer Journal, 38(7):552–565, 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.
 
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
 
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.
  Thomas Noll. On the First-Order Equivalence of Call-by-Name and Call-by-Value. In Sophie Tison, editor, Proceedings of CAAP 1994. 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.

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.
 
Joost-Pieter Katoen, and Martin Rem. Recognizing K-rotated segments. International Journal of High Speed Computing, 5(2):293–305, 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.

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.

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