Publications

Publications

2017

[bibtex]
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Motion Planning under Partial Observability using Game-Based Abstraction. Proc. of CDC, IEEE, 2017.

[bibtex]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques. IEEE Transactions on Industrial Informatics, 2017.
Download
[bibtex]
Joost-Pieter Katoen. Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract). Prof. of ICTAC, Volume of LNCS, pages 1-2, Springer, 2017.
Download
[bibtex]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems. Proc. of SAFECOMP, Volume 10488 of LNCS, pages 3-19, Springer, 2017.
Download
[bibtex]
Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Arne Storjohann. Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms. Proc. of 36th IEEE Symposium on Reliable Distributed Systems (SRDS), IEEE CS (Recipient of Best Paper Award), 2017.
Download
[bibtex]
Joost-Pieter Katoen, Falak Sher. Modal Stochastic Games: Abstraction-Refinement of Probabilistic Automata. Models, Algorithms, Logics and Tools (Festschrift Kim Larsen), Volume 10460 of LNCS, pages 426-448, Springer, 2017.
Link
[bibtex]
Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker. Proc. of CAV, Volume 10427 of LNCS, pages 592–600, Springer, 2017.
Link
[bibtex]
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives. Proc. of CAV, Volume 10426 of LNCS, pages 140–159, Springer, 2017.
DOI
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Proc. of the 32nd Annual Symposium on Logic in Computer Science (LICS 2017), pages 1-12, IEEE, 2017.
Link
[bibtex]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs. Proc. of TACAS, Volume 10206 of LNCS, pages 133-150, Springer, 2017.
Download
[bibtex]
Carlos E. Budde, Christian Dehnert, E. Moritz Hahn, Arnd Hartmanns, Sebastian Junges, Andrea Turrini. “JANI: Quantitative Model and Tool Interaction. Proc. of TACAS, Volume 10206 of LNCS, pages 151-168, Springer, 2017.
Link
[bibtex]
Hannah Arndt, Christina Jansen, Christoph Matheja, Thomas Noll. Heap Abstraction Beyond Context-Freeness. Technical report at arxiv number 1705.03754, 2017.
DOI
[bibtex]
Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. Satisfiability Checking and Symbolic Computation. ACM Commun. Comput. Algebra 50(4), pages 145–147, 2017.
Download
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations. Collected Abstracts of the 2nd Workshop on Probabilistic Programming Semantics (PPS 2017), 2017.
Download
[bibtex]
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate. Quantitative Model Checking of Controlled Discrete-Time Markov Processes. Information and Computation 253, pages 1-35, 2017.
DOI
[bibtex]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Marielle Stoelinga. Fault Trees on a Diet: Automated Reduction by Graph Rewriting. Formal Aspects of Computing 29(4), pages 651-703, 2017.
DOI
[bibtex]
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger. Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic. Proc. ESOP 2017, Volume 10201 of LNCS, pages 611–638, Springer, 2017.
DOI
[bibtex]
Louis Wachtmeister, Thomas Noll. Analysing Cryptographically-Masked Information Flows in MILS-AADL Specifications. Proc. Int. Workshop on MILS: Architecture and Assurance for Secure Systems, Zenodo, 2017.

[bibtex]
Stefan Schupp, Erika Abraham, Ibtissem Ben Makhlouf, Stefan Kowalewski. HyPro: A C++ Library for State Set Representations for Hybrid Systems Reachability Analysis. Proc. of the 9th NASA Formal Methods Symposium (NFM'17), Volume 10227 of LNCS, pages 288–294, Springer International Publishing, 2017.
Download
[bibtex]
Stefan Schupp, Johanna Nellen, Erika Abraham. Divide and Conquer: Variable Set Separation in Hybrid Systems Reachability Analysis. Proc. of the 15th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL'17), Volume 250 of EPTCS, pages 1–14, Open Publishing Association, 2017.

[bibtex]
Sascha Müller, Andreas Gerndt, Thomas Noll. Synthesizing FDIR Recovery Strategies from Non-Deterministic Dynamic Fault Trees. 2017 AIAA SPACE Forum, to be published, 2017.

[bibtex]
Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. The COMPASS 3.0 Toolset (short paper). Proc. 5th Int. Symp. on Model-Based Safety and Assessment (IMBSA 2017), to be published, 2017.
DOI
[bibtex]
Marco Bozzano, Harold Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. Formal Methods for Aerospace Systems: Achievements and Challenges. In Shin Nakajima, Jean-Pierre Talpin, Masumi Toyoshima, Huafeng Yu editors, Cyber-Physical System Design from an Architecture Analysis Viewpoint: Communications of NII Shonan Meetings, Springer Singapore, 2017.
Download
[bibtex]
Erika Abraham. Techniques and Tools for Hybrid Systems Reachability Analysis. Proc. Numerical Software Verification (NSV'17), , 2017.
Download
[bibtex]
Tarik Viehmann, Gereon Kremer, Erika Abraham. Comparing Different Projection Operators in the Cylindrical Algebraic Decomposition for SMT Solving. Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, Volume of CEUR-WS, , 2017.

[bibtex]
Erika Abraham, Jasper Nalbach, Gereon Kremer. Embedding the Virtual Substitution Method in the Model Constructing Satisfiability Calculus Framework. Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation, CEUR-WS, 2017.

[bibtex]
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle McIver. Conditioning in Probabilistic Programming. In , ACM Transactions on Programming Languages and Systems (TOPLAS), [to appear], 2017.
DOI
[bibtex]
Erika Abraham, Hadas Kress-Gazit, Lorenzo Natale, Armando Tacchella editors. Computer-Assisted Engineering for Robotics and Autonomous Systems (Dagstuhl Seminar 17071). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, Volume 7/2 of Dagstuhl Reports, pages 48–63, 2017.
2016
Download
[bibtex]
Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga. Confluence Reduction for Markov Automata. Theoretical Computer Science 655(Part B), pages 193–219, 2016.
Download
[bibtex]
Joost-Pieter Katoen, Hao Wu. Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow. ACM Transactions on Embedded Computing Systems 22(1), pages 28, 2016.
Download
[bibtex]
Johanna Nellen. Analysis and Synthesis of Hybrid Systems in Control Engineering. Phd Thesis at RWTH Aachen University, 2016.
DOI
[bibtex]
Erika Abraham, Thi Mai Thuong Tran, Martin Steffen. Observable Interface Behavior and Inheritance. Mathematical Structures in Computer Science 26(3), pages 561–605, 2016.
Download
[bibtex]
Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs. Proc. of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, Springer, 2016.
DOI
[bibtex]
Johanna Nellen, Kai Driessen, Martin R. Neuhäußer, Erika Abraham, Benedikt Wolters. Two CEGAR-Based Approaches for the Safety Verification of PLC-Controlled Plants. Information Systems Frontiers 18(5), pages 927–952, 2016.
DOI
[bibtex]
Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. Proc. of ATVA, Volume 9938 of LNCS, pages 50–67, Springer, 2016.
Download
[bibtex]
Victor Bos, Harold Bruintjes, Stefano Tonetta. Catalogue of System and Software Properties. Proc. of the 35th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP), Volume 9922 of LNCS, pages 88–101, Springer, 2016.
Link
[bibtex]
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models. Proc. of Cross-Disciplinary Challenges for Autonomous Systems (CDCAS), Volume of AAAI Technical Reports, AAAI Press, 2016.
Link
[bibtex]
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.
DOI
[bibtex]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis. Proc. of the 35th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP), Volume 9922 of LNCS, pages 253–265, Springer, 2016.
Download
[bibtex]
Gereon Kremer, Florian Corzilius, Erika Abraham. A Generalised Branch-and-Bound Approach and its Application in SAT Modulo Nonlinear Integer Arithmetic. 18th International Workshop on Computer Algebra in Scientific Computing (CASC'16), Volume 9890 of LNCS, pages 315-335, Springer, 2016.
Download
[bibtex]
Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, James Gross. Model-Checking Assisted Protocol Design for Ultra-Reliable Low-Latency Wireless Networks. Proc. of the 35th Symp. on Reliable Distributed Systems (SRDS), pages 307–316, IEEE CS, 2016.
Download
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs. Proc. of the 13th International Conference on Quantitative Evaluation of SysTems (QEST 2016), Volume 9826 of LNCS, pages 191-206, Springer, 2016.
DOI
[bibtex]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga. Uncovering Dynamic Fault Trees. Proc. of IEEE/IFIP Symposium on Dependable Systems and Networks (DSN), pages 299-310, IEEE CS, 2016.
Download
[bibtex]
Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs. Proc. of the 31st Annual Symposium on Logic in Computer Science (LICS 2016), pages 672-681, ACM, 2016.
Download
[bibtex]
Joost-Pieter Katoen. The Probabilistic Model Checking Landscape. Proc. of Logic in Computer Science (LICS), pages 31-46, ACM, 2016.
DOI
[bibtex]
Mohamed Amin Ben Sassi, Sriram Sankaranarayanan, Xin Chen, Erika Abraham. Linear Relaxations of Polynomial Positivity for Polynomial Lyapunov Function Synthesis. IMA Journal of Mathematical Control and Information 33(3), pages 723–756, 2016.
DOI
[bibtex]
Sebastian Junges, Nils Jansen, Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs. Proc. of TACAS, Volume 9636 of LNCS, pages 130-146, Springer, 2016.
DOI
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs (EATCS Best Paper Award). Proc. of the 25th European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, pages 364 - 389, Springer, 2016.

[bibtex]
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo. On the Semantic Intricacies of Conditioning. Collected Abstracts of the 1st Workshop on Probabilistic Programming Semantics (PPS 2016), 2016.
Download
[bibtex]
Anton J. Wijs, Joost-Pieter Katoen, Dragan Bosnacki. Efficient GPU Algorithms for Parallel Decomposition of Graphs into Strongly Connected and Maximal End Components. Formal Methods in System Design 48(3), pages 274-300, 2016.
DOI
[bibtex]
Erika Abraham, Marcello M. Bonsangue, Einar Broch Johnsen editors. Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Springer International Publishing, Volume 9660 of LNCS, 2016.
DOI
[bibtex]
Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Joost-Pieter Katoen, Erika Abraham, Harold Bruintjes. Parameter Synthesis for Probabilistic Systems. Proc. of the 19th GI/ITG/GMM Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'16), pages 72-74, Albert-Ludwigs-Universität Freiburg, 2016.
DOI
[bibtex]
Erika Abraham, Pascal Fontaine, Thomas Sturm, Dongming Wang. Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). Dagstuhl Reports 5(11), pages 71–89, 2016.
Download
[bibtex]
Souymodip Chakraborty, Joost-Pieter Katoen. On the Satisfiability of Some Simple Probabilistic Logics. Proc. of Logic in Computer Science (LICS), pages 56-66, ACM, 2016.
DOI
[bibtex]
Erika Abraham, Marieke Huisman editors. Proceedings of the 12th International Conference on Integrated Formal Methods (iFM'16). Springer International Publishing, Volume 9681 of LNCS, 2016.

[bibtex]
Erika Abraham, Sergiy Bogomolov editors. Proceedings of the 2016 International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR'16). IEEE, 2016.
DOI
[bibtex]
Erika Abraham, Gereon Kremer. Satisfiability Checking: Theory and Applications. Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM'16), Volume 9763 of LNCS, pages 9–23, Springer International Publishing, 2016.

[bibtex]
Luca Aceto, Tom Henzinger, Joost-Pieter Katoen, Wolfgang Thomas, Moshe Vardi. Viewpoints on "Logic activities in Europe", twenty years later. Bulletin of the EATCS 118, 2016.

[bibtex]
Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. Satisfiability Checking and Symbolic Computation. CoRR (Proc. of the 41th Int. Symposium on Symbolic and Algebraic Computation, ISSAC'16) abs/1607.06945, 2016.
DOI
[bibtex]
Erika Abraham, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm. SC$^ 2$: Satisfiability Checking meets Symbolic Computation. Proc. of the 9th Conf. on Intelligent Computer Mathematics (CICM'16), Volume 9791 of LNCS, pages 28-43, , 2016.
DOI
[bibtex]
Erika Abraham, Klaus Havelund. Some Recent Advances in Automated Analysis. Software Tools for Technology Transfer 18(2), pages 121–128, 2016.
Download
[bibtex]
Hao Wu, Xiaoxiao Yang, Joost-Pieter Katoen. Performance Evaluation of Concurrent Data Structures. Prof. of Dependable Software Engineering: Theories, Tools, and Applications (SETTA), Volume 9984 of LNCS, pages 38–49, Springer, 2016.

[bibtex]
Florian Corzilius. Integrating Virtual Substitution into Strategic SMT Solving. Phd Thesis at RWTH Aachen University, 2016.

[bibtex]
Pascal Richter, David Laukamp, Levin Gerdes, Martin Frank, Erika Abraham. Heliostat Field Layout Optimization with Evolutionary Algorithms. Proc. of the 2nd Global Conference on Artificial Intelligence (GCAI'16), Volume 41 of EPiC Series in Computing, pages 240–252, EasyChair, 2016.
DOI
[bibtex]
Francesco Leofante, Simone Vuotto, Erika Abraham, Armando Tacchella, Nils Jansen. Combining Static and Runtime Methods to Achieve Safe Standing-Up for Humanoid Robots. Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, Part I, Volume 9952 of LNCS, pages 496-514, Springer International Publishing, 2016.
Download
[bibtex]
Erika Abraham, Florian Corzilius, Einar Broch Johnsen, Gereon Kremer, Jacopo Mauro. Zephyrus2: On the Fly Deployment Optimization Using SMT and CP Technologies. Dependable Software Engineering: Theories, Tools, and Applications (SETTA'16), Volume 9984 of LNCS, pages 229–245, Springer, 2016.

[bibtex]
Erika Abraham. Symbolic Computation Techniques in Satisfiability Checking. Proc. of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC'16), pages 3–10, IEEE Computer Society, 2016.
DOI
[bibtex]
Francesco Leofante, Armando Tacchella. Learning in Physical Domains: Mating Safety Requirements and Costly Sampling. AI*IA 2016: Advances in Artificial Intelligence - XVth International Conference of the Italian Association for Artificial Intelligence, Genova, Italy, November 29 - December 1, 2016, Proceedings, Volume 10037 of LNCS, pages 539–552, Springer, 2016.

[bibtex]
Francesco Leofante, Luca Pulina, Armando Tacchella. Learning with Safety Requirements: State of the Art and Open Questions. Proceedings of the 23rd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2016 (RCRA 2016) A workshop of the XV International Conference of the Italian Association for Artificial, Volume 1745 of CEUR Workshop Proceedings, pages 11–25, CEUR-WS.org, 2016.

[bibtex]
Nicolò Arnaldi, Chiara Barone, Franco Fusco, Francesco Leofante, Armando Tacchella. Autonomous Driving and Undergraduates: an Affordable Setup for Teaching Robotics. Proceedings of the 3rd Italian Workshop on Artificial Intelligence and Robotics - A workshop of the XV International Conference of the Italian Association for Artificial Intelligence, AIRO@AI*IA 2016, Genova, Italy, November 28, 2016., Volume 1834 of CEUR Workshop Proceedings, pages 5–9, CEUR-WS.org, 2016.
2015
Download
[bibtex]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Marielle Stoelinga. Fault Trees on a Diet. 1st Symp. on Dependable Software Engineering: Theories, Tools and Applications (SETTA), Volume 9409 of LNCS, pages 3–18, Springer, 2015.
Download
[bibtex]
Joost-Pieter Katoen. Probabilistic Programming: A True Challenge in Verification. 13th Int. Symp. on Automated Technology for Verification and Analysis (ATVA), Volume of LNCS, pages 1–3, Springer-Verlag, 2015.
DOI
[bibtex]
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Juggrnaut: Using Graph Grammars for Abstracting Unbounded Heap Structures. Formal Methods in System Design 47(2), pages 159–203, 2015.
Download
[bibtex]
Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Probabilistic Programs - A Natural Model for Approximate Computations. Workshop on Approximate Computing (AC15), 2015.
Download
[bibtex]
Martin Fraenzle, Sebastian Gerwinn, Paul Kröger, Alessandro Abate, Joost-Pieter Katoen. Multi-Objective Parameter Synthesis in Probabilistic Hybrid Systems. 13th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Volume 9268 of LNCS, pages 93–107, Springer-Verlag, 2015.
DOI
[bibtex]
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, Erika Abraham. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. Proc. of the 18th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'15), Volume 9340 of LNCS, pages 360–368, Springer, 2015.
DOI
[bibtex]
Sascha Geulen, Martina Josevski, Johanna Nellen, Janosch Fuchs, Lukas Netz, Benedikt Wolters, Dirk Abel, Erika Abraham, Walter Unger. Learning-based Control Strategies for Hybrid Electric Vehicles. Proc. of the 2015 IEEE Conf. on Control Applications (CCA'15), pages 1722–1728, IEEE, 2015.
DOI
[bibtex]
Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo. Understanding Probabilistic Programs. Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Volume 9360 of LNCS, pages 15-32, Springer, 2015.
Download
[bibtex]
Souymodip Chakraborty, Joost-Pieter Katoen. P-Automata for Markov Decision Processes. 3rd Workshop on Strategic Reasoning, pages 10, University of Oxford, 2015.
Download
[bibtex]
Friedrich Gretz. Semantics and Loop Invariant Synthesis for Probabilistic Programs. Phd Thesis at RWTH Aachen University, 2015.
Download
[bibtex]
Benjamin Lucien Kaminski, Joost-Pieter Katoen. On the Hardness of Almost-Sure Termination. Proc. of the 40th International Symposium on Mathematical Foundations of Computer Science (MFCS 2015), Part I, Volume 9234 of LNCS, pages 307-318, Springer, 2015.
Download
[bibtex]
Souymodip Chakraborty, Joost-Pieter Katoen, Falak Sher, Martin Strelec. Modelling and Statistical Model Checking of a Microgrid. Software Tools for Technology Transfer 17(4), pages 537–554, 2015.
Download
[bibtex]
Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Bruintjes, Joost-Pieter Katoen, Erika Abraham. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool. Proc. of the 27th Int. Conf. on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, pages 214–231, Springer, 2015.
Download
[bibtex]
Tim Quatmann, Nils Jansen, Christian Dehnert, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards. Proc. of the 20th Int. Symp. on Formal Methods (FM'15), Volume 9109 of LNCS, pages 435–452, Springer, 2015.
Download
[bibtex]
Souymodip Chakraborty, Joost-Pieter Katoen. Model Checking of Open Interval Markov Chains. Analytical and Stochastic Modelling Techniques and Applications (ASMTA), Volume 9081 of LNCS, pages 30–42, , 2015.

[bibtex]
Sascha Geulen, Martina Josevski, Johanna Nellen, Janosch Fuchs, Lukas Netz, Benedikt Wolters, Erika Abraham, Walter Unger, Dirk Abel. Online Lernen als Kontrollstrategie in Hybridfahrzeugen. Proc. of the 7th VDI/VDE Fachtagung AUTOREG: Auf dem Weg zum automatisierten Fahren, Volume 2233 of VDI-Berichte, pages 101–112, VDI Verlag, 2015.
Link
[bibtex]
Erika Abraham. Building Bridges between Symbolic Computation and Satisfiability Checking. Proc. of the 2015 ACM on Int. Symp. on Symbolic and Algebraic Computation (ISSAC'15), pages 1–6, ACM, 2015.
Link
[bibtex]
Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic. Technical report at RWTH Aachen University number AIB-2015-12, 2015.
Link
[bibtex]
Shashank Pathak, Erika Abraham, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models. Proc. of the 7th NASA Formal Methods Symp. (NFM'15), Volume 9058 of LNCS, pages 295–309, Springer, 2015.
Download
[bibtex]
Falak Sher. Abstraction and Refinement of Probabilistic Automata using Modal Stochastic Games. Phd Thesis at RWTH Aachen University, 2015.
Link
[bibtex]
Daniela Lepri, Erika Abraham, Peter Csaba Ölveczky. Sound and Complete Timed CTL Model Checking of Timed Kripke Structures and Real-Time Rewrite Theories. Science of Computer Programming 99, pages 128–192, 2015.
Link
[bibtex]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude: What Happened at the 2010 Sauna World Championships?. Science of Computer Programming 99, pages 95–127, 2015.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata. Logical Methods in Computer Science (LMCS) 11(1:15), pages 1–23, 2015.
Download
[bibtex]
Nils Jansen. Counterexamples in Probabilistic Verification. Phd Thesis at RWTH Aachen University, 2015.
Link
[bibtex]
Xin Chen. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Phd Thesis at RWTH Aachen University, 2015.
Download
[bibtex]
Benjamin Lucien Kaminski. Analyzing Expected Outcomes and (Positive) Almost-Sure Termination of Probabilistic Programs is Hard. Proc. of the Young Researchers' Conference "Frontiers of Formal Methods" (FFM 2015), pages 179-184, Aachener Informatik Berichte, 2015.

[bibtex]
Christina Jansen. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs. Proceedings of the Young Researchers’ Conference “Frontiers of Formal Methods”, Volume of Aachener Informatik Berichte, pages 145-150, RWTH Aachen, 2015.
Download
[bibtex]
Arpit Sharma. Reduction Techniques for Nondeterministic and Probabilistic Systems. Phd Thesis at RWTH Aachen University, 2015.
DOI
[bibtex]
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying Pointer Programs using Graph Grammars. Science of Computer Programming 97, pages 157–162, 2015.
DOI
[bibtex]
Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, Thomas Noll. Compositional Analysis Using Component-Oriented Interpolation. Proceedings Formal Aspects of Component Software (FACS 2014), Volume 8997 of LNCS, pages 68–85, Springer, 2015.
DOI
[bibtex]
Thomas Noll. Safety, Dependability and Performance Analysis of Aerospace Systems. Proc. 3rd Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), Volume 476 of CCIS, pages 17–31, Springer, 2015.
DOI
[bibtex]
Kevin van der Pol, Thomas Noll. Security Type Checking for MILS-AADL Specifications. International Workshop on MILS: Architecture and Assurance for Secure Systems, Zenodo, 2015.
Link
[bibtex]
Xin Chen, Stefan Schupp, Ibtissem Ben Makhlouf, Erika Abraham, Goran Frehse, Stefan Kowalewski. A Benchmark Suite for Hybrid Systems Reachability Analysis. Proc. of the 7th NASA Formal Methods Symp. (NFM'15), Volume 9058 of LNCS, pages 408–414, Springer, 2015.
Link
[bibtex]
Johanna Nellen, Erika Abraham, Benedikt Wolters. A CEGAR Tool for the Reachability Analysis of PLC-Controlled Plants using Hybrid Automata. In Thouraya Bouabana-Tebibel, Stuart H. Rubin editors, Formalisms for Reuse and Systems Integration, pages 55–78, Volume 346 of Advances in Intelligent Systems and Computing, 2015.
Download
[bibtex]
Harold Bruintjes, Joost-Pieter Katoen, David Lesens. A statistical approach for timed reachability in AADL models. Dependable Systems and Networks (DSN), pages 81–88, IEEE CS Press, 2015.
Download
[bibtex]
Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver. Conditioning in Probabilistic Programming. Proc. of the 31st Conference on the Mathematical Foundations of Programming Semantics (MFPS 2015), ENTCS 319, pages 199-216, 2015.
Download
[bibtex]
Tim Lange, Martin R. Neuhäußer, Thomas Noll. IC3 Software Model Checking on Control Flow Automata. Formal Methods in Computer-Aided Design (FMCAD 2015), pages 97–104, IEEE, 2015.
Link
[bibtex]
Johanna Nellen, Benedikt Wolters, Lukas Netz, Sascha Geulen, Erika Abraham. A Genetic Algorithm based Control Strategy for the Energy Management Problem in PHEVs. Proc. of the 1st Global Conference on Artificial Intelligence (GCAI'15), Volume 36 of EPiC Series in Computer Science, pages 196–214, EasyChair, 2015.
DOI
[bibtex]
Christoph Matheja, Christina Jansen, Thomas Noll. Tree-Like Grammars and Separation Logic. Programming Languages and Systems (APLAS 2015), Volume 9458 of LNCS, pages 90–108, Springer, 2015.
Download
[bibtex]
Stefan Schupp, Erika Abraham, Xin Chen, Ibtissem Ben Makhlouf, Goran Frehse, Sriram Sankaranarayanan, Stefan Kowalewski. Current Challenges in the Verification of Hybrid Systems. Proc. of the 5th Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems (CyPhy’15), Volume 9361 of Information Systems and Applications, incl. Internet/Web, and HCI, pages 8–24, Springer, 2015.

[bibtex]
Erika Abraham, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit. Challenges and Recommendations for Preparing HPC Applications for Exascale. CoRR abs/1503.06974, 2015.

[bibtex]
Erika Abraham, Costas Bekas, Ivona Brandic, Samir Genaim, Einar Broch Johnsen, Ivan Kondov, Sabri Pllana, Achim Streit. Preparing HPC Applications for Exascale: Challenges and Recommendations. Proc. of the 18th International Conference on Network-Based Information Systems (NbIS'15), pages 401-406, IEEE, 2015.

[bibtex]
Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Flow* 1.2: More Effective to Play with Hybrid Systems. Proceedings of the 1st and 2nd Int. Workshop on Applied veRification for Continuous and Hybrid Systems (ARCH'15), Volume 34 of EasyChair Proceedings in Computing, pages 152–159, EasyChair, 2015.
Download
[bibtex]
Jonathan Heinen. Verifying Java Programs: A Graph Grammar Approach. Phd Thesis at RWTH Aachen University, 2015.
2014
DOI
[bibtex]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Panagiotis Katsaros, Konstantinos Mokos, Viet Yen Nguyen, Thomas Noll, Bart Postma, Marco Roveri. Spacecraft Early Design Validation using Formal Methods. Reliability Engineering and System Safety 132, pages 20–35, 2014.
Link
[bibtex]
Hongfei Fu. Verifying Probabilistic Systems: New Algorithms and Complexity Results. Phd Thesis at RWTH Aachen University, 2014.
DOI
[bibtex]
Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, Thomas Noll. A Review of Statistical Model Checking Pitfalls on Real-Time Stochastic Models. Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, Volume 8803 of LNCS, pages 177–192, Springer, 2014.
Download
[bibtex]
Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer. Analysis of Timed and Long-Run Objectives in Markov Automata. Logical Methods in Computer Science 10(3), 2014.
Download
[bibtex]
Joost-Pieter Katoen. Model Checking Gigantic Markov Models. 12th International Conference on Software Engineering and Formal Methods (SEFM), Volume 8702 of LNCS, pages 1–2, , 2014.
Download
[bibtex]
Souymodip Chakraborty, Joost-Pieter Katoen. Parametric LTL on Markov Chains. IFIP Conference on Theoretical Computer Science, Volume 8705 of LNCS, pages 207–222, , 2014.
Download
[bibtex]
Arpit Sharma, Joost-Pieter Katoen. Layered Reduction for Abstract Probabilistic Automata . 14th International Conference on Application of Concurrency to System Design (ACSD), ISBN 978-1-4799-4281-7, pages 21–31, IEEE, ISBN 978-1-4799-4281-7, 2014.
Download
[bibtex]
Erika Abraham, Bernd Becker, Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer. Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey. Proc. of the 14th Int. School on Formal Methods for the Design of Computer, Communication and Software Systems: Executable Software Models (SFM-14:ESM), Volume 8483 of LNCS, pages 65–121, Springer, 2014.
Link
[bibtex]
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.
Download
[bibtex]
Hongfei Fu. Maximal Cost-Bounded Reachability Probability on Continuous-Time Markov Decision Processes. FoSSaCS, Volume 8412 of LNCS, pages 73–87, Springer, 2014.
Download
[bibtex]
Nils Jansen, Ralf Wimmer, Erika Abraham, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster. Symbolic Counterexample Generation for Large Discrete-Time Markov Chains. Science of Computer Programming 91 (Part A), pages 90–114, 2014.
Download
[bibtex]
Federico Olmedo. Approximate Relational Reasoning for Probabilistic Programs. Phd Thesis at Technical University of Madrid, 2014.
Download
[bibtex]
Arpit Sharma, Joost-Pieter Katoen. Layered Reduction for Modal Specification Theories. Formal Aspects of Component Software (FACS 2013), 10th International Symposium (FACS), Revised Selected Papers, Volume 8348 of LNCS, pages 1–19, Springer, 2014.
Download
[bibtex]
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. Operational versus Weakest Pre-expectation Semantics for the Probabilistic Guarded Command Language. Performance Evaluation 73, pages 110–132, 2014.
Download
[bibtex]
Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga, Ted Luiten, Judi Romijn. Smart Railroad Maintenance Engineering with Stochastic Model Checking. 2nd Int. Conf. on Railway Technology: Research, Development and Maintenance (Railways 2014), pages 1–16, Saxe-Coburg Publications, 2014.
DOI
[bibtex]
Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Performance Analysis of Computing Servers – a case study exploiting a new GSPN semantics. Measurement, Modelling and Evaluation of Computing Systems and Dependability and Fault-Tolerance (MMB & DFT 2014), Volume 8376 of LNCS, pages 57–72, Springer, 2014.
Download
[bibtex]
Joost-Pieter Katoen, Lei Song, Lijun Zhang. Probably Safe or Live. Computer Science Logic and Logic in Computer Science (CSL-LICS), ACM, 2014.
Download
[bibtex]
Tomas Brazdil, Stefan Kiefer, Antonín Kucera, Petr Novotny, Joost-Pieter Katoen. Zero-Reachability in Probabilistic Multi-Counter Automata. Computer Science Logic and Logic in Computer Science (CSL-LICS), ACM, 2014.
DOI
[bibtex]
Erika Abraham, Klaus Havelund editors. Proc. of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '14). Springer, Volume 8413 of LNCS, 2014.
Link
[bibtex]
Erika Abraham, Alberto Avritzer, Anne Remke, William H. Sanders editors. Randomized Timed and Hybrid Models for Critical Infrastructures (Dagstuhl Seminar 14031). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Volume 4 of Dagstuhl Reports, 2014.
Download
[bibtex]
Anton J. Wijs, Joost-Pieter Katoen, Dragan Bosnacki. GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components. Computer-Aided Verification (CAV), Volume 8559 of LNCS, pages 309–325, , 2014.
Download
[bibtex]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification. 11th Int. Conf. on Quantitative Evaluation of Systems (QEST'14), Volume 8657 of LNCS, pages 404–420, Springer, 2014.
DOI
[bibtex]
Christina Jansen, Thomas Noll. Generating Abstract Graph-Based Procedure Summaries for Pointer Programs. Proc. 7th Int. Conf. on Graph Transformation (ICGT 2014), Volume 8571 of LNCS, pages 49–64, Springer, 2014.
DOI
[bibtex]
Christina Jansen, Florian Göbe, Thomas Noll. Generating Inductive Predicates for Symbolic Execution of Pointer-Manipulating Programs. Proc. 7th Int. Conf. on Graph Transformation (ICGT 2014), Volume 8571 of LNCS, pages 65–80, Springer, 2014.
DOI
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Linear-Time Probabilistic Verification. Theoretical Computer Science 549, pages 61–100, 2014.
Download
[bibtex]
Falak Sher, Joost-Pieter Katoen. Tight Game Abstractions of Probabilistic Automata. Concurrency Theory (CONCUR), Volume 8704 of LNCS, pages 576–592, Springer, 2014.
Download
[bibtex]
Joost-Pieter Katoen, Hao Wu. Exponentially timed SADF: Compositional Semantics, Reduction, and Analysis. Embedded Software (EMSOFT), pages 1–10, ACM Press, 2014.
Download
[bibtex]
Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Abraham, Joost-Pieter Katoen. Fast Debugging of PRISM Models. Int. Symp. on Automated Technology for Verification and Analysis (ATVA'14), Volume 8837 of LNCS, pages 146–162, Springer, 2014.
Link
[bibtex]
Ralf Wimmer, Erika Abraham. Maybe or Maybe Not: Contributions to Stochastic Verification. Aspekte der Technischen Informatik: Festschrift zum 60. Geburtstag von Bernd Becker, Monsenstein und Vannerdat, 2014.
Link
[bibtex]
Pascal Richter, Martin Frank, Erika Abraham. Multi-objective Optimization of Solar Tower Power Plants. Proc. of the 18th European Conference on Mathematics for Industry (ECMI'14), Volume of Mathematics in Industry, Springer, 2014.

[bibtex]
Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Under-approximate Flowpipes for Non-linear Continuous Systems. Proc. of Formal Methods in Computer-Aided Design (FMCAD'14), pages 59–66, IEEE/ACM, 2014.
DOI
[bibtex]
Johanna Nellen, Erika Abraham. A CEGAR Approach for the Reachability Analysis of PLC-Controlled Chemical Plants. Proc. of the 15th Int. Conf. on Information Reuse and Integration (IRI'14), pages 500–507, IEEE Computer Society Press, 2014.
Link
[bibtex]
Johanna Nellen, Erika Abraham, Xin Chen, Pieter Collins. Counterexample Generation for Hybrid Automata. Proc. of the 2nd Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'13), Volume 419 of CCIS, pages 88–106, Springer, 2014.
DOI
[bibtex]
Erika Abraham, Catuscia Palamidessi editors. Proc. of the 34th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE'14), Held as Part of the 9th International Federated Conference on Distributed Computing Techniques, DisCoTec 2014, Berlin. Springer, Volume 8461 of LNCS, 2014.
Link
[bibtex]
Thomas Noll. Safety, Dependability and Performance Analysis of Aerospace Systems. Preliminary proceedings of 3rd Int. Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), pages 2–5, , 2014.

[bibtex]
Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Formal Validation Methods in Model-Based Spacecraft Systems Engineering. In Daniele Gianni, Andrea D'Ambrogio, Andreas Tolk editors, Modeling and Simulation-Based Systems Engineering Handbook, pages 339–375, 2014.
Download
[bibtex]
Christian Dehnert, Daniel Gebler, Michele Volpato, David N. Jansen. On Abstraction of Probabilistic Systems. International Autumn School, ROCKS 2012 (Advanced Lectures), Volume 8453 of LNCS, pages 87–116, Springer, 2014.
2013
Download
[bibtex]
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.
Download
[bibtex]
Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. Probabilistic Relational Reasoning for Differential Privacy. ACM Transactions on Programming Languages and Systems 35(3), 2013.
Link
[bibtex]
Tim Lange, Martin R. Neuhäußer, Thomas Noll. Speeding Up the Safety Verification of Programmable Logic Controller Code. Proc. 9th Haifa Verification Conf. (HVC 2013), Volume 8244 of LNCS, pages 44–60, Springer, 2013.
Download
[bibtex]
Viet Yen Nguyen. Trustworthy Spacecraft Design Using Formal Methods. Technical report at RWTH Aachen University number , 2013.

[bibtex]
Sriram Sankaranarayanan, Xin Chen, Erika Abraham. Lyapunov Function Synthesis using Handelman Representations. The 9th IFAC Symposium on Nonlinear Control Systems (NOLCOS'13) (invited paper), , 2013.
Download
[bibtex]
Bernhard Ern, Viet Yen Nguyen, Thomas Noll. Characterization of Failure Effects on AADL Models. Proceedings of the 32nd International Conference on Computer Safety, Reliability and Security (SAFECOMP 2013), Volume 8153 of LNCS, pages 241–252, Springer, 2013.
Download
[bibtex]
Sebastian Junges, Ulrich Loup, Florian Corzilius, Erika Abraham. On Gröbner Bases in the Context of Satisfiability-Modulo-Theories Solving over the Real Numbers. Proc. of the 5th International Conference on Algebraic Informatics (CAI'13), Volume 8080 of LNCS, pages 186–198, Springer-Verlag, 2013.
Download
[bibtex]
Viet Yen Nguyen, Theo C. Ruys. Selected Dynamic Issues in Software Model Checking. International Journal on Software Tools for Technology Transfer (STTT) 15(4), 2013.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata. Proc. of the 10th Int. Conf. on Quantitative Evaluation of Systems (QEST'13), Volume 8054 of LNCS, pages 39–54, Springer-Verlag, 2013.
Download
[bibtex]
Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer. Modelling, Reduction and Analysis of Markov Automata. 10th Int. Conf. on Quantitative Evaluation of Systems (QEST'13), Volume 8054 of LNCS, pages 34–50, Springer, 2013.
Download
[bibtex]
Joost-Pieter Katoen. Concurrency meets Probability: Theory and Practice (Abstract). Int. Conf. on Concurrency Theory (CONCUR), Volume 8052 of LNCS, pages 44–45, , 2013.
Link
[bibtex]
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.
Download
[bibtex]
Souymodip Chakraborty, Joost-Pieter Katoen. Parametric LTL on Markov Chains. TCS , pages 207–221, , 2013.
Link
[bibtex]
Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, Lijun Zhang. A Semantics for Every GSPN. Int. Conf. on Application and Theory of Petri Nets and Concurrency (ICATPN), Volume 7927 of LNCS, pages 90–109, Springer, 2013.
DOI
[bibtex]
Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Fabio Somenzi, Erika Abraham. From Statistical Model Checking to Statistical Model Inference: Characterizing the Effect of Process Variations in Analog Circuits. Proc. of the 2013 IEEE/ACM International Conference on Computer-Aided Design (ICCAD'13), pages 662–669, IEEE, 2013.
Download
[bibtex]
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.
Download
[bibtex]
Daniel Neider, Nils Jansen. Regular Model Checking Using Solver Technologies and Automata Learning. 5th NASA Formal Methods Symposium (NFM'13), Volume 7871 of LNCS, pages 16–31, Springer Berlin Heidelberg, 2013.
Download
[bibtex]
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.
Link
[bibtex]
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate. Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems. Hybrid Systems: Computation and Control (HSCC), pages 293–303, ACM, 2013.
Link
[bibtex]
Hongfei Fu. Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. Hybrid Systems: Computation and Control (HSCC), pages 323–332, ACM, 2013.
Link
[bibtex]
Haidi Yue. Analyzing Energy Consumption of Wireless Networks: A Model-based Approach. Phd Thesis at RWTH Aachen University, 2013.
Link
[bibtex]
Joost-Pieter Katoen, Doron Peled. Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems. European Symposium on Programming (ESOP), Volume 7792 of LNCS, pages 411–430, Springer, 2013.
Download
[bibtex]
Christel Baier, E. Moritz Hahn, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Model Checking for Performability. Mathematical Structures in Computer Science 23(4), pages 751–795, 2013.
Download
[bibtex]
E. Moritz Hahn, Arnd Hartmanns, Holger Hermanns, Joost-Pieter Katoen. A Compositional Modeling and Analysis Framework for Stochastic Hybrid Systems. Formal Methods in System Design 43(2), pages 191–232, 2013.
Download
[bibtex]
Christian Dehnert, David Parker, Joost-Pieter Katoen. SMT-based Bisimulation Minimisation of Markov Models. 14th International Conference on Verification, Model Checking, and Abstract Interpretation, Volume 7737 of LNCS, pages 28–47, Springer, 2013.
Link
[bibtex]
Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Model-Based Energy Optimization of Automotive Control Systems. Proc. 16th Conf. on Design, Automation & Test in Europe (DATE 2013), pages 761–766, EDA Consortium, 2013.
Download
[bibtex]
Joost-Pieter Katoen. Model Checking Meets Probability: A Gentle Introduction. In , Engineering Dependable Software Systems, pages 177–205, Volume 34 of NATO Science for Peace and Security Series - D, 2013.

[bibtex]
Yan Zhang, Xin Chen, Sriram Sankaranarayanan, Erika Abraham. Empirical Flowpipe Constructions for Analog Circuits. Workshop on Frontiers in Analog CAD (FAC'13), , 2013.
Download
[bibtex]
Arpit Sharma. A Two Step Perspective for Kripke Structure Reduction. 39th International Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM), Student Research Forum (ISBN 978-80-87136-15-7), , 2013.

[bibtex]
Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Flow*: An Analyzer for Non-Linear Hybrid Systems. Proc. of the 25th Int. Conf. on Computer Aided Verification (CAV'13), Volume 8044 of LNCS, pages 258–263, Springer-Verlag, 2013.
Download
[bibtex]
Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Abraham, Bernd Becker. A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. Proc. of the 24th International Conference on Automated Deduction (CADE-24), Volume 7898 of LNCS, pages 193–207, Springer-Verlag, 2013.

[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Erika Abraham. Stochastic Bounded Model Checking: Bounded Rewards and Compositionality. Proc. of Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'13), pages 243–254, , 2013.
Link
[bibtex]
Markus Bals, Christina Jansen, Thomas Noll. Incremental Construction of Greibach Normal Form for Context-Free Grammars. Proc. Int. Symp. on Theoretical Aspects of Software Engineering (TASE 2013), pages 165–168, IEEE Computer Society, 2013.
Link
[bibtex]
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski. Abstract Probabilistic Automata. Information and Computation 232, pages 66–116, 2013.

[bibtex]
Daniela Lepri, Erika Abraham, Peter Csaba Ölveczky. A Timed CTL Model Checker for Real-Time Maude. Proc. of the 5th Int. Conf. on Algebra and Coalgebra in Computer Science (CALCO'13), Volume 8089 of LNCS, pages 334–339, Springer-Verlag, 2013.
Download
[bibtex]
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. PRINSYS — on a Quest for Probabilistic Loop Invariants. 10th Int. Conf. on Quantitative Evaluation of Systems (QEST'13), Volume 8054 of LNCS, pages 172–187, Springer, 2013.
DOI
[bibtex]
Frédéric Herbreteau, Balaguru Srivathsan. Coarse abstractions make Zeno behaviours difficult to detect. Logical Methods in Computer Science 9(1), 2013.

[bibtex]
Frédéric Herbreteau, Balaguru Srivathsan, Igor Walukiewicz. Lazy abstractions for timed automata. Computer Aided Verification (CAV'13), Volume 8044 of LNCS, pages 990–1005, Springer, 2013.

[bibtex]
Souymodip Chakraborty, Martin Strelec, Joost-Pieter Katoen, Falak Sher. Modelling and Statistical Model Checking of a Microgrid. Workshop on Statistical Model Checking (SMC), Volume of EPTCS, , 2013.
Download
[bibtex]
Sabrina von Styp, Liyong Yu. Symbolic Model-Based Testing for Industrial Automation Software. Haifa Verification Conference, Volume 8244 of Lecture Notes in Computer Science, pages 78–94, Springer, 2013.
Download
[bibtex]
Gilles Barthe, Federico Olmedo. Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs. In , Automata, Languages, and Programming, pages 49–60, Volume 7966 of Lecture Notes in Computer Science, 2013.
Download
[bibtex]
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin. Verified Indifferentiable Hashing into Elliptic Curves. Journal of Computer Security 21(6), pages 881–917, 2013.

[bibtex]
Sabrina von Styp. Symbolic Methods in Testing (Dagstuhl Seminar 13021. Dagstuhl Reports 3(1), 2013.
2012
Download
[bibtex]
Nils Jansen, Erika Abraham, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. The COMICS Tool - Computing Minimal Counterexamples for DTMCs. Proc. of the 10th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'12), Volume 7561 of LNCS, pages 349–353, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. Quantitative Evaluation of Systems (QEST), IEEE CS Press, 2012.
Download
[bibtex]
Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga. Efficient Modelling and Generation of Markov Automata. Concurrency Theory (CONCUR), Volume 7454 of LNCS, pages 364–379, Springer-Verlag, 2012.
Download
[bibtex]
Falak Sher, Joost-Pieter Katoen. Compositional Abstraction Techniques for Probabilistic Automata. IFIP Conference on Theoretical Computer Science (TCS2012), Volume 7604 of LNCS, pages 325–341, Springer-Verlag, 2012.
Download
[bibtex]
Nils Jansen, Erika Abraham, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker. Symbolic Counterexample Generation for Discrete-time Markov Chains. 9th Int. Symp. on Formal Aspects of Component Software (FACS'12), Volume 7684 of LNCS, pages 134–151, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
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.
Download
[bibtex]
Mani Swaminathan, Joost-Pieter Katoen, Ernst-Rüdiger Olderog. Layered Reasoning for Randomized Distributed Algorithms. Formal Aspects of Computing 24(4–6), pages 477–496, 2012.
Download
[bibtex]
Marie-Aude Esteve, Joost-Pieter Katoen, Viet Yen Nguyen, Bart Postma, Yuri Yushtein. Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite. 34th International Conference on Software Engineering (ICSE), pages 1022–1031, ACM and IEEE CS Press, 2012.
Link
[bibtex]
Joost-Pieter Katoen. GSPNs Revisited: Simple Semantics and New Analysis Algorithms. Applications of Concurrency to System Design (ACSD), pages 6–12, IEEE CS Press, 2012.
Download
[bibtex]
Florian Corzilius, Ulrich Loup, Sebastian Junges, Erika Abraham. SMT-RAT: An SMT-Compliant Nonlinear Real Arithmetic Toolbox (Tool Presentation). Int. Conf. on Theory and Applications of Satisfiability Testing (SAT'12), Volume 7317 of LNCS, pages 442–448, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
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.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Bernd Becker, Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models. Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), Volume 7214 of LNCS, pages 299–314, Springer Berlin Heidelberg, 2012.
DOI
[bibtex]
Daniela Lepri, Erika Abraham, Peter Csaba Ölveczky. Timed CTL Model Checking in Real-Time Maude. Proc. of the 9th Int. Workshop on Rewriting Logic and its Applications (WRLA'12), Volume 7571 of LNCS, pages 182–200, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
Dennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer. Quantitative Timed Analysis of Interactive Markov Chains. NASA Formal Methods Symposium (NFM), Volume 7226 of Lecture Notes in Computer Science, pages 8–23, Springer-Verlag, 2012.
DOI
[bibtex]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Formal Modeling and Analysis of Human Body Exposure to Extreme Heat in HI-Maude. Proc. of the 9th Int. Workshop on Rewriting Logic and its Applications (WRLA'12), Volume 7571 of LNCS, pages 139–161, Springer Berlin Heidelberg, 2012.
Download
[bibtex]
Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga, Mark Timmer. A linear process-algebraic format with data for probabilistic automata. Theoretical Computer Science 413, pages 36–57, 2012.
Download
[bibtex]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Three-Valued Abstraction for Probabilistic Systems. Journal on Logic and Algebraic Programming 81(4), pages 356–389, 2012.
Download
[bibtex]
Arpit Sharma, Joost-Pieter Katoen. Weighted Lumpability on Markov Chains. 8th Ershov Informatics Conference (PSI) , Volume 7162 of LNCS, pages 322–339, Springer Verlag, 2012.
Download
[bibtex]
Joost-Pieter Katoen. Model Checking: One Can Do Much More Than You Think!. Fundamentals of Software Engineering (FSEN), Volume 7141 of LNCS, pages 1–14, Springer-Verlag, 2012.

[bibtex]
Etienne Lozes, Florent Jacquemard, Jules Villard, Ralf Treinen. Multiple Congruence Relations, First-Order Theories on Terms, and the Frames of the Applied Pi-Calculus. Theory of Security and Applications (TOSCA 2011), Volume 6993 of LNCS, pages 166–185, , 2012.
Download
[bibtex]
Bart Theelen, Joost-Pieter Katoen, Hao Wu. Model Checking of Scenario-Aware Dataflow with CADP. Design, Automation, and Test in Europe (DATE) , pages 653–658, IEEE CS Press, 2012.
Download
[bibtex]
Ralf Wimmer, Nils Jansen, Erika Abraham, Joost-Pieter Katoen, Bernd Becker. Minimal Critical Subsystems as Counterexamples for omega-Regular DTMC Properties. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'12), pages 169–180, Verlag Dr. Kovac, 2012.
Download
[bibtex]
Johanna Nellen, Erika Abraham. Hybrid Sequential Function Charts. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'12), Volume 68 of Schriftenreihe Forschungsergebnisse zur Informatik, pages 109–120, Verlag Dr. Kova─Ź, 2012.
Download
[bibtex]
Alessandro D'Innocenzo, Alessandro Abate, Joost-Pieter Katoen. Robust PCTL Model Checking. Hybrid Systems: Computation and Control (HSCC), pages 275–286, ACM Press, 2012.
Download
[bibtex]
Arpit Sharma. Weighted Probabilistic Equivalence Preserves omega-Regular Properties. 16th Measurement, Modeling, and Evaluation of Computing Systems and Dependability and Fault Tolerance Conference (MMB/DFT), Volume 7201 of LNCS, pages 121–135, Springer Verlag, 2012.
Link
[bibtex]
Kamal Barakat, Stefan Kowalewski, Thomas Noll. A Native Approach to Modeling Timed Behavior in the Pi-Calculus (short paper). Proc. of 6th IEEE Int. Symp. on Theoretical Aspects of Software Engineering (TASE 2012), pages 253–256, IEEE, 2012.

[bibtex]
Hongfei Fu. Computing Game Metrics on Markov Decision Processes. 39th International Colloquium on Automata, Languages and Programming (ICALP), Volume 7392 of LNCS, pages 227–238, Springer-Verlag, 2012.
Download
[bibtex]
Jonathan Heinen, Christina Jansen, Henrik Barthels. Juggrnaut - An Abstract JVM. 2nd Int. Conf. on Formal Verification of Object-Oriented Software (FoVeOOS 2011), Volume 7421 of LNCS, pages 142–159, Springer, 2012.
Download
[bibtex]
Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Taylor Model Flowpipe Construction for Non-linear Hybrid Systems. Proc. of the 33rd IEEE Real-Time Systems Symposium (RTSS'12), pages 183–192, IEEE Computer Society, 2012.
Link
[bibtex]
Thomas Noll. Correctness, Safety and Fault Tolerance in Aerospace Systems: The ESA COMPASS Project (Abstract). Architecture-Driven Semantic Analysis of Embedded Systems (Dagstuhl Seminar 12272), Volume 2 of Dagstuhl Reports, pages 42, Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2012.

[bibtex]
Frédéric Herbreteau, Balaguru Srivathsan, Igor Walukiewicz. Efficient emptiness check for timed Büchi automata. Formal Methods in System Design 40(2), pages 122–146, 2012.

[bibtex]
Balaguru Srivathsan, Igor Walukiewicz. An alternate proof of Statman's finite completeness theorem. Information Processing Letters 112(14-15), pages 612–616, 2012.

[bibtex]
Frédéric Herbreteau, Balaguru Srivathsan, Igor Walukiewicz. Better abstractions for timed automata. LICS, pages 375 –384, IEEE, 2012.

[bibtex]
Xin Chen, Erika Abraham, Sriram Sankaranarayanan. Taylor Model Over-approximations for Flowpipe/Guard Intersections. 5th Int. Workshop on Numerical Software Verification (NSV'12), , 2012.
Link
[bibtex]
Joost-Pieter Katoen, Viet Yen Nguyen. Ruimtevaartsoftware ideale proeftuin voor formele methoden. Bits en Chips 10, pages 40–41, 2012.

[bibtex]
Dragan Bosnacki, Maximilian R. Odenbrett, Anton J. Wijs, Willem Ligtenberg, Peter Hilbers. Efficient reconstruction of biological networks via transitive reduction on general purpose graphics processors. BMC Bioinformatics 13, pages 281, 2012.
Download
[bibtex]
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin. Verified Indifferentiable Hashing into Elliptic Curves. 1st Conference on Principles of Security and Trust – POST 2012, Volume of Lecture Notes in Computer Science, Springer, 2012.
Download
[bibtex]
Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin. Probabilistic Relational Reasoning for Differential Privacy. 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 97–110, ACM, 2012.
2011
Download
[bibtex]
Erika Abraham, Nadine Bergner, Philipp Brauner, Florian Corzilius, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Johanna Nellen, Ulrik Schroeder. On Collaboratively Conveying Computer Science to Pupils. Proc. of the 11th Koli Calling Int. Conf. on Computing Education Research (KOLI'11), pages 132–137, ACM, 2011.
Download
[bibtex]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. SMA—The Smyle Modeling Approach. Proceedings 3rd IFIP TC2 Central and East European Conference on Software Engineering Techniques (CEE-SET 2008), Volume 4980 of LNCS, pages 103–117, , 2011.
Download
[bibtex]
Nils Jansen, Erika Abraham, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical Counterexamples for Discrete-Time Markov Chains. 9th Int. Symp. on Automated Technology for Verification and Analysis (ATVA'11), Volume 6996 of LNCS, pages 443–452, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Jonathan Heinen, Christina Jansen. Juggrnaut - An Abstract JVM. Formal Verification of Object-Oriented Software. Papers presented at the 2nd International Conference, October 5-7, 2011, Turin, Italy, Volume 2011 of Karlsruhe Reports in Informatics, pages 226–243, Karlsruhe, 2011.
Download
[bibtex]
Jonathan Heinen, Christina Jansen. Juggrnaut - An Abstract JVM. Technical report at RWTH Aachen University, Germany number AIB 2011-21, 2011.
Download
[bibtex]
Xin Chen, Erika Abraham, Goran Frehse. Efficient Bounded Reachability Computation for Rectangular Automata. 5th Workshop on Reachability Problems (RP'11), Volume 6945 of LNCS, pages 139–152, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Observing Continuous-Time MDPs by 1-Clock Timed Automata. Workshop on Reachability Problems (RP), Volume 6945 of LNCS, pages 2–25, Springer-Verlag, 2011.

[bibtex]
Joost-Pieter Katoen, Barbara König editors. 22nd Conference on Concurrency Theory (CONCUR). Springer-Verlag, Volume 6901 of LNCS, 2011.

[bibtex]
Sabrina von Styp, Liyong Yu, Gustavo Quirós. Automatic Test-Case Derivation and Execution in Industrial Control. iATPA 2011: First Workshop on Industrial Automation Tool Integration for Engineering Project Automation, CEUR-WS, 2011.
Download
[bibtex]
Jó Agila Bitsch Link, Christoph Wollgarten, Stefan Schupp, Klaus Wehrle. Perfect Difference Sets for Neighbor Discovery: Energy Efficient and Fair. Proceedings of the 3rd Extreme Conference on Communication: The Amazon Expedition, Volume of ExtremeCom '11, , 2011.
Download
[bibtex]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Adaptive-Step-Size Numerical Methods in Rewriting-Logic-Based Formal Analysis of Interacting Hybrid Systems. Int. Workshop on Harnessing Theories for Tool Support in Software (TTSS'10), Volume 274 of ENTCS, pages 17–32, Elsevier Science Publishers, 2011.
Download
[bibtex]
Yuri Yushtein, Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive, Marco Roveri. System-Software Co-Engineering: Dependability and Safety Perspective. 4th IEEE Int. Conf. on Space Mission Challenges in Information Technology (SMC-IT 2011), pages 18–25, IEEE CS Press, 2011.
Download
[bibtex]
Joost-Pieter Katoen. Towards Trustworthy Aerospace Systems: An Experience Report. 16th International Workshop on Formal Methods for Industrial Critical Systems (FMICS), Volume 6959 of LNCS, pages 1–4, Springer-Verlag, 2011.
Download
[bibtex]
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.
Download
[bibtex]
Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars. 5th Int. Conf. on Language and Automata Theory and Applications (LATA 2011), Volume 6638 of LNCS, pages 323–335, Springer-Verlag, 2011.
Download
[bibtex]
Ulrich Loup, Erika Abraham. I-RiSC: An SMT-Compliant Solver for the Existential Fragment of Real Algebra. 4th Int. Conf. on Algebraic Informatics (CAI'11), Volume 6742 of LNCS, pages 230–246, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. Counterexample Generation for Markov Chains using SMT-based Bounded Model Checking. Formal Techniques for Distributed Systems (FMOODS/FORTE'11), Volume 6722 of LNCS, pages 75–89, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Formal Modeling and Analysis of Hybrid Systems in Rewriting Logic using Higher-Order Numerical Methods and Discrete-Event Detection. Int. Symp. on Computer Science and Software Engineering (CSSE'11), pages 1–8, IEEE, 2011.
Link
[bibtex]
Joost-Pieter Katoen, Thomas Noll. Trustworthy Aerospace Systems. Public Service Review: European Science and Technology 11, pages 204–205, 2011.
Download
[bibtex]
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski. New Results on Abstract Probabilistic Automata. Applications of Concurrency to System Design (ACSD), pages 118–127, IEEE CS Press, 2011.
Download
[bibtex]
Raimondas Sasnauskas, Oscar Soria Dustmann, Benjamin Lucien Kaminski, Klaus Wehrle, Carsten Weise, Stefan Kowalewski. Scalable Symbolic Execution of Distributed Systems. Proc. of the 31st International Conference on Distributed Computing Systems (ICDCS 2011), pages 333-342, IEEE Computer Society, 2011.
Link
[bibtex]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Safety, Dependability, and Performance Analysis of Extended AADL Models. The Computer Journal 54(5), pages 754–775, 2011.
Download
[bibtex]
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.
Download
[bibtex]
Alexandru Mereacre. Verification of Continuous-Space Stochastic Systems. Phd Thesis at RWTH Aachen University, 2011.
Download
[bibtex]
Alessandro Abate, Joost-Pieter Katoen, Alexandru Mereacre. Quantitative Automata Model Checking of Autonomous Stochastic Hybrid Systems. 14th ACM International Conference on Hybrid Systems: Computation and Control (HSCC), pages 83–92, ACM Press, 2011.
Download
[bibtex]
Ulrich Loup, Erika Abraham. GiNaCRA: A C++ Library for Real Algebraic Computations. 3rd NASA Formal Methods Symp. (NFM'11), Volume 6617 of LNCS, pages 512–517, Springer Berlin Heidelberg, 2011.

[bibtex]
E. Moritz Hahn, Tingting Han, Lijun Zhang. Synthesis for PCTL in Parametric Markov Decision Processes. NASA Formal Methods - Third International Symposium (NFM), Volume 6617 of LNCS, pages 146–161, , 2011.
Download
[bibtex]
Erika Abraham, Tobias Schubert, Bernd Becker, Martin Fraenzle, Christian Herde. Parallel SAT Solving in Bounded Model Checking. Journal of Logic and Computation 21(1), pages 5–21, 2011.
Download
[bibtex]
Xin Chen, Erika Abraham. Choice of Directions for the Approximation of Reachable Sets for Hybrid Systems. 13th Int. Conf. on Computer Aided Systems Theory (EUROCAST'11), Volume 6927 of LNCS, pages 535–542, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Joost-Pieter Katoen, Ivan S. Zapreev, E. Moritz Hahn, Holger Hermanns, David N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC. Performance Evaluation 68(2), pages 90–104, 2011.
Download
[bibtex]
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski. Abstract Probabilistic Automata. Verification, Model Checking and Abstract Interpretation (VMCAI), Volume 6538 of LNCS, pages 324–339, Springer-Verlag, 2011.
Download
[bibtex]
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.
Link
[bibtex]
Bastian Schlich, Thomas Noll, Jörg Brauer, Lucas Brutschy. Reduction of Interrupt Handler Executions for Model Checking Embedded Software. Proc. of 5th Int. Haifa Verification Conference (HVC 2009), Volume 6405 of LNCS, pages 5–20, Springer, 2011.
Download
[bibtex]
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen. Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. Performance Evaluation 68(2), pages 105–125, 2011.
Download
[bibtex]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. Logical Methods in Computer Science 7(1-2), pages 1–34, 2011.
Download
[bibtex]
Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Efficient CTMC Model Checking of Linear Real-Time Objectives. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 6605 of LNCS, pages 128–142, , 2011.
Download
[bibtex]
Pascal Richter, Erika Abraham, Gabriel Morin. Optimisation of Concentrating Solar Thermal Power Plants with Neural Networks. Int. Conf. on Adaptive and Natural Computing Algorithms (ICANNGA'11), Volume 6593 of LNCS, pages 190–199, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. SMT-based Counterexample Generation for Markov Chains. Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'11), pages 19–28, OFFIS-Institut für Informatik, 2011.

[bibtex]
Ralf Mitsching, Frank Fiedler, Henrik Bohnenkamp, Carsten Weise, Stefan Kowalewski. TripleT: Improving Test Responsiveness for High Performance Embedded Systems. Proc. 4th IEEE International Conference on Software Testing, Verification, and Validation (ICSTW), pages 67–74, IEEE, 2011.
Download
[bibtex]
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, Maria Prandini. A two-step scheme for approximate model checking of stochastic hybrid systems. Proceedings 18th IFAC World Congress 2011, Volume 18 of IFAC-PapersOnLine, Elsevier, 2011.
Download
[bibtex]
Bettina Braitling, Ralf Wimmer, Bernd Becker, Nils Jansen, Erika Abraham. SMT-based Counterexample Generation for Discrete-Time Markov Chains. Workshop on Rigorous Dependability Analysis using Model Checking Techniques for Stochastic Systems (ROCKS'11), , 2011.
Download
[bibtex]
Haidi Yue, Henrik Bohnenkamp, Malte Kampschulte, Joost-Pieter Katoen. Analysing and Improving Energy Efficiency of Distributed Slotted Aloha. 11th Int. Conf. on Next Generation Wired/Wireless Advanced Networking (NEW2AN), Volume 6869 of LNCS, pages 197–208, Springer-Verlag, 2011.
Download
[bibtex]
Florian Corzilius, Erika Abraham. Virtual Substitution for SMT Solving. 18th Int. Symp. on Fundamentals of Computation Theory (FCT'11), Volume 6914 of LNCS, pages 360–371, Springer Berlin Heidelberg, 2011.
Download
[bibtex]
Muhammad Fadlisyah, Peter Csaba Ölveczky, Erika Abraham. Object-Oriented Formal Modeling and Analysis of Interacting Hybrid Systems in HI-Maude. 9th Int. Conf. on Software Engineering and Formal Methods (SEFM'11), Volume 7041 of LNCS, pages 415–430, Springer Berlin Heidelberg, 2011.

[bibtex]
Hongfei Fu. Model Checking EGF on Basic Parallel Processes. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 6996 of LNCS, pages 120–134, Springer, 2011.

[bibtex]
Thomas Noll. Analyzing Reconfigurable Component-Based Systems Using Attribute Grammars. Pre-Proceedings 8th Int. Symp. on Formal Aspects of Component Software (FACS), Oslo University, 2011.
Link
[bibtex]
Hongfei Fu, Joost-Pieter Katoen. Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems. Foundations of Software Technology and Theoretical Computer Science (FSTTCS), Volume 13 of LIPIcs, pages 445–456, Schloss Dagstuhl, 2011.
DOI
[bibtex]
Thi Mai Thuong Tran, Martin Steffen, Erika Abraham. Inheritance and Observability. Proc. of the Nordic Workshop on Programming Theory (NWPT'11), Volume of Mathematical Structures in Computer Science, , 2011.

[bibtex]
Frédéric Herbreteau, Balaguru Srivathsan. Coarse abstractions make Zeno behaviours difficult to detect. CONCUR, Volume 6901 of LNCS, pages 92–107, Springer, 2011.

[bibtex]
Frédéric Herbreteau, Dileep Kini, Balaguru Srivathsan, Igor Walukiewicz. Using non-convex approximations for efficient analysis of timed automata. FSTTCS, Volume 13 of LIPIcs, pages 78 –89, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011.
Download
[bibtex]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Reachability probabilities in Markovian Timed Automata. Proceedings of the 50th IEEE Conference on Decision and Control and European Control Conference (CDC-ECC), pages 7075–7080, IEEE, 2011.
Download
[bibtex]
Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin. Verifiable Security of Boneh-Franklin Identity-Based Encryption. 5th International Conference on Provable Security, Volume 6980 of Lecture Notes in Computer Science, pages 68–83, Springer, 2011.
2010
Download
[bibtex]
Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, Carroll Morgan. Linear-Invariant Generation for Probabilistic Programs. Static Analysis Symposium (SAS), Volume 6337 of LNCS, pages 390–406, Springer-Verlag, 2010.
Download
[bibtex]
Erika Abraham, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. DTMC Model Checking by SCC Reduction. 7th Int. Conf. on Quantitative Evaluation of Systems (QEST'10), pages 37–46, IEEE, 2010.
Download
[bibtex]
Erika Abraham, Philipp Brauner, Nils Jansen, Thiemo Leonhardt, Ulrich Loup, Ulrik Schroeder. Podcastproduktion als kollaborativer Zugang zur theoretischen Informatik. Interaktive Kulturen - Die 8. E-Learning Fachtagung Informatik (DeLFI'10), Volume 169 of LNI, pages 239–251, Gesellschaft für Informatik, 2010.
Download
[bibtex]
Angelika Mader, Henrik Bohnenkamp, Yaroslav S. Usenko, David N. Jansen, Johann Hurink, Holger Hermanns. Synthesis and Stochastic Assessment of Cost-Optimal Schedules. Software Tools for Technology Transfer 12(5), pages 305–318, 2010.
Download
[bibtex]
Pierre Valadeau. Dependability and FDIR Model Based Analysis. Technical report at EADS Astrium number , 2010.
Download
[bibtex]
Haidi Yue, Joost-Pieter Katoen. Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption. 17th International Conference on Analytical and Stochastic Modelling Techniques and Applications (ASMTA), Volume 6148 of LNCS, pages 247–261, , 2010.
Link
[bibtex]
Maximilian R. Odenbrett, Viet Yen Nguyen, Thomas Noll. Slicing AADL Specifications for Model Checking. Proc. of the 2nd NASA Formal Methods Symp. (NFM 2010), Volume of NASA Conference Proceedings, pages 217–221, , 2010.
DOI
[bibtex]
Markus Geimer, Felix Wolf, Brian J. N. Wylie, Erika Abraham, Daniel Becker, Bernd Mohr. The Scalasca Performance Toolset Architecture. Concurrency and Computation: Practice and Experience 22(6), pages 702–719, 2010.
Download
[bibtex]
Daniel Klink. Three-Valued Abstraction for Stochastic Systems. Phd Thesis at RWTH Aachen University, 2010.
Download
[bibtex]
Joost-Pieter Katoen. Advances in Probabilistic Model Checking. Verification, Model Checking, and Abstract Interpretation (VMCAI), Volume 5944 of Lecture Notes in Computer Science, pages 25, Springer-Verlag, 2010.
Link
[bibtex]
Martin R. Neuhäußer. Model Checking Nondeterministic and Randomly Timed Systems. Phd Thesis at RWTH Aachen University and University of Twente, 2010.
Link
[bibtex]
Jonathan Heinen, Thomas Noll, Stefan Rieger. Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures. Proc. 3rd Int. Workshop on Harnessing Theories for Tool Support in Software (TTSS 2009), Volume 266 of ENTCS, pages 93–107, Elsevier, 2010.
Download
[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Performance Evaluation and Model Checking Join Forces. Communications of the ACM 53(9), pages 76–85, 2010.
Download
[bibtex]
Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Performability Assessment by Model Checking of Markov Reward Models. Formal Methods in Systems Design 36(1), pages 1–36, 2010.
Download
[bibtex]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. Learning Communicating Automata from MSCs. IEEE Transactions on Software Engineering 36(3), pages 390–408, 2010.
Download
[bibtex]
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, Maria Prandini. Approximate model checking of stochastic hybrid systems. European Journal of Control 16(6), pages 624–641, 2010.
Link
[bibtex]
Marco Bozzano, Roberto Cavada, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive. Formal Verification and Validation of AADL Models. Proc. of Embedded Real Time Software and Systems Conf. (ERTS$^2$ 2010), , 2010.
Link
[bibtex]
Lijun Zhang, Martin R. Neuhäußer. Model Checking Interactive Markov Chains. Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 6015 of Lecture Notes in Computer Science, pages 53–68, Springer, 2010.
Download
[bibtex]
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.
Download
[bibtex]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. SMA: The Smyle Modeling Approach. Computing and Informatics 29, pages 45–72, 2010.
Download
[bibtex]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer. A Model Checker for AADL. Proc. of 22nd Int. Conf. on Computer Aided Verification (CAV 2010), Volume 6174 of LNCS, pages 562–565, Springer, 2010.
Download
[bibtex]
Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga, Mark Timmer. A Linear Process Algebraic Format for Probabilistic Systems with Data. Applications of Concurrency to System Design (ACSD), IEEE CS Press, 2010.
Download
[bibtex]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker, Daniel Neider, David Piegdon. libalf: the Automata Learning Framework. Computer-Aided Verification (CAV), Volume 6174 of LNCS, pages 360–364, Springer-Verlag, 2010.
Download
[bibtex]
Daniela Lepri, Peter Csaba Ölveczky, Erika Abraham. Model Checking Classes of Metric LTL Properties of Object-Oriented Real-Time Maude Specifications. 1st Int. Workshop on Rewriting Techniques for Real-Time Systems (RTRTS'10), Volume 36 of Electronic Proceedings in Theoretical Computer Science, pages 117–136, Open Publishing Association, 2010.
Download
[bibtex]
Muhammad Fadlisyah, Erika Abraham, Daniela Lepri, Peter Csaba Ölveczky. A Rewriting-Logic-Based Technique for Modeling Thermal Systems. 1st Int. Workshop on Rewriting Techniques for Real-Time Systems (RTRTS'10), Volume 36 of Electronic Proceedings in Theoretical Computer Science, pages 82–100, Cornell University Library, 2010.
Download
[bibtex]
Haidi Yue, Henrik Bohnenkamp, Joost-Pieter Katoen. Analyzing Energy Consumption in a Gossiping MAC Protocol. Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance (MMB/DFT), Volume 5987 of LNCS, pages 107–119, Springer-Verlag, 2010.
Link
[bibtex]
Jörg Brauer, Thomas Noll, Bastian Schlich. Interval Analysis of Microcontroller Code using Abstract Interpretation of Hardware and Software. Proc. 13th International Workshop on Software and Compilers for Embedded Systems (SCOPES 2010), Volume of Digital Library, ACM, 2010.
Download
[bibtex]
Marijn R. Jongerden, Alexandru Mereacre, Henrik Bohnenkamp, Boudewijn R. Haverkort, Joost-Pieter Katoen. Computing Optimal Schedules for Battery Usage in Embedded Systems. IEEE Transactions on Industrial Informatics 6(3), pages 276–286, 2010.
Download
[bibtex]
Sabrina von Styp, Henrik Bohnenkamp, Julien Schmaltz. A Conformance Testing Relation for Symbolic Timed Automata. Proc. FORMATS 2010, Volume 6246 of LNCS, pages 243–255, Springer-Verlag, 2010.
Download
[bibtex]
Holger Hermanns, Joost-Pieter Katoen. The How and Why of Interactive Markov Chains. Formal Methods for Components and Objects (FMCO), Volume 6286 of LNCS, pages 311–337, Springer-Verlag, 2010.
Download
[bibtex]
Kai Bollue, Michaela Slaats, Erika Abraham, Wolfgang Thomas, Dirk Abel. Synthesis of Behavioral Controllers for DES: Increasing Efficiency. 10th Int. Workshop on Discrete-Event Systems (WODES'10), pages 30–37, IFAC, 2010.
Download
[bibtex]
Martin R. Neuhäußer, Lijun Zhang. Time-Bounded Reachability Probabilities in Continuous-Time Markov Decision Processes. Quantitative Evaluation of Systems (QEST), IEEE CS Press, 2010.
Download
[bibtex]
Falko Dulat, Joost-Pieter Katoen, Viet Yen Nguyen. Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report. Proceedings of 7th European Performance Engineering Workshop (EPEW 2010), Volume 6342 of LNCS, pages 115–130, Springer, 2010.
Link
[bibtex]
Jörg Brauer, Volker Kamin, Stefan Kowalewski, Thomas Noll. Loop Refinement Using Octagons and Satisfiability. Proc. of 5th International Workshop on Systems Software Verification (SSV 2010), , 2010.
Download
[bibtex]
Erika Abraham, Ulrich Loup, Florian Corzilius, Thomas Sturm. A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra,. Verification over Discrete-Continuous Boundaries, Dagstuhl Seminar, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2010.

[bibtex]
Natalia Kalinnik, Erika Abraham, Tobias Schubert, Ralf Wimmer, Bernd Becker. Exploiting Different Strategies for the Parallelization of an SMT Solver. 13. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'10), pages 97–106, Fraunhofer Verlag, 2010.
Download
[bibtex]
Muhammad Fadlisyah, Erika Abraham, Peter Csaba Ölveczky. Rewriting-Logic-Based Formal Modeling and Analysis of Interacting Hybrid Systems. Nordic Workshop on Programming Theory (NWPT'10), , 2010.
Download
[bibtex]
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.
Download
[bibtex]
Erika Abraham, Ulrich Loup, Ralf Wimmer, Joost-Pieter Katoen. On the Minimization of Hybrid Automata. Nordic Workshop on Programming Theory (NWPT'10), , 2010.

[bibtex]
Frédéric Herbreteau, Balaguru Srivathsan, Igor Walukiewicz. Efficient emptiness check for timed Büchi automata. CAV, Volume 6174 of LNCS, pages 148–161, Springer, 2010.

[bibtex]
Frédéric Herbreteau, Balaguru Srivathsan. Efficient on-the-fly emptiness check for timed Büchi automata. ATVA, Volume 6252 of LNCS, pages 218–232, Springer, 2010.

[bibtex]
Sabrina von Styp. Symbolic and Timed Testing. Proceedings of the Joint Workshop of the German Research Training Groups in Computer Science, Algorithmic synthesis of reactive and discrete-continuous systems, AlgoSyn 2010, , 2010.
2009

[bibtex]
Stefan Rieger. Verification of Pointer Programs. Phd Thesis at RWTH Aachen University, 2009.
Download
[bibtex]
Carsten Kern. Learning Communicating and Nondeterministic Automata. Phd Thesis at RWTH Aachen University, 2009.
Link
[bibtex]
Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Codesign of Dependable Systems: A Component-Based Modeling Language. Proc. 7th ACM-IEEE Int. Conf. on Formal Methods and Models for Codesign (MEMOCODE 2009), pages 121–130, IEEE CS Press, 2009.
Download
[bibtex]
Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik Bohnenkamp, Joost-Pieter Katoen. Maximizing System Lifetime by Battery Scheduling. 39th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, pages 63–72, IEEE Computer Society, 2009.
Download
[bibtex]
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.
Link
[bibtex]
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.
Download
[bibtex]
Viet Yen Nguyen, Theo C. Ruys. Memoised Garbage Collection for Software Model Checking. Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume of LNCS, Springer-Verlag, 2009.
Link
[bibtex]
Niels H.M. Aan de Brugh, Viet Yen Nguyen, Theo C. Ruys. MoonWalker: Verification of .NET Programs. Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume of LNCS, Springer-Verlag, 2009.
Link
[bibtex]
Martin R. Neuhäußer, Marielle Stoelinga, Joost-Pieter Katoen. Delayed Nondeterminism in Continuous-Time Markov Decision Processes. Foundations of Software Science and Computation Structures (FoSSaCS), Volume 5504 of LNCS, pages 364–379, Springer-Verlag, 2009.
Download
[bibtex]
Tingting Han, Joost-Pieter Katoen, Berteun Damman. Counterexample Generation in Probabilistic Model Checking. IEEE Transactions on Software Engineering 35(2), pages 241–257, 2009.

[bibtex]
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.

[bibtex]
. Proc. DSN 2009. IEEE Computer Society, 2009.

[bibtex]
Ralf Mitsching, Carsten Weise, André Kolbe, Henrik Bohnenkamp, Norbert Berzen. Towards an industrial strength process for timed testing. IEEE International Conference on Software Testing, Verification, and Validation, pages 29–38, IEEE Computer Society, 2009.
Download
[bibtex]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications. IEEE Symposium on Logic in Computer Science (LICS), IEEE CS Press, 2009.
Download
[bibtex]
Benedikt Bollig, Peter Habermehl, Carsten Kern, Martin Leucker. Angluin-Style Learning of NFA. Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI-09), pages 1004–1009, AAAI Press, 2009.
Link
[bibtex]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems. Proc. 28th Int. Conf. on Computer Safety, Reliability and Security (SAFECOMP 2009), Volume 5775 of LNCS, pages 173–186, Springer, 2009.
Download
[bibtex]
Joost-Pieter Katoen, Ivan S. Zapreev. Simulation-based CTMC Model Checking: An Empirical Evaluation. Quantitative Evaluation of Systems (QEST), pages 31–40, IEEE CS Press, 2009.
Download
[bibtex]
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen. Time-Bounded Reachability in Tree-Structured QBDs by Abstraction. Quantitative Evaluation of Systems (QEST), pages 133–142, IEEE CS Press, 2009.
Download
[bibtex]
Joost-Pieter Katoen, Ivan S. Zapreev, E. Moritz Hahn, Holger Hermanns, David N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC. Quantitative Evaluation of Systems (QEST), pages 167–176, IEEE CS Press, 2009.
Download
[bibtex]
Joost-Pieter Katoen, Daniel Klink, Martin R. Neuhäußer. Compositional Abstraction of Stochastic Systems . Formal Modeling and Analysis of Timed Systems (FORMATS), Volume 5813 of LNCS, pages 195–211, Springer, 2009.
Download
[bibtex]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. LTL model checking of time-inhomogeneous Markov chains. 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09), Volume 5799 of LNCS, pages 104–119, , 2009.
Link
[bibtex]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Verification and Performance Evaluation of AADL Models (Tool Demonstration). 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.
Link
[bibtex]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Model-Based Codesign of Critical Embedded Systems. Proc. 2nd Int. Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB 2009), Volume 507 of CEUR Workshop Proceedings, pages 87–91, , 2009.
Download
[bibtex]
Tingting Han. Diagnosis, Synthesis and Analysis of Probabilistic Models. Phd Thesis at University of Twente and RWTH Aachen University, 2009.
DOI
[bibtex]
Erika Abraham, Immo Grabe, Andreas Grüner, Martin Steffen. Behavioral Interface Description of an Object-oriented Language with Futures and Promises. Journal of Logic and Algebraic Programming 78(7), pages 491–518, 2009.
Download
[bibtex]
Natalia Kalinnik, Tobias Schubert, Erika Abraham, Ralf Wimmer, Bernd Becker. Picoso - A Parallel Interval Constraint Solver. Int. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA'09), pages 473–479, CSREA Press, 2009.

[bibtex]
Sabrina von Styp. Towards a theory for timed symbolic testing. Proceedings of Formal Methods 2009 Doctoral Symposium, Volume 09-15 of CS-Report , pages 39–45, Technical University Eindhoven, 2009.
Download
[bibtex]
Erika Abraham, Ulrich Loup. SMT-Solving for the First-Order Theory of the Reals. Algorithms and Applications for Next Generation SAT Solvers, Dagstuhl Seminar, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany, 2009.

[bibtex]
Hongfei Fu. Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable. 7th Asian Symposium on Programming Languages and Systems (APLAS), Volume 5904 of LNCS, pages 327–342, Springer, 2009.
Download
[bibtex]
Santiago Zanella Béguelin, Benjamin Grégoire, Gilles Barthe, Federico Olmedo. Formally Certifying the Security of Digital Signature Schemes. 30th IEEE Symposium on Security and Privacy, pages 237–250, IEEE Computer Society, 2009.
2008
Download
[bibtex]
Manuela Bujorianu, Joost-Pieter Katoen. Symmetry reduction for stochastic hybrid systems. Proceedings 47th IEEE Conference on Decision and Control (CDC), pages 233–238, IEEE Control Systems Society, 2008.
Download
[bibtex]
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Approximate parameter synthesis for probabilistic time-bounded reachability. Proceedings of IEEE Real-Time Systems Symposium (RTSS), pages 173–182, IEEE CS Press, 2008.
Download
[bibtex]
Joost-Pieter Katoen. How to model and analyze gossiping protocols?. ACM Performance Evaluation Review 36(3), pages 3–6, 2008.
Download
[bibtex]
Xin Chen, Yuxin Deng. Game Characterizations of Process Equivalences. Proceedings of the 6th Asian Symposium on Programming Languages and Systems (APLAS'08), Volume 5356 of Lecture Notes in Computer Science, pages 107–121, Springer Verlag, 2008.

[bibtex]
Lijun Zhang, Friedrich Eisenbrand, Holger Hermanns, David N. Jansen. Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations. Logical Methods in Computer Science 4(4), 2008.
Download
[bibtex]
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.
Download
[bibtex]
Berteun Damman, Tingting Han, Joost-Pieter Katoen. Regular Expressions for PCTL Counterexamples. Proceedings 5th International Conference on Quantitative Evaluation of Systems (QEST), pages 179–188, IEEE CS Press, 2008.
Download
[bibtex]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Abstraction for Stochastic Systems by Erlang's Method of Stages. 19th International Conference on Concurrency Theory (CONCUR'08), Volume 5201 of LNCS, pages 279–294, Springer, 2008.
Download
[bibtex]
Benedikt Bollig, Carsten Kern, Joost-Pieter Katoen, Martin Leucker. Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning. 19th International Conference on Concurrency Theory (CONCUR'08), Volume 5201 of LNCS, pages 162–166, Springer, 2008.
Link
[bibtex]
Viet Yen Nguyen, Theo C. Ruys. Incremental Hashing for SPIN. Proceedings 15th International SPIN Workshop on Model Checking Software, Volume 5156 of LNCS, pages 232–249, , 2008.
Download
[bibtex]
Taolue Chen, Tingting Han, Joost-Pieter Katoen. Time-Abstracting Bisimulation for Probabilistic Timed Automata. 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 177–184, IEEE CS Press, 2008.
Download
[bibtex]
Christel Baier, Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008.
Download
[bibtex]
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains. Hybrid Systems: Computation and Control (HSCC), Volume 4981 of LNCS, pages 244–258, Springer Verlag, 2008.
Download
[bibtex]
Ivan S. Zapreev. Model Checking Markov Chains: Techniques and Tools. Phd Thesis at University of Twente, 2008.
Download
[bibtex]
Henrik Bohnenkamp, Marielle Stoelinga. Quantitative Testing. Technical report at RWTH Aachen number AIB-2008-02, 2008.
Download
[bibtex]
David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Marielle Stoelinga, Ivan S. Zapreev. How fast and fat is your probabilistic model checker? An experimental comparison. Hardware and Software: Verification and Testing (Haifa Verification Conference, HVC), Volume 4899 of LNCS, pages 69–85, Springer, 2008.
Link
[bibtex]
Thomas Noll, Bastian Schlich. Delayed Nondeterminism in Model Checking Embedded Systems Assembly Code. Hardware and Software: Verification and Testing (Haifa Verification Conference, HVC 2007), Volume 4899 of LNCS, pages 185–201, Springer, 2008.
Link
[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Reachability in continuous-time Markov reward decision processes. In Erich Graedel, Joerg Flum, Thomas Wilke editors, Logic and Automata: History and Perspectives, pages 53–72, Volume 2 of Texts in Logics and Games, 2008.
Link
[bibtex]
Gerlind Herberich, Thomas Noll, Bastian Schlich, Carsten Weise. Proving Correctness of an Efficient Abstraction for Interrupt Handling. Proceedings 3rd International Workshop on Systems Software Verification (SSV 2008), Volume 217 of ENTCS, pages 133–150, Elsevier, 2008.
Link
[bibtex]
Lars Helge Haß, Thomas Noll. Equational Abstractions for Reducing the State Space of Rewrite Theories. Proc. of 7th Int. Workshop on Rewriting Logic and its Applications (WRLA 2008), Volume 238 of ENTCS, pages 139–154, Elsevier, 2008.
Download
[bibtex]
Thomas Noll, Stefan Rieger. Verifying Dynamic Pointer-Manipulating Threads. Proceedings 15th International Symposium on Formal Methods (FM 2008), Volume 5014 of LNCS, pages 84–99, Springer, 2008.
Download
[bibtex]
Joost-Pieter Katoen. Perspectives in Probabilistic Verification. 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering (TASE), pages 3–10, IEEE CS Press, 2008.
Download
[bibtex]
Mani Swaminathan, Martin Fraenzle, Joost-Pieter Katoen. The Surprising Robustness of (Closed) Timed Automata against Clock-Drift. 5th IFIP International Conference on Theoretical Computer Science (IFIP TCS), Volume 273 of IFIP, pages 537–553, Springer, 2008.
Link
[bibtex]
Stefan Rieger, Thomas Noll. Abstracting Complex Data Structures by Hyperedge Replacement. 4th Int. Conference on Graph Transformations (ICGT 2008), Volume 5214 of LNCS, pages 69–83, Springer, 2008.
Download
[bibtex]
Joost-Pieter Katoen, Alexandru Mereacre. Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains. Formal Modeling and Analysis of Timed Systems (FORMATS), Volume 5215 of LNCS, pages 203–217, Springer-Verlag, 2008.
Download
[bibtex]
Henrik Bohnenkamp, Marielle Stoelinga. Quantitative Testing. Proceedings 8th ACM & IEEE International Conference on Embedded Software (EMSOFT), pages 227–236, ACM Press, 2008.

[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Deductive Proof System for Multithreaded Java with Exceptions. Fundamenta Informaticae 82(4), pages 391–463, 2008.
DOI
[bibtex]
Erika Abraham, Andreas Grüner, Martin Steffen. Heap-Abstraction for an Object-Oriented Calculus with Thread Classes. Software and Systems Modeling 7(2), pages 177–208, 2008.
DOI
[bibtex]
Erika Abraham, Andreas Grüner, Martin Steffen. Abstract Interace Behavior of Object-Oriented Languages with Monitors. Theory of Computing Systems 43(3), pages 322–361, 2008.

[bibtex]
Markus Geimer, Felix Wolf, Brian J. N. Wylie, Erika Abraham, Daniel Becker, Bernd Mohr. The SCALASCA Performance Toolset Architecture. Int. Workshop on Scalable Tools for High-End Computing (STHEC'08), pages 56–65, , 2008.

[bibtex]
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, Zoltan Szebenyi. Usage of the SCALASCA Toolset for Scalable Performance Analysis of Large-Scale Parallel Applications. 2nd HLRS Parallel Tools Workshop, pages 157–167, , 2008.
Download
[bibtex]
Joost-Pieter Katoen. Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques. Design, Automation and Test in Europe (DATE), pages 86–87, IEEE CS Press, 2008.
2007
Download
[bibtex]
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.
Download
[bibtex]
Tingting Han, Joost-Pieter Katoen. Providing evidence of likely being on time – Counterexample generation for CTMC model checking. Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA'07), Volume of Lecture Notes in Computer Science, Springer Verlag, 2007.
Download
[bibtex]
Joost-Pieter Katoen. Abstraction of Probabilistic Systems. Formal Methods for Timed Systems (FORMATS'07), Volume 4763 of LNCS, pages 1–3, Springer-Verlag, 2007.

[bibtex]
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.
Download
[bibtex]
Martin R. Neuhäußer, Joost-Pieter Katoen. Bisimulation and Logical Preservation for Continuous-Time Markov Decision Processes. 18th International Conference on Concurrency Theory (CONCUR'07), Volume 4703 of LNCS, pages 412–427, Springer-Verlag, 2007.
Download
[bibtex]
Thomas Noll, Stefan Rieger. Composing Transformations to Optimize Linear Code. Proc. 4th Int. Colloquium on Theoretical Aspects of Computing (ICTAC 2007), Volume 4711 of LNCS, pages 425–439, , 2007.
Download
[bibtex]
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.
Download
[bibtex]
Martin R. Neuhäußer, Thomas Noll. Abstraction and Model Checking of Core Erlang Programs in Maude. Proceedings of the 6th International Workshop on Rewriting Logic and its Applications, Volume 176 of ENTCS, pages 147–163, Elsevier, 2007.
Download
[bibtex]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Three-valued abstraction for continuous-time Markov chains. Proceedings of the 19th International Conference on Computer Aided Verification (CAV), Volume 4590 of Lecture Notes in Computer Science, pages 311–324, Springer Verlag, 2007.
Download
[bibtex]
Henrik Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen. Motor: The MoDeST Tool Environment. Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07), Volume 4424 of Lecture Notes in Computer Science, pages 500–504, Springer-Verlag, 2007.
Download
[bibtex]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. Replaying Play in and Play out: Synthesis of Design Models from Scenarios by Learning. Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07), Volume 4424 of Lecture Notes in Computer Science, pages 435–450, Springer Verlag, 2007.
Download
[bibtex]
Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking.. Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07), Volume 4424 of Lecture Notes in Computer Science, pages 76–92, Springer Verlag, 2007.
Download
[bibtex]
Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying Concurrent List-Manipulating Programs by LTL Model Checking. Workshop on Heap Analysis and Verification (HAV 2007), pages 94–113, , 2007.
Download
[bibtex]
Tingting Han, Joost-Pieter Katoen. Counterexamples in probabilistic model checking. Proceedings of the 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'07), Volume 4424 of Lecture Notes in Computer Science, pages 60–75, Springer Verlag, 2007.
DOI
[bibtex]
Erika Abraham, Marc Herbstritt, Bernd Becker, Martin Steffen. Bounded Model Checking with Parametric Data Structures. Int. Workshop on Bounded Model Checking (BMC'06), Volume 174 of ENTCS, pages 3–16, Elsevier Science Publishers, 2007.
Download
[bibtex]
Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, Michele Loreti, Mieke Massink. Model checking mobile stochastic logic. Theoretical Computer Science 382, pages 42–70, 2007.
Download
[bibtex]
Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen. Flow faster: efficient decision algorithms for probabilistic simulations. Tools and algorithms for the construction and analysis of systems, Volume 4424 of Lecture notes in computer science, pages 155–169, Springer, 2007.

[bibtex]
Henrik Bohnenkamp, Axel Belinfante. Timed Model-Based Testing. Tangram: Model-based integration and testing of complex high-tech systems, pages 115–128, Embedded Systems Institute, The Netherlands, 2007.
DOI
[bibtex]
Marc Herbstritt, Bernd Becker, Erika Abraham, Christian Herde. On Variable Selection in SAT-LP-based Bounded Model Checking of Linear Hybrid Automata. IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS'07), pages 1–6, IEEE Computer Society, 2007.

[bibtex]
Erika Abraham, Immo Grabe, Andreas Grüner, Martin Steffen. Abstract Interface Behavior of an Object-Oriented Language with Futures and Promises. Nordic Workshop on Programming Theory (NWPT'07), , 2007.
2006
Download
[bibtex]
Joost-Pieter Katoen. Stochastic model checking. In Christos G. Cassandras, John Lygeros editors, Stochastic Hybrid Systems: Recent Developments and Research Trends, 2006.
Download
[bibtex]
Dino Distefano, Joost-Pieter Katoen, Arend Rensink. Safety and liveness in concurrent pointer programs. Formal Methods for Components and Objects, Volume 4111 of LNCS, pages 280–312, Springer-Verlag, 2006.
Download
[bibtex]
Henrik Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen. MoDeST: A compositional modeling formalism for hard and softly timed systems. IEEE Transactions on Software Engineering 32(10), pages 812–830, 2006.
Download
[bibtex]
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.

[bibtex]
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.
Download
[bibtex]
Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen. Probably on time and within budget – On reachability in priced probabilistic timed automata. Quantitative Evaluation of Systems (QEST), IEEE CS Press, 2006.
Download
[bibtex]
Joost-Pieter Katoen, Ivan S. Zapreev. Safe on-the-fly steady-state detection for time-bounded reachability. Quantitative Evaluation of Systems (QEST), pages 301–310, IEEE CS Press, 2006.
Download
[bibtex]
Tingting Han, Joost-Pieter Katoen. Counterexamples in probabilistic model checking. Technical report at RWTH Aachen number AIB 2006-09, 2006.
Link
[bibtex]
Thomas Noll, Stefan Rieger. Optimization of Straight-Line Code Revisited. Softwaretechnik-Trends 26(2), 2006.
Download
[bibtex]
Benedikt Bollig, Carsten Kern, Markus Schlütter, Volker Stolz. MSCan - A Tool for Analyzing MSC Specifications. Proceedings of the 12th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'06), Volume 3920 of Lecture Notes in Computer Science, pages 455–458, Springer, 2006.
Download
[bibtex]
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.
Download
[bibtex]
Rocco De Nicola, Joost-Pieter Katoen, Diego Latella, Mieke Massink. Towards a logic for performance and mobility. Electronic Notes in Theoretical Computer Science 153, pages 161–175, 2006.
Link
[bibtex]
Klaus Indermark, Thomas Noll. Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information. Acta Informatica 43(1), pages 1–43, 2006.

[bibtex]
Chanchal Kumar Roy, Thomas Noll, Banani Roy, James R. Cordy. Towards Automatic Verification of Erlang Programs by pi-Calculus Translation. Proceedings of the ACM SIGPLAN 2006 Erlang Workshop, pages 38–50, ACM Press, 2006.
Download
[bibtex]
Mario Bravetti, Holger Hermanns, Joost-Pieter Katoen. YMCA: Why Markov Chain Algebra?. Electronic Notes in Theoretical Computer Science 162, pages 107–112, 2006.
DOI
[bibtex]
Erika Abraham, Tobias Schubert, Bernd Becker, Martin Fraenzle, Christian Herde. Parallel SAT Solving in Bounded Model Checking. Parallel and Distributed Methods in Verification (PDMC'06), Volume 4346 of LNCS, pages 301–315, Springer Berlin Heidelberg, 2006.

[bibtex]
Erika Abraham, Marc Herbstritt, Bernd Becker, Martin Steffen. Memory-Aware Bounded Model Checking for Linear Hybrid Systems. 9th. Workshop for Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'06), pages 153–162, , 2006.

[bibtex]
Erika Abraham, Andreas Grüner, Martin Steffen. Heap-Abstraction for an Object-Oriented Calculus with Thread Classes. Logical Approaches to Computational Barriers: 2nd Conf. on Computability in Europe (CiE'06), Volume 3988 of LNCS, pages 1–10, Springer-Verlag, 2006.

[bibtex]
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.
DOI
[bibtex]
Erika Abraham, Andreas Grüner, Martin Steffen. Abstract Interface Behavior of Object-Oriented Languages with Monitors. 8th IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS'06), Volume 4037 of LNCS, pages 218–232, Springer Berlin Heidelberg, 2006.
2005
Download
[bibtex]
Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Verena Wolf. Comparative branching-time semantics for Markov chains. Information and Computation 200(2), pages 149–214, 2005.
Download
[bibtex]
Carsten Kern. Analysis and Imlementations of MSC Specifications. IFM2005 Doctoral Symposium on Integrated Formal Methods, Volume of Technische universiteit eindhoven: Computer Science-Report 05-29, pages 55–61, Judi Romijn, Graeme Smith, Jaco van de Pol, 2005.

[bibtex]
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.
Download
[bibtex]
Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev. A Markov reward model checker. Quantitative Evaluation of Systems (QEST), pages 243–244, IEEE CS Press, 2005.

[bibtex]
. Proceedings of the 2005 International Conference on Dependable Systems and Networks (DSN 2005). IEEE Computer Society, 2005.
Download
[bibtex]
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.
Download
[bibtex]
Erika Abraham. An Assertional Proof System for Multithreaded Java — Theory and Tool Support. Phd Thesis at University of Leiden, 2005.
Download
[bibtex]
Henrik Bohnenkamp, Axel Belinfante. Timed Testing with TorX. Formal Methods 2005, pages 173–188, Springer-Verlag, 2005.
Download
[bibtex]
Henrik Bohnenkamp, Johan Gorter, Jarno Guidi, Joost-Pieter Katoen. Are you still there? — A Lightweight Algorithm To Monitor Node Presence in Self-Configuring Networks. , pages 704–709, , 2005.

[bibtex]
John Fitzgerald, Ian Hayes, Andrzej Tarlecki editors. Formal Methods 2005. Springer-Verlag, Volume 3582 of LNCS, 2005.
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen. A theory of stochastic systems. Part I: Stochastic automata. Information and Computation 203(1), pages 1–38, 2005.
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen. A theory of stochastic systems. Part II: Process algebra. Information and Computation 203(1), pages 39–74, 2005.

[bibtex]
Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, Alexander Pretschner editors. Model-Based Testing of Reactive Systems (Advanced Lectures). Springer-Verlag, Volume 3472 of Lecture Notes in Computer Science, 2005.
Download
[bibtex]
Lucia Cloth, Joost-Pieter Katoen, Maneesh Khattri, Reza Pulungan. Model checking Markov reward models with impulse rewards. , pages 722–731, , 2005.
Download
[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Model checking meets performance evaluation. SIGMETRICS Performance Evaluation Review 32(4), pages 10–15, 2005.
Download
[bibtex]
Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Boudewijn R. Haverkort. Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theoretical Computer Science 345(1), pages 2–26, 2005.
Link
[bibtex]
Thomas Noll. Equational Abstractions for Model Checking Erlang Programs. Proceedings of the International Workshop on Software Verification and Validation (SVV 2003), Volume 118 of ENTCS, pages 145–162, Elsevier, 2005.
Link
[bibtex]
Martin Leucker, Thomas Noll, Perdita Stevens, Michael Weber. Functional Programming Languages for Verification Tools: A Comparison of ML and Haskell. Software Tools for Technology Transfer 7(2), pages 184–194, 2005.
Link
[bibtex]
Thomas Noll, Chanchal Kumar Roy. Modeling Erlang in the pi-Calculus. Proceedings of the ACM SIGPLAN 2005 Erlang Workshop, pages 72–77, ACM Press, 2005.
Download
[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. An Assertion-Based Proof System for Multithreaded Java. Theoretical Computer Science 331(2-3), pages 251–290, 2005.
DOI
[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Inductive Proof Outlines for Exceptions in Multithreaded Java. Foundations of Software Engineering (Theory and Practice) (FSEN'05), Volume 159 of ENTCS, pages 281–297, Elsevier Science Publishers, 2005.
DOI
[bibtex]
Erika Abraham, Bernd Becker, Felix Klaedke, Martin Steffen. Optimizing Bounded Model Checking for Linear Hybrid Systems. Verification, Model Checking, and Abstract Interpretation (VMCAI'05), Volume 3385 of LNCS, pages 396–412, Springer Berlin Heidelberg, 2005.

[bibtex]
Erika Abraham, Andreas Grüner, Martin Steffen. Dynamic Heap-Abstraction for Open, Object-Oriented Systems with Thread Classes. Proc. of the 1st Int. Workshop on the Verification of Concurrent Systems with Dynamic Allocated Heaps (COSMICAH'05), pages 47-61, Queen Mary Technical Report RR-05-04, 2005.
2004
Download
[bibtex]
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.

[bibtex]
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.
Download
[bibtex]
Henrik Bohnenkamp, Holger Hermanns, Ric Klaren, Angelika Mader, Yaroslav Usenko. Synthesis and stochastic assessment of schedules for lacquer production. Quantitative Evaluation of Systems (QEST 2004), pages 28–37, IEEE Computer Society Press, 2004.
Download
[bibtex]
Joost-Pieter Katoen, Henrik Bohnenkamp, Ric Klaren, 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, 2004.

[bibtex]
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.
Download
[bibtex]
Dino Distefano, Joost-Pieter Katoen, Arend Rensink. Who is pointing when to whom? – On the automated verification of linked list structures. Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pages 250–262, LNCS vol. 3328, Springer-Verlag, 2004.
Download
[bibtex]
Mieke Massink, Joost-Pieter Katoen, Diego Latella. Model checking dependability attributes of wireless group communication. Dependable Systems and Networks (DSN), pages 711–720, IEEE Computer Society, 2004.
Download
[bibtex]
Christel Baier, Holger Hermanns, Joost-Pieter Katoen. Probabilistic weak simulation is decidable in polynomial time. Information Processing Letters 89(3), pages 123–130, 2004.

[bibtex]
Giuliana Franceschinis, Boudewijn R. Haverkort, Joost-Pieter Katoen, Murray Woodside editors. Proceedings of the First Int. Conf. on Quantitative Evaluation of Systems (QEST). IEEE CS Press, 2004.

[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen, Markus Siegle editors. Validation of Stochastic Systems. Springer-Verlag, Volume 2925 of LNCS, 2004.
Download
[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Efficient computation of maximal timed reachability probabilities in uniform continuous-time Markov decision processes. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 61–76, LNCS vol. 2988, Springer-Verlag, 2004.
DOI
[bibtex]
Erika Abraham, Marcello M. Bonsangue, Frank S. de Boer, Martin Steffen. Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes. Theoretical Aspects of Computing (ICTAC'04), Volume 3407 of LNCS, pages 37–51, Springer Berlin Heidelberg, 2004.
DOI
[bibtex]
Erika Abraham, Frank S. de Boer, Marcello M. Bonsangue, Andreas Grüner, Martin Steffen. Observability, Connectivity, and Replay in a Sequential Calculus of Classes. Formal Methods for Components and Objects (FMCO'04), Volume 3657 of LNCS, pages 296–316, Springer Berlin Heidelberg, 2004.
DOI
[bibtex]
Frank S. de Boer, Marcello M. Bonsangue, Martin Steffen, Erika Abraham. A Fully Abstract Trace Semantics for UML Components. Formal Methods for Components and Objects (FMCO'04), Volume 3657 of LNCS, pages 49–69, Springer Berlin Heidelberg, 2004.

[bibtex]
Erika Abraham, Marcello M. Bonsangue, Frank S. de Boer, Martin Steffen. Classes, Object Connectivity, and Observability (Extended abstract). 12. Kolloquium Programmiersprachen und Grundlagen der Programmierung, University Freiburg, 2004.

[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Inductive Proof Outlines for Multithreaded Java with Exceptions. 12. Kolloquium Programmiersprachen und Grundlagen der Programmierung, , 2004.
2003

[bibtex]
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.

[bibtex]
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.

[bibtex]
. Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003). IEEE Computer Society Press, 2003.

[bibtex]
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.
Download
[bibtex]
Henrik Bohnenkamp, Peter van der Stok, Holger Hermanns, Frits Vaandrager. Cost-optimization of the IPv4 Zeroconf protocol. , pages 531–540, , 2003.
Download
[bibtex]
Henrik Bohnenkamp, Tod Courtney, David Daly, Salem Derisavi, Holger Hermanns, Joost-Pieter Katoen, Vinh Vi Lam, Bill Sanders. On integrating the Möbius and MoDeST modeling tools. Dependable Systems and Networks (DSN), pages 671, IEEE, 2003.
Download
[bibtex]
Henrik Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen, Ric Klaren. The MoDeST Modeling Tool and its implementation. Computer Performance Evaluation: Modelling Techniques and Tools (TOOLS 2003), Volume 2794 of LNCS, Springer-Verlag, 2003.

[bibtex]
Lars-Åke Fredlund, Dilian Gurov, Thomas Noll, Mads Dam, Thomas Arts, Gennady Chugunov. A Verification Tool for Erlang. Software Tools for Technology Transfer 4(4), pages 405–420, 2003.

[bibtex]
Thomas Noll. Term Rewriting Models of Concurrency: Foundations and Applications. Habilitation Thesis. RWTH Aachen University, 2003.
Download
[bibtex]
David N. Jansen, Holger Hermanns, Joost-Pieter Katoen. A QoS-Oriented Extension of UML Statecharts. The Unified Modeling Language (UML), Volume 2853 of LNCS, pages 76–92, Springer-Verlag, 2003.
Download
[bibtex]
Suzana Andova, Holger Hermanns, Joost-Pieter Katoen. Discrete-time rewards model-checked. Formal Methods for Timed Systems (FORMATS), Volume 2791 of LNCS, pages 88–104, Springer-Verlag, 2003.
Download
[bibtex]
Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Verena Wolf. Comparative branching-time semantics for Markov chains. Concurrency Theory (CONCUR), Volume 2761 of LNCS, pages 492–508, Springer-Verlag, 2003.
Download
[bibtex]
Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle. A tool for model-checking Markov chains. STTT 4(2), pages 153–172, 2003.
Download
[bibtex]
Peter Buchholz, Joost-Pieter Katoen, Peter Kemper, Carsten Tepper. Model-checking large structured Markov chains. J. Log. Algebr. Program 56(1-2), pages 69–97, 2003.
Download
[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Model-checking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering 29(6), pages 524–541, 2003.
DOI
[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Compositional Operational Semantics for JavaMT. Verification: Theory and Practice, Celebrating Zohar Manna's 64th Birthday, Volume 2772 of LNCS, pages 290–303, Springer Berlin Heidelberg, 2003.
DOI
[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Inductive Proof-Outlines for Monitors in Java. Formal Methods for Open Object-Based Distributed Systems (FMOODS'03), Volume 2884 of LNCS, pages 155–169, Springer Berlin Heidelberg, 2003.
DOI
[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Tool-Supported Proof System for Multithreaded Java. Formal Methods for Components and Objects (FMCO'02), Volume 2852 of LNCS, pages 1–32, Springer Berlin Heidelberg, 2003.

[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. A Tool-supported Assertional Proof System for Multithreaded Java. Proc. of the Workshop on Formal Techniques for Java-like Programs (FTfJP'03), Technical report 408 from the ETH Zürich, 2003.
2002

[bibtex]
Holger Hermanns, Roberto Segala editors. Process Algebra and Probabilistic Methods (PAPM-ProbmiV 2002). Springer Verlag, Volume 2399 of Lecture Notes in Computer Science, 2002.

[bibtex]
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.

[bibtex]
Henrik Bohnenkamp, Boudewijn R. Haverkort. The Mean Value of the Maximum. , pages 37–56, , 2002.

[bibtex]
Benedikt Bollig, Martin Leucker, Thomas Noll. Generalized Regular MSC Languages. Proceedings 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2002), pages 52–66, Springer-Verlag, 2002.

[bibtex]
Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, Christel Baier. Model checking performability properties. Dependable Systems and Networks (DSN), pages 103–113, IEEE CS Press, 2002.

[bibtex]
David N. Jansen, Holger Hermanns, Joost-Pieter Katoen. A probabilistic extension of UML statecharts – specification and verification. Formal Techniques for Real-Time and Fault-Tolerant systems (FTRTFT), Volume 2469 of LNCS, pages 355–374, Springer-Verlag, 2002.

[bibtex]
Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Boudewijn R. Haverkort. Simulation for continuous-time Markov chains. Concurrency Theory (CONCUR), Volume 2421 of LNCS, pages 338–354, Springer-Verlag, 2002.

[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Automated performance and dependability evaluation using model checking. Computer Performance Evaluation, Volume 2459 of LNCS, pages 261–289, Springer-Verlag, 2002.

[bibtex]
Dino Distefano, Arend Rensink, Joost-Pieter Katoen. Model checking birth and death. IFIP Working Conference on Theoretical Computer Science (TCS), Volume 223 of IFIP Proceedings, pages 435–447, Kluwer Academic Publishers, 2002.

[bibtex]
Holger Hermanns, Ulrich Herzog, Joost-Pieter Katoen. Process algebra for performance evaluation. Theor. Comput. Sci 274(1-2), pages 43–87, 2002.

[bibtex]
Joost-Pieter Katoen, Perdita Stevens editors. Tools and Algorithms for the Construction and Analysis of Computer Systems (TACAS). LNCS vol. 2280, Springer-Verlag, 2002.
DOI
[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Verification for Java's Reentrant Multithreading Concept. Foundations of Software Science and Computation Structures (FoSSaCS'02), Volume 2303 of LNCS, pages 5–20, Springer Berlin Heidelberg, 2002.

[bibtex]
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
Link
[bibtex]
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.

[bibtex]
Lucia Cloth, Henrik Bohnenkamp, Boudewijn R. Haverkort. Using Max-Plus Algebra for the Evaluation of Stochastic Process Algebra Prefixes. , , 2001.

[bibtex]
Lars-Åke Fredlund, Dilian Gurov, Thomas Noll. Semi-Automated Verification of Erlang Code. Proc. 16th IEEE International Conference on Automated Software Engineering (ASE 2001), pages 319–323, IEEE Computer Society Press, 2001.

[bibtex]
. Kolloquium Programmiersprachen und Grundlagen der Programmierung. Technical report at Aachen University of Technology number 2001-11, 2001.

[bibtex]
Martin Leucker, Thomas Noll. Truth/SLC – A Parallel Verification Platform for Concurrent Systems (tool description). Proceedings 13th Conference on Computer Aided Verification (CAV 2001), pages 255–259, Springer-Verlag, 2001.

[bibtex]
Thomas Noll. A Rewriting Logic Implementation of Erlang. Proceedings of First Workshop on Language Descriptions, Tools and Applications (ETAPS/LDTA 2001), Elsevier Science Publishers, 2001.

[bibtex]
Benedikt Bollig, Martin Leucker, Thomas Noll. Regular MSC Languages. Technical report at RWTH Aachen University number 01-05, 2001.

[bibtex]
Thomas Noll, Lars-Åke Fredlund, Dilian Gurov. The Erlang Verification Tool (tool description). Proceedings 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), Volume 2031 of Lecture Notes in Computer Science, pages 582–585, , 2001.

[bibtex]
Thomas Arts, Thomas Noll. Verifying Generic Erlang Client–Server Implementations. Selected Papers of the 12th International Workshop on the Implementation of Functional Languages (IFL 2000), pages 37–52, , 2001.

[bibtex]
Martin Leucker, Thomas Noll. Rewriting Logic as a Framework for Generic Verification Tools. Proceedings of Third International Workshop on Rewriting Logic and Its Applications (WRLA 2000), Elsevier, 2001.

[bibtex]
Theo C. Ruys, Rom Langerak, Joost-Pieter Katoen, Diego Latella, Mieke Massink. First passage time analysis of stochastic process algebra using partial orders. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 220–236, LNCS vol. 2031, Springer-Verlag, 2001.

[bibtex]
Gabriel Infante G. López, Holger Hermanns, Joost-Pieter Katoen. Beyond memoryless distributions: model checking semi-Markov chains. Process Algebra and Probabilistic Methods (PAPM-Probmiv), pages 57–70, LNCS vol. 2165, Springer-Verlag, 2001.

[bibtex]
Joost-Pieter Katoen, Marta Kwiatkowska, Gethin Norman, David Parker. Faster and Symbolic CTMC Model Checking. Process Algebra and Probabilistic Methods (PAPM-Probmiv), pages 23–38, LNCS vol. 2165, Springer-Verlag, 2001.

[bibtex]
Joost-Pieter Katoen, Christel Baier, Diego Latella. Metric semantics for true concurrent real time. Theor. Comput. Sci 254(1-2), pages 501–542, 2001.
Download
[bibtex]
Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen, Ric Klaren. MoDeST: A Modelling language for Stochastic Timed systems. Process Algebra and Probabilistic Methods (PAPM-Probmiv), pages 87–104, LNCS vol. 2165, Springer-Verlag, 2001.

[bibtex]
Ed Brinksma, Holger Hermanns, Joost-Pieter Katoen editors. Lectures on Formal Methods and Performance Analysis. Springer-Verlag, Volume 2090 of LNCS, 2001.

[bibtex]
Holger Hermanns, Joost-Pieter Katoen. Performance analysis := (process algebra + model checking) × Markov chains. In Kim G. Larsen, Mogens Nielsen editors, Concurrency Theory (CONCUR), volume 2154 of Lecture Notes in Computer Science, pages 59–82, 2001.

[bibtex]
Joost-Pieter Katoen, Pedro R. D'Argenio. General distributions in process algebra. In Ed Brinksma, Holger Hermanns, Joost-Pieter Katoen editors, Lectures on Formal Methods and Performance Analysis (FMPA), pages 375–429, 2001.
Link
[bibtex]
Erika Abraham, Ulrich Hannemann, Martin Steffen. Verification of Hybrid Systems: Formalization and Proof Rules in PVS. IEEE Engineering of Complex Computer Systems (ICECCS'01), pages 48–57, IEEE, 2001.
DOI
[bibtex]
Erika Abraham, Ulrich Hannemann, Martin Steffen. Assertion-Based Analysis of Hybrid Systems with PVS. Computer Aided Systems Theory (EUROCAST'01), Volume 2178 of LNCS, pages 94–109, Springer Berlin Heidelberg, 2001.

[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Deductive Verification for Multithreaded Java. 11. Kolloquium Programmiersprachen und Grundlagen der Programmierung, pages 121–126, , 2001.

[bibtex]
Erika Abraham, Frank S. de Boer, Willem-Paul de Roever, Martin Steffen. Proof Outlines for Threads in Java. 11th Kolloquium Programmiersprachen und Grundlagen der Programmierung, , 2001.
2000

[bibtex]
Boudewijn R. Haverkort, Henrik Bohnenkamp, Connie U. Smith editors. Computer Performance Evaluation—Modelling Techniques and Tools (Proceedings TOOLS 2000). Springer Verlag, 2000.

[bibtex]
Thomas Noll, Heiko Vogler. The Universality of Higher-Order Attributed Tree Transducers. Theory of Computing Systems 34, pages 45–75, 2000.

[bibtex]
Thomas Arts, Thomas Noll. Verifying Generic Erlang Client-Server Implementations. Technical report at RWTH Aachen University number 2000-08, 2000.

[bibtex]
Thomas Arts, Thomas Noll. Verifying Generic Erlang Client-Server Implementations. Proceedings of the 12th International Workshop on Implementation of Functional Languages (IFL 2000), pages 387–402, RWTH Aachen University, 2000.

[bibtex]
Martin Leucker, Thomas Noll. Truth – A Real-World Application in Haskell. Proceedings of the 12th International Workshop on Implementation of Functional Languages (IFL 2000), pages 363–380, RWTH Aachen University, 2000.

[bibtex]
Dino Distefano, Joost-Pieter Katoen, Arend Rensink. A temporal logic for object-based systems. Formal Methods for Open Object-based Distributed Systems IV (FMOODS), pages 305–326, IFIP Proceedings vol. 177, Kluwer Academic Publishers, 2000.

[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. On the logical characterisation of performability properties. Automata, Languages and Programming (ICALP), pages 780–792, LNCS vol. 1853, Springer-Verlag, 2000.

[bibtex]
Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle. A Markov chain model checker. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 357–373, LNCS vol. 1785, Springer, 2000.

[bibtex]
Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. The use of model checking techniques for quantitative dependability evaluation. IEEE Symposium on Reliable Distributed Systems (SRDS), pages 228–238, IEEE CS Press, 2000.

[bibtex]
Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle. Towards model checking stochastic process algebra. Integrated Formal Methods (IFM), pages 420–439, LNCS vol. 1945, Springer, 2000.

[bibtex]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Model checking continuous-time Markov chains by transient analysis. Computer-Aided Verification (CAV), pages 358–372, LNCS vol. 1855, Springer, 2000.

[bibtex]
Holger Hermanns, Joost-Pieter Katoen. Automated compositional Markov chain generation for a plain-old telephone system. Science of Computer Programming 36(1), pages 97–127, 2000.

[bibtex]
Joost-Pieter Katoen, Albert Nymeyer. Pattern-matching algorithms based on term rewrite systems. Theor. Comput. Sci 238(1-2), pages 439–464, 2000.

[bibtex]
Dino Distefano, Joost-Pieter Katoen, Arend Rensink. Towards model checking OCL. ECOOP-Workshop on Defining Precise Semantics for UML. Sophia-Antipolis, France, 10 pages, , 2000.
Link
[bibtex]
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.
DOI
[bibtex]
Erika Abraham, Frank S. de Boer. Proof-Outlines for Threads in Java. Concurrency Theory (CONCUR'00), Volume 1877 of LNCS, pages 229–242, Springer Berlin Heidelberg, 2000.

[bibtex]
Jan B. de Meer, Erika Abraham. Formal Methods for Reflective System Specification. Formale Beschreibungstechniken für verteilte Systeme, pages 51–57, Shaker Verlag, 2000.
1999
Link
[bibtex]
Pedro R. D'Argenio. Algebras and Automata for Timed and Stochastic Systems. Phd Thesis at Department of Computer Science, University of Twente, 1999.

[bibtex]
Joost-Pieter Katoen editors. Proceedings of the 5th International AMAST Workshop, ARTS '99. Springer-Verlag, Volume 1601 of Lecture Notes in Computer Science, 1999.

[bibtex]
Boudewijn R. Haverkort, Alexander Bell, Henrik Bohnenkamp. On the efficient sequential and distributed Evaluation of very large stochastic Petri nets. , pages 12–21, , 1999.

[bibtex]
Henrik Bohnenkamp, Boudewijn R. Haverkort. Stochastic event structures for the decomposition of stochastic process algebra models. , pages 25–39, , 1999.

[bibtex]
Henrik Bohnenkamp, Boudewijn R. Haverkort. Semi-Numerical Solution of Stochastic Process Algebra Models. , pages 228–243, , 1999.

[bibtex]
Thomas Noll. Kohärenzeigenschaften in termersetzungsbasierten Modellen für verteilte Systeme (Abstract). 9. Theorietag der GI-Fachgruppe 0.1.5 ``Automaten und Formale Sprachen'', pages 52, University of Kassel, 1999.

[bibtex]
Thomas Noll. On Coherence Properties in Term Rewriting Models of Concurrency. Proceedings of the 10th International Conference on Concurrency Theory (CONCUR 1999), pages 478–493, Springer-Verlag, 1999.

[bibtex]
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.

[bibtex]
Martin Leucker, Thomas Noll. Rapid Prototyping of Specification Language Implementations. Proceedings of the 10th IEEE International Workshop on Rapid System Prototyping (RSP 1999), pages 60–65, IEEE Computer Society Press, 1999.

[bibtex]
Martin Lange, Martin Leucker, Thomas Noll, Stephan Tobies. Truth – A Verification Platform for Concurrent Systems. In Rudolf Berghammer, Yassine Lakhnech editors, Tool Support for System Specification, Development, and Verification, pages 150–159, 1999.
Download
[bibtex]
Christel Baier, Joost-Pieter Katoen, Holger Hermanns. Approximate Symbolic Model Checking of Continuous-Time Markov Chains. Concurrency Theory (CONCUR), volume 1664 of Lecture Notes in Computer Science, pages, pages 146–162, Springer, 1999.

[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen, Ed Brinksma. Specification and analysis of soft real-time systems: quality and quantity. IEEE Real-Time Systems Symposium (RTSS), pages 104–114, IEEE Computer Society Press, 1999.
Download
[bibtex]
Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen. On Generative Parallel Composition. Electronic Notes in Theoretical Computer Science 22, 1999.
1998

[bibtex]
Martin Lange, Martin Leucker, Thomas Noll, Stephan Tobies. Truth – A Verification Platform for Concurrent Systems (extended abstract). Proceedings of Tools 1998, pages 21–26, Christian-Albrechts University of Kiel, 1998.

[bibtex]
Can Adam Albayrak, Thomas Noll. The WHILE Hierarchy of Program Schemes is Infinite. Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS 1998), pages 35–47, Springer-Verlag, 1998.
Download
[bibtex]
Joost-Pieter Katoen, Rom Langerak, Ed Brinksma, Diego Latella, Tommaso Bolognesi. A Consistent Causality-Based View on a Timed Process Algebra Including Urgent Interactions. Formal Methods in System Design 12(2), pages 189–216, 1998.
Download
[bibtex]
Joost-Pieter Katoen, Lennard Lambert. Pomsets for message sequence charts. Formale Beschreibungstechniken für verteilte Systeme (FBT), pages 197–208, Shaker Verlag, 1998.
Download
[bibtex]
Howard Bowman, Joost-Pieter Katoen. A True Concurrency Semantics for ET-LOTOS. International IEEE Conference on Applications of Concurrency to System Design (CSD), pages 228–239, IEEE Computer Society Press, 1998.
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen, Ed Brinksma. An algebraic approach to the specification of stochastic systems (extended abstract). IFIP Working Conference on Programming Concepts and Methods (PROCOMET), pages 126–148, Chapman & Hall, 1998.
Download
[bibtex]
Howard Bowman, Giorgio P. Faconti, Joost-Pieter Katoen, Diego Latella, Mieke Massink. Automatic Verification of a Lip-Synchronisation Protocol Using Uppaal (Extended version). Formal Aspects of Computing 10(5-6), pages 550–575, 1998.
Download
[bibtex]
Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, Diego Latella. Partial-order models for quantitative extensions of LOTOS. Computer Networks & ISDN Systems 30(9-10), pages 925–950, 1998.
Download
[bibtex]
Christel Baier, Joost-Pieter Katoen, Diego Latella. Metric Semantics for True Concurrent Real Time. Automata, Languages, and Programming (ICALP), volume 1443 of Lecture Notes in Computer Science, pages 568–580, Springer, 1998.
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen, Ed Brinksma. General purpose discrete-event simulation using SPADES. 6th International Workshop on Process Algebra and Performance Modelling (PAPM), pages 85–103, CLUT Press, 1998.
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen, Ed Brinksma. A compositional approach to generalised semi-Markov processes. 4th Int. Workshop on Discrete-Event Systems (WODES), pages 391–397, IEE Press, 1998.

[bibtex]
Jörg Bruske, Erika Abraham, Josef Pauli, Gerald Sommer. Head-pose Estimation from Facial Images with Subspace Neural Networks. Neural Network and Brain (ICNN&B'98), pages 528–530, Publishing House of Electronics Industry, 1998.

[bibtex]
Erika Abraham. Bestimmung der Gesichtspose mit künstlichen neuronalen Netzen. Diploma thesis at the Christian-Albrechts-University Kiel, Germany, 1998.
1997
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans. The Bounded Retransmission Protocol Must Be on Time!. 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.
Download
[bibtex]
Rom Langerak, Ed Brinksma, Joost-Pieter Katoen. Causal ambiguity and partial orders in event structures. Concurrency Theory (CONCUR), volume 1243 of Lecture Notes in Computer Science, pages 317–332, Springer, 1997.
Download
[bibtex]
Albert Nymeyer, Joost-Pieter Katoen. Code generation based on formal bottom-up rewrite systems theory and heuristic search. Acta Informatica 34(4), pages 597–635, 1997.
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen, Ed Brinksma. A stochastic automata model and its algebraic approach. 5th International Workshop on Process Algebra and Performance Modelling (PAPM) CTIT Technical Report 97-14, pages 1–16, University of Twente, 1997.

[bibtex]
Jörg Bruske, Erika Abraham, Gerald Sommer. Visuomotorische Koordination eines Roboterarmes mit Kohonen-Karten, Neuronalem Gas und Dynamischen Zellstrukturen - Ein Vergleich. Selbstorganisation von Adaptivem Verhalten (SOAVE'97), Volume of Fortschrittsberichte VDI, Reihe 8, Nr. 663, pages 203–211, VDI Verlag, 1997.
Download
[bibtex]
Albert Nymeyer, Joost-Pieter Katoen. The systematic development of a pattern-matching algorithm using term-rewriting systems. Proc. of Computing: The Australasian Theory Symposium (CATS), , 1997.
1996

[bibtex]
Thomas Noll, Stefan Roßmanith. Parallel Evaluation of LR-Attributed Grammars. Proceedings of the Poster Session of CC 1996, pages 105–112, Linköping University, 1996.
Download
[bibtex]
Jacob Brunekreef, Joost-Pieter Katoen, Ron Koymans, Sjouke Mauw. Design and Analysis of Dynamic Leader Election Protocols in Broadcast Networks. Distributed Computing 9(4), pages 157–171, 1996.
Download
[bibtex]
Joost-Pieter Katoen, Rom Langerak, Diego Latella, Ed Brinksma. On specifying realtime systems in a causality-based setting. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), volume 1135 of Lecture Notes in Computer Science, pages 385–405, Springer, 1996.
Download
[bibtex]
Pedro R. D'Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans. Modelling and verifying a bounded retransmission protocol using Uppaal. COST 247 Int. Workshop on Applied Formal Methods in System Design, pages 114–128, University of Maribor, 1996.
Download
[bibtex]
Joost-Pieter Katoen, Diego Latella, Ed Brinksma, Rom Langerak. Stochastic simulation of event structures. 4th International Workshop on Process Algebra and Performance Modelling (PAPM), pages 21–40, CLUT Press, 1996.
Download
[bibtex]
Albert Nymeyer, Joost-Pieter Katoen, Ymte Westra, Henk Alblas. Code generation = A* + BURS. Compiler Construction (CC), volume 1060 of Lecture Notes in Computer Science, pages 160–177, Springer-Verlag, 1996.
Download
[bibtex]
Joost-Pieter Katoen, Berry Schoenmakers. Systolic arrays for the recognition of permutation-invariant segments. Science of Computer Programming 27(2), pages 119–137, 1996.
Download
[bibtex]
Georgios Karagiannis, Joost-Pieter Katoen, Ignas G.M.M. Niemegeers. B-ISDN to the cell site switch versus B-ISDN to the mobile terminal. IEEE International Conference on Communicating Systems (ICCS), pages 629–633, IEEE Press, 1996.
1995
Download
[bibtex]
Joost-Pieter Katoen. Functional integration of B-ISDN and UMTS. 45th IEEE Vehicular Technology Conference (VTC), pages 163–168, IEEE Press (extended version as Technical Report 95-02, University of Twente), 1995.
Download
[bibtex]
Joost-Pieter Katoen. Causal behaviours and nets. Application and Theory of Petri Nets 1995 (ATPN), volume 935 of Lecture Notes in Computer Science, pages 258–277, Springer, 1995.
Download
[bibtex]
Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, Diego Latella. A stochastic causality-based process algebra. The Computer Journal 38(7), pages 552–565, 1995.
Download
[bibtex]
Marten Sinderen van, Luís Ferreira Pires, Chris A. Vissers, Joost-Pieter Katoen. A design model for open distributed processing systems. Computer Networks & ISDN Systems 27(6), pages 1263–1285, 1995.
1994

[bibtex]
Thomas Noll. On the First-Order Equivalence of Call-by-Name and Call-by-Value. Proceedings of CAAP 1994, pages 246–260, Springer-Verlag, 1994.

[bibtex]
Thomas Noll, Heiko Vogler. Top-Down Parsing with Simultaneous Evaluation of Noncircular Attribute Grammars. Fundamenta Informaticae 20, pages 285–332, 1994.
Download
[bibtex]
Joost-Pieter Katoen, Rom Langerak, Diego Latella, Ed Brinksma. Performance analysis and true concurrency semantics (extended abstract). 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, IMMD, 1994.
Download
[bibtex]
Joost-Pieter Katoen, Rom Langerak, Diego Latella. Modelling systems by probabilistic process algebra: an event structures approach. Formal Description Techniques VI (FORTE), volume C–22 in IFIP Transactions, pages 253–268, North-Holland, 1994.
Download
[bibtex]
Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, Diego Latella. Performance analysis and true concurrency semantics. Theories and Experiences for Real-Time System Development, chapter 12, AMAST Series in Computing 2, pages 309–337, 1994.
Download
[bibtex]
Jacob Brunekreef, Joost-Pieter Katoen, Ron Koymans, Sjouke Mauw. Algebraic specification of dynamic leader election protocols in broadcast networks. Algebra of Communicating Processes (ACP), Workshops in Computing, pages 338–357, Springer-Verlag, 1994.
Download
[bibtex]
Joost-Pieter Katoen, Jeroen van de Lagemaat. Circuit Switching. In , , Samsom BedrijfsInformatie, 1994.
Download
[bibtex]
Joost-Pieter Katoen, Jeroen van de Lagemaat. Packet Switching. In , , Samsom BedrijfsInformatie, 1994.
1993

[bibtex]
Andrea Kindler, Thomas Noll, Bernhard Steffen. Hierarchical Parallelization of Imperative Programs. Proceedings of Euromicro Workshop on Parallel and Distributed Processing, pages 178–184, IEEE Computer Society Press, 1993.
Download
[bibtex]
Joost-Pieter Katoen. A semi-Markov model of a home network access protocol. Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS), vol. 25 of Simulation Series, pages 293–299, SCS, 1993.
Download
[bibtex]
Joost-Pieter Katoen, Martin Rem. Recognizing K-rotated segments. International Journal of High Speed Computing 5(2), pages 293–305, 1993.
1992

[bibtex]
Thomas Noll, Heiko Vogler. Top-Down Parsing with Simultaneous Evaluation of Noncircular Attribute Grammars. Technical report at RWTH Aachen University number 1992-14, 1992.
Download
[bibtex]
Joost-Pieter Katoen, Berry Schoenmakers. A parallel program for recognizing P-invariant segments. Algorithms and Parallel VLSI Architectures II, pages 79–85, North-Holland, 1992.
1989
Download
[bibtex]
Cees Hemerik, Joost-Pieter Katoen. Bottom-up tree acceptors. Science of Computer Programming 13(1), pages 51–72, 1989.