Technical Reports

2018
	Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic. Technical report at arxiv number 1802.10467, 2018.
2017
	Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness. Technical report at arxiv number 1705.03754, 2017.
	Marieke Huisman, Thomas Noll, Makoto Tatsuta. Analysis and Verification of Pointer Programs. Technical report at National Institute of Informatics number 2017-14, 2017.
2016
	Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Technical report at arXiv number 1610.07041, 2016.
2015
	Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic. Technical report at RWTH Aachen University number AIB-2015-12, 2015.
2014
	Christina Jansen, Florian Göbe, Thomas Noll. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs. Technical report at RWTH Aachen University number AIB-2014-08, 2014.
2013
	Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. Technical report at Cornell University number arXiv:1312.3979, 2013.
	Viet Yen Nguyen. Trustworthy Spacecraft Design Using Formal Methods. Technical report at RWTH Aachen University number , 2013.
	Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Performance Analysis of Computing Servers using Stochastic Petri Nets and Markov Automata. Technical report at RWTH Aachen University number AIB-2013-10, 2013.
	Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Abraham. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers. Technical report at RWTH Aachen University number AIB-2013-08, 2013.
	Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata. Technical report at Cornell University number arXiv:1305.5055, 2013.
2012
	Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes. Technical report at Reports of SFB/TR 14 AVACS number 88, 2012.
	Nils Jansen, Erika Abraham, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool - Computing Minimal Counterexamples for Discrete-time Markov Chains. Technical report at Cornell University number arXiv:1206.0603v1, 2012.
2011
	Jonathan Heinen, Christina Jansen. Juggrnaut - An Abstract JVM. Technical report at RWTH Aachen University, Germany number AIB 2011-21, 2011.
	Xin Chen, Erika Abraham, Goran Frehse. Efficient Bounded Reachability Computation for Rectangular Automata. Technical report at RWTH Aachen University, Germany number AIB 2011-15, 2011.
	Nils Jansen, Erika Abraham, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical Counterexamples for Discrete-Time Markov Chains. Technical report at RWTH Aachen University number AIB-2011-11, 2011.
	Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars. Technical report at RWTH Aachen University, Germany number AIB 2011-04, 2011.
2010
	Pierre Valadeau. Dependability and FDIR Model Based Analysis. Technical report at EADS Astrium number , 2010.
	Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Computing Maximum Reachability Probabilities in Markovian Timed Automata. Technical report at Computer Science Department, RWTH Aachen University number AIB-2010-06, 2010.
	Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Efficient CTMC Model Checking of Linear Real-Time Objectives. Technical report at RWTH Aachen University number , 2010.
2009
	Joost-Pieter Katoen, Daniel Klink, Martin R. Neuhäußer. Compositional Abstraction for Stochastic Systems. Technical report at RWTH Aachen number AIB-2009-15, 2009.
	Martin R. Neuhäußer, Lijun Zhang. Time-Bounded Reachability in Continuous-Time Markov Decision Processes. Technical report at RWTH Aachen, Department of Computer Science number 2009-12, 2009.
	Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Quantitative model checking of continuous-time Markov chains against timed automata specifications. Technical report at RWTH Aachen University number AIB-2009-02, 2009.
2008
	Benedikt Bollig, Peter Habermehl, Carsten Kern, Martin Leucker. Angluin-Style Learning of NFA. Technical report at Laboratoire Spécification et Vérification, ENS Cachan, France number LSV-08-28, 2008.
	Henrik Bohnenkamp, Marielle Stoelinga. Quantitative Testing. Technical report at RWTH Aachen number AIB-2008-02, 2008.
2007
	Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Compositional Modeling and Minimization of Time-Inhomogeneous Markov Chains. Technical report at RWTH Aachen number AIB-2007-21, 2007.
	Erika Abraham, Immo Grabe, Andreas Grüner, Martin Steffen. Behavioral Interface Description of an Object-Oriented Language with Futures and Promises. Technical report at University of Oslo, Dept. of Computer Science number 364, 2007.
	Martin R. Neuhäußer, Joost-Pieter Katoen. Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. Technical report at RWTH Aachen University, Dept. of Computer Science number AIB 2007-10, 2007.
2006
	Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning. Technical report at RWTH Aachen number AIB-2006-12, 2006.
	Erika Abraham, Andreas Grüner, Martin Steffen. Abstract Interface Behavior of Object-Oriented Languages with Monitors. Technical report at Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number 0612, 2006.
	Tingting Han, Joost-Pieter Katoen. Counterexamples in probabilistic model checking. Technical report at RWTH Aachen number AIB 2006-09, 2006.
	Angelika Mader, Henrik Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann Hurink, Holger Hermanns. Synthesis and Stochastic Assessment of Cost-Optimal Schedules. Technical report at University of Twente number 06-14, 2006.
	Erika Abraham, Andreas Grüner, Martin Steffen. Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes. Technical report at Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number 0601, 2006.
2005
	Erika Abraham, Andreas Grüner, Martin Steffen. An Open Structural Operational Semantics for an Object-Oriented Calculus with Thread Classes. Technical report at Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number 0505, 2005.
	Joost-Pieter Katoen, Ivan S. Zapreev. Safe on-the-fly steady-state detection for time-bounded reachability.. Technical report at CTIT, University of Twente number TR-CTIT-05-52, 2005.
2004
	Henrik Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen. MoDeST: A compositional modeling formalism for real-time and stochastic systems. Technical report at Centre for Telematics and Information Technology, University of Twente number TR-CTIT-04-46, 2004.
	Erika Abraham, Bernd Becker, Felix Klaedke, Martin Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems. Technical report at Albert-Ludwigs-Universität Freiburg, Fakultät für Angewandte Wissenschaften, Institut für Informatik number TR214, 2004.
	Klaus Indermark, Thomas Noll. Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information. Technical report at RWTH Aachen University number 2004-08, 2004.
2003
	Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Inductive Proof Outlines for Multithreaded Java with Exceptions. Technical report at Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number 0313, 2003.
	Erika Abraham, Marcello M. Bonsangue, Frank S. de Boer, Martin Steffen. A Structural Operational Semantics for a Concurrent Class Calculus. Technical report at Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number 0307, 2003.
	Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Hoare Logic for Monitors in Java. Technical report at Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number TR-ST-03-1, 2003.
2002
	Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Compositional Operational Semantics for JavaMT. Technical report at Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number TR-ST-02-2, 2002.
	Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Verification for Java's Reentrant Multithreading Concept: Soundness and Completeness. Technical report at Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number TR-ST-02-1, 2002.
2001
	Erika Abraham, Ulrich Hannemann, Martin Steffen. Verification of Hybrid Systems: Formalization and Proof Rules in PVS. Technical report at Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel number TR-ST-01-1, 2001.
	Benedikt Bollig, Martin Leucker, Thomas Noll. Regular MSC Languages. Technical report at RWTH Aachen University number 01-05, 2001.
2000
	Thomas Arts, Thomas Noll. Verifying Generic Erlang Client-Server Implementations. Technical report at RWTH Aachen University number 2000-08, 2000.
	Pedro R. D'Argenio. A compositional Translation of Stochastic Automata into Timed Automata. Technical report at CTIT, University of Twente number TR-CTIT-00-08, 2000.
1999
	Thomas Noll, Heiko Vogler. On the Universality of Higher-Order Attributed Tree Transducers. Technical report at Dresden University of Technology number TUD-FI 99/05, 1999.
1992
	Thomas Noll, Heiko Vogler. Top-Down Parsing with Simultaneous Evaluation of Noncircular Attribute Grammars. Technical report at RWTH Aachen University number 1992-14, 1992.

BSc/MSc/Diploma Topics
Teaching WS 2012/13
Hybrid Systems Group

We are looking for a HiWi for the Compiler Construction course. If you are interested, please contact Thomas Noll.

Joost-Pieter Katoen has been appointed as a member of the renowned Academia Europaea (Academy of Europe), a European, non-governmental association acting as an Academy whose members are scientists and scholars who collectively aim to promote learning, education and research.

Vacancies for postdoctoral researchers in "Automated Analysis of Probabilistic Programs". Application deadline: August 15, 2013.

Joost-Pieter Katoen has been awarded a Distinguished Professorship from the RWTH Aachen University.

The Hybrid Systems: Computation and Control (HSCC'13) conference in Philadelphia has been very successful: Hongfei Fu received the best student paper award for his paper "Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata". Besides, the paper by Ilya Tkachev, Alexandru Mereacre, Alessandro Abate and Joost-Pieter Katoen was ranked second in the overall best paper award selection.

Joost-Pieter Katoen has been elected as Steering Committee Chair of ETAPS (www.etaps.org), the largest conference on theory and practice of software in Europe. He is the first non-UK ETAPS SC chair since the conference was initiated in 1998. More information here.

The Alumni-Magazine of RWTH Aachen University contains an interview with our former PhD student and postdoctoral researcher, Dr. Tingting Han.

HiWi's wanted to work in a new European Space Agency project for enhancing state-of-the-art design and analysis tools (COMPASS) for the next generation European rockets. Need programming and model checking affinity. See here for details and contact.

We offer openings for several PhD candidates in the area of
"Model-Based Design and Analysis for Dependable Software Systems". Deadline for application: September 14, 2012. For further information click here.

The Theory of Hybrid Systems Group offers two jobs as student assistants within the CEBug project. For more information, look here.

Dino Distefano received the prestigious Roger Needham Award for his work on software verification. This award is for a distinguished research contribution in computer science by a UK based researcher who has completed up to 10 years of post-doctoral research. Dr. Distefano was the first PhD student supervised by Joost-Pieter Katoen.

Marijn Jongerden received the German MMB (Messung, Modellierung und Bewertung von Rechensystemen) Award 2012 of the GI/ITG-Committee for Measurement, Modelling and Evaluation of Computing Systems for his PhD-thesis on "Model-based energy analysis of battery powered systems". His work was supervised by Boudewijn Haverkort (Twente) and Joost-Pieter Katoen.

Our paper "Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite" has been accepted to ICSE 2012 in the track SE in Practice (18% acceptance rate). The paper treats a new satellite from the European Space Agency that was modeled and analyzed with modern tools during the actual satellite design.

Joost-Pieter Katoen will act as DJ in the "Nacht der Professoren" in the Apollo bar and cinema.