Joost-Pieter Katoen

Photo of Joost-Pieter Katoen

Email: katoen@cs.rwth-aachen.de
Address: Room 4201
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21200

Please visit my personal page in the web

Publications

Own publications

2026

Conference paper
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler
Programming languages and systems
PDF of Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops RWTH record for Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops BibTeX for Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
Conference paper
Caesar: A Deductive Verifier for Probabilistic Programs
Philipp Schroer, Kevin Batz, Umut Yigit Dural, Darion Haase, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Computer Aided Verification
PDF of Caesar: A Deductive Verifier for Probabilistic Programs RWTH record for Caesar: A Deductive Verifier for Probabilistic Programs BibTeX for Caesar: A Deductive Verifier for Probabilistic Programs
Journal article
Search and explore: symbiotic policy synthesis in POMDPs
Roman Andriushchenko, Alexander Nikolai Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Filip Macák
Formal methods in system design
PDF of Search and explore: symbiotic policy synthesis in POMDPs RWTH record for Search and explore: symbiotic policy synthesis in POMDPs BibTeX for Search and explore: symbiotic policy synthesis in POMDPs
Conference paper
Verifying Sampling Algorithms via Distributional Invariants
Daniel Zilken, Kevin Batz, Joost-Pieter Katoen, Tobias Winkler
Formal Methods
PDF of Verifying Sampling Algorithms via Distributional Invariants RWTH record for Verifying Sampling Algorithms via Distributional Invariants BibTeX for Verifying Sampling Algorithms via Distributional Invariants
Journal article
On termination of polynomial programs with equality conditions
Yangjia Li, Mingshuai Chen, Liangran Zhao, Naijun Zhan, Hui Lu, Guohua Wu, Joost-Pieter Katoen
Information and computation
RWTH record for On termination of polynomial programs with equality conditions BibTeX for On termination of polynomial programs with equality conditions
Conference paper
Highly Incremental: A Simple Programmatic Approach for Many Objectives
Philipp Schroer, Joost-Pieter Katoen
Formal Methods
PDF of Highly Incremental: A Simple Programmatic Approach for Many Objectives RWTH record for Highly Incremental: A Simple Programmatic Approach for Many Objectives BibTeX for Highly Incremental: A Simple Programmatic Approach for Many Objectives
Preprint
Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
Philipp Schroer, Joost-Pieter Katoen
PDF of Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)RWTH record for Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)BibTeX for Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
Conference paper
Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
Linus Heck, Tim Quatmann, Jip Josephine Spel, Joost-Pieter Katoen, Sebastian Junges
Automated technology for verification and analysis
RWTH record for Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains BibTeX for Generalized Parameter Lifting: Finer Abstractions for Parametric Markov Chains
Conference paper
Facing Uncertainty in AI: From Formal Verification To Synthesis
Joost-Pieter Katoen
Theoretical Aspects of Computing – ICTAC 2025
RWTH record for Facing Uncertainty in AI: From Formal Verification To Synthesis BibTeX for Facing Uncertainty in AI: From Formal Verification To Synthesis
Book chapter
The Optimal Strategy to Meet the Deadline: Ask Christel!
Joost-Pieter Katoen
Principles of formal quantitative analysis
RWTH record for The Optimal Strategy to Meet the Deadline: Ask Christel!BibTeX for The Optimal Strategy to Meet the Deadline: Ask Christel!
Artifact
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation)
Philipp Schröer, Darion Haase, Joost-Pieter Katoen
Zenodo
RWTH record for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation)BibTeX for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Artifact Evaluation)

2025

Preprint
Compositional Reasoning for Parametric Probabilistic Automata
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
PDF of Compositional Reasoning for Parametric Probabilistic Automata RWTH record for Compositional Reasoning for Parametric Probabilistic Automata BibTeX for Compositional Reasoning for Parametric Probabilistic Automata
Conference paper
Quantifier Elimination and Craig Interpolation: The Quantitative Way
Kevin Batz, Joost-Pieter Katoen, Nora Orhan
Foundations of Software Science and Computation Structures
PDF of Quantifier Elimination and Craig Interpolation: The Quantitative Way RWTH record for Quantifier Elimination and Craig Interpolation: The Quantitative Way BibTeX for Quantifier Elimination and Craig Interpolation: The Quantitative Way
Conference paper
Bayesian Inference in Quantum Programs
Christina Gehnen, Dominique Unruh, Joost-Pieter Katoen
52nd International Colloquium on Automata, Languages, and Programming
PDF of Bayesian Inference in Quantum Programs RWTH record for Bayesian Inference in Quantum Programs BibTeX for Bayesian Inference in Quantum Programs
Preprint
Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
Philipp Schroer, Darion Haase, Joost-Pieter Katoen
PDF of Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)RWTH record for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)BibTeX for Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing (Extended Version)
Conference paper
Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Emma Katharina Ahrens, Jan-Christoph Kassing, Jürgen Giesl, Joost-Pieter Katoen
10th International Conference on Formal Structures for Computation and Deduction
PDF of Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems RWTH record for Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems BibTeX for Weighted Rewriting: Semiring Semantics for Abstract Reduction Systems
Conference paper
A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
Raphael Jean Berthon, Joost-Pieter Katoen, Zihan Zhou
36th International Conference on Concurrency Theory
PDF of A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games RWTH record for A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games BibTeX for A Direct Reduction from Stochastic Parity Games to Simple Stochastic Games
Conference paper
Compositional Reasoning for Parametric Probabilistic Automata
Hannah Mertens, Tim Quatmann, Joost-Pieter Katoen
36th International Conference on Concurrency Theory
PDF of Compositional Reasoning for Parametric Probabilistic Automata RWTH record for Compositional Reasoning for Parametric Probabilistic Automata BibTeX for Compositional Reasoning for Parametric Probabilistic Automata
Conference paper
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Timm Spork, Christel Baier, Joost-Pieter Katoen, Sascha Klüppelholz, Jakob Piribauer
Computer Aided Verification
PDF of Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains RWTH record for Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains BibTeX for Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Conference paper
Multi-Cost-Bounded Reachability Analysis of POMDPs
Alexander Nikolai Bork, Tim Quatmann, Joost-Pieter Katoen, Svenja Maria Stein
Conference on Uncertainty in Artificial Intelligence, 21-25 July 2025, Rio Othon Palace, Rio de Janeiro, Brazil
PDF of Multi-Cost-Bounded Reachability Analysis of POMDPs RWTH record for Multi-Cost-Bounded Reachability Analysis of POMDPs BibTeX for Multi-Cost-Bounded Reachability Analysis of POMDPs
Conference paper
Robust Strategies for Stochastic Multi-Agent Systems
Raphael Jean Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano
Proceedings of AAMAS-2025
PDF of Robust Strategies for Stochastic Multi-Agent Systems RWTH record for Robust Strategies for Stochastic Multi-Agent Systems BibTeX for Robust Strategies for Stochastic Multi-Agent Systems
Journal article
Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler
Journal of automated reasoning
PDF of Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate RWTH record for Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate BibTeX for Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate
Journal article
Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Kevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler
Proceedings of the ACM on programming languages
PDF of Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back RWTH record for Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back BibTeX for Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Journal article
Introduction to the Special Collection from FM 2023
Marsha Chechik, Joost-Pieter Katoen
Formal aspects of computing
RWTH record for Introduction to the Special Collection from FM 2023 BibTeX for Introduction to the Special Collection from FM 2023
Journal article
An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty
Roman Andriushchenko, Milan Češka, Filip Macák, Sebastian Junges, Joost-Pieter Katoen
Journal of artificial intelligence research
PDF of An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty RWTH record for An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty BibTeX for An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty
Book
Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th Birthday
Springer
RWTH record for Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th Birthday BibTeX for Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th Birthday
Book
Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday
Springer
RWTH record for Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday BibTeX for Principles of verification: cycling the probabilistic landscape : essays dedicated to Joost-Pieter Katoen on the occasion of his 60th birthday

2024

Conference paper
A Spectrum of Approximate Probabilistic Bisimulations
Timm Spork, Christel Baier, Joost-Pieter Katoen, Jakob Piribauer, Tim Quatmann
35th International Conference on Concurrency Theory
PDF of A Spectrum of Approximate Probabilistic Bisimulations RWTH record for A Spectrum of Approximate Probabilistic Bisimulations BibTeX for A Spectrum of Approximate Probabilistic Bisimulations
Journal article
A Compositional Semantics of Boolean-Logic Driven Markov Processes
Shahid Khan, Joost-Pieter Katoen, Marc Bouissou
IEEE transactions on dependable and secure computing
RWTH record for A Compositional Semantics of Boolean-Logic Driven Markov Processes BibTeX for A Compositional Semantics of Boolean-Logic Driven Markov Processes
Conference paper
Markov Decision Processes with Sure Parity and Multiple Reachability Objectives
Raphael Jean Berthon, Joost-Pieter Katoen, Tobias Winkler
Reachability problems
RWTH record for Markov Decision Processes with Sure Parity and Multiple Reachability Objectives BibTeX for Markov Decision Processes with Sure Parity and Multiple Reachability Objectives
Preprint
Natural Strategic Ability in Stochastic Multi-Agent Systems
Raphael Jean Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano
PDF of Natural Strategic Ability in Stochastic Multi-Agent Systems RWTH record for Natural Strategic Ability in Stochastic Multi-Agent Systems BibTeX for Natural Strategic Ability in Stochastic Multi-Agent Systems
Conference paper
Natural Strategic Ability in Stochastic Multi-Agent Systems
Raphael Jean Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano
Thirty-Eighth AAAI Conference on Artificial Intelligence
RWTH record for Natural Strategic Ability in Stochastic Multi-Agent Systems BibTeX for Natural Strategic Ability in Stochastic Multi-Agent Systems
Conference paper
Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler
Tools and algorithms for the construction and analysis of systems
PDF of Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains RWTH record for Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains BibTeX for Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains
Conference paper
SAFEST: Fault Tree Analysis Via Probabilistic Model Checking
Matthias Volk, Falak Sher, Joost-Pieter Katoen, Mariëlle Stoelinga
Annual Reliability and Maintainability Symposium 2024 proceedings
RWTH record for SAFEST: Fault Tree Analysis Via Probabilistic Model Checking BibTeX for SAFEST: Fault Tree Analysis Via Probabilistic Model Checking
Journal article
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen
Proceedings of the ACM on programming languages
PDF of Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions RWTH record for Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions BibTeX for Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Journal article
Parameter synthesis for Markov models : covering the parameter space
Sebastian Junges, Erika Ábrahám, Hans Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk
Formal methods in system design
PDF of Parameter synthesis for Markov models : covering the parameter space RWTH record for Parameter synthesis for Markov models : covering the parameter space BibTeX for Parameter synthesis for Markov models : covering the parameter space
Journal article
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler
Proceedings of the ACM on programming languages
PDF of Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs RWTH record for Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs BibTeX for Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Journal article
Stochastic games with lexicographic objectives
Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler
Formal methods in system design
PDF of Stochastic games with lexicographic objectives RWTH record for Stochastic games with lexicographic objectives BibTeX for Stochastic games with lexicographic objectives

2023

Conference paper
Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks
Bahare Salmani Barzoki, Joost-Pieter Katoen
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence
RWTH record for Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks BibTeX for Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks
Proceedings
Formal Methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023 : proceedings
Springer
RWTH record for Formal Methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023 : proceedings BibTeX for Formal Methods : 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023 : proceedings
Preprint
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen
PDF of Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions RWTH record for Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions BibTeX for Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Journal article
Model Checking Temporal Properties of Recursive Probabilistic Programs
Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen
Logical methods in computer science
PDF of Model Checking Temporal Properties of Recursive Probabilistic Programs RWTH record for Model Checking Temporal Properties of Recursive Probabilistic Programs BibTeX for Model Checking Temporal Properties of Recursive Probabilistic Programs
Preprint
A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
PDF of A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)RWTH record for A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)BibTeX for A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)
Journal article
A Deductive Verification Infrastructure for Probabilistic Programs
Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Proceedings of the ACM on programming languages
PDF of A Deductive Verification Infrastructure for Probabilistic Programs RWTH record for A Deductive Verification Infrastructure for Probabilistic Programs BibTeX for A Deductive Verification Infrastructure for Probabilistic Programs
Conference paper
On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata
Tobias Winkler, Joost-Pieter Katoen
2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
RWTH record for On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata BibTeX for On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata
Conference paper
Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
Tobias Winkler, Joost-Pieter Katoen
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration RWTH record for Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration BibTeX for Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration
Journal article
Automatically Finding the Right Probabilities in Bayesian Networks
Bahare Salmani Barzoki, Joost-Pieter Katoen
Journal of artificial intelligence research
PDF of Automatically Finding the Right Probabilities in Bayesian Networks RWTH record for Automatically Finding the Right Probabilities in Bayesian Networks BibTeX for Automatically Finding the Right Probabilities in Bayesian Networks
Conference paper
Search and Explore: Symbiotic Policy Synthesis in POMDPs
Roman Andriushchenko, Alexander Nikolai Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Filip Macák
Computer Aided Verification
PDF of Search and Explore: Symbiotic Policy Synthesis in POMDPs RWTH record for Search and Explore: Symbiotic Policy Synthesis in POMDPs BibTeX for Search and Explore: Symbiotic Policy Synthesis in POMDPs
Journal article
Lower Bounds for Possibly Divergent Probabilistic Programs
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
Proceedings of the ACM on programming languages
PDF of Lower Bounds for Possibly Divergent Probabilistic Programs RWTH record for Lower Bounds for Possibly Divergent Probabilistic Programs BibTeX for Lower Bounds for Possibly Divergent Probabilistic Programs
Conference paper
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants RWTH record for Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants BibTeX for Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Journal article
A Calculus for Amortized Expected Runtimes
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht
Proceedings of the ACM on programming languages
PDF of A Calculus for Amortized Expected Runtimes RWTH record for A Calculus for Amortized Expected Runtimes BibTeX for A Calculus for Amortized Expected Runtimes
Preprint
Exact Probabilistic Inference Using Generating Functions
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen
PDF of Exact Probabilistic Inference Using Generating Functions RWTH record for Exact Probabilistic Inference Using Generating Functions BibTeX for Exact Probabilistic Inference Using Generating Functions

2022

Journal article
The probabilistic termination tool amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
Formal methods in system design
PDF of The probabilistic termination tool amber RWTH record for The probabilistic termination tool amber BibTeX for The probabilistic termination tool amber
Book chapter
Parameter Synthesis in Markov Models: A Gentle Survey
Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
Principles of systems design
RWTH record for Parameter Synthesis in Markov Models: A Gentle Survey BibTeX for Parameter Synthesis in Markov Models: A Gentle Survey
Journal article
Reasoning about distributed reconfigurable systems
Emma Katharina Ahrens, Marius Bozga, Radu Iosif, Joost-Pieter Katoen
Proceedings of the ACM on programming languages
RWTH record for Reasoning about distributed reconfigurable systems BibTeX for Reasoning about distributed reconfigurable systems
Conference paper
BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, Marielle Stoelinga
NASA Formal Methods
RWTH record for BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees BibTeX for BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees
Journal article
Convex Optimization for Parameter Synthesis in MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu
IEEE transactions on automatic control
RWTH record for Convex Optimization for Parameter Synthesis in MDPs BibTeX for Convex Optimization for Parameter Synthesis in MDPs
Journal article
Generative Datalog with Continuous Distributions
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
Journal of the ACM
RWTH record for Generative Datalog with Continuous Distributions BibTeX for Generative Datalog with Continuous Distributions
Journal article
Scenario-based verification of uncertain parametric MDPs
Thom Badings, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu
International journal on software tools for technology transfer
PDF of Scenario-based verification of uncertain parametric MDPs RWTH record for Scenario-based verification of uncertain parametric MDPs BibTeX for Scenario-based verification of uncertain parametric MDPs
Conference paper
POMDP Controllers with Optimal Budget
Jip Josephine Spel, Svenja Maria Stein, Joost-Pieter Katoen
Quantitative evaluation of systems
RWTH record for POMDP Controllers with Optimal Budget BibTeX for POMDP Controllers with Optimal Budget
Journal article
Encoding inductive invariants as barrier certificates : Synthesis via difference-of-convex programming
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
Information and computation
RWTH record for Encoding inductive invariants as barrier certificates : Synthesis via difference-of-convex programming BibTeX for Encoding inductive invariants as barrier certificates : Synthesis via difference-of-convex programming
Technical report
50 Jahre Studiengang Informatik an der RWTH Aachen : Ein Streifzug in Text und Bild
RWTH record for 50 Jahre Studiengang Informatik an der RWTH Aachen : Ein Streifzug in Text und Bild BibTeX for 50 Jahre Studiengang Informatik an der RWTH Aachen : Ein Streifzug in Text und Bild
Preprint
Towards Concurrent Quantitative Separation Logic
Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll
PDF of Towards Concurrent Quantitative Separation Logic RWTH record for Towards Concurrent Quantitative Separation Logic BibTeX for Towards Concurrent Quantitative Separation Logic
Conference paper
Towards Concurrent Quantitative Separation Logic
Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll
33rd International Conference on Concurrency Theory (CONCUR 2022)
PDF of Towards Concurrent Quantitative Separation Logic RWTH record for Towards Concurrent Quantitative Separation Logic BibTeX for Towards Concurrent Quantitative Separation Logic
Conference paper
Configurable Benchmarks for C Model Checkers
Xaver Fink, Philipp Berger, Joost-Pieter Katoen
NASA Formal Methods
RWTH record for Configurable Benchmarks for C Model Checkers BibTeX for Configurable Benchmarks for C Model Checkers
Conference paper
Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler
Computer Aided Verification
PDF of Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions RWTH record for Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions BibTeX for Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions
Journal article
Weighted programming : a programming paradigm for specifying mathematical models
Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler
Proceedings of the ACM on programming languages
PDF of Weighted programming : a programming paradigm for specifying mathematical models RWTH record for Weighted programming : a programming paradigm for specifying mathematical models BibTeX for Weighted programming : a programming paradigm for specifying mathematical models
Conference paper
Under-Approximating Expected Total Rewards in POMDPs
Alexander Nikolai Bork, Joost-Pieter Katoen, Tim Quatmann
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Under-Approximating Expected Total Rewards in POMDPs RWTH record for Under-Approximating Expected Total Rewards in POMDPs BibTeX for Under-Approximating Expected Total Rewards in POMDPs
Journal article
DFT modeling approach for operational risk assessment of railway infrastructure
Norman Weik, Matthias Volk, Joost-Pieter Katoen, Nils Nießen
International journal on software tools for technology transfer
PDF of DFT modeling approach for operational risk assessment of railway infrastructure RWTH record for DFT modeling approach for operational risk assessment of railway infrastructure BibTeX for DFT modeling approach for operational risk assessment of railway infrastructure
Conference paper
Foundations for Entailment Checking in Quantitative Separation Logic
Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll
Programming Languages and Systems
PDF of Foundations for Entailment Checking in Quantitative Separation Logic RWTH record for Foundations for Entailment Checking in Quantitative Separation Logic BibTeX for Foundations for Entailment Checking in Quantitative Separation Logic
Conference paper
Model Checking Temporal Properties of Recursive Probabilistic Programs
Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen
Foundations of Software Science and Computation Structures
PDF of Model Checking Temporal Properties of Recursive Probabilistic Programs RWTH record for Model Checking Temporal Properties of Recursive Probabilistic Programs BibTeX for Model Checking Temporal Properties of Recursive Probabilistic Programs
Conference paper
Gradient-Descent for Randomized Controllers Under Partial Observability
Linus Heck, Jip Josephine Spel, Sebastian Junges, Joshua Moerman, Joost-Pieter Katoen
Verification, Model Checking, and Abstract Interpretation
RWTH record for Gradient-Descent for Randomized Controllers Under Partial Observability BibTeX for Gradient-Descent for Randomized Controllers Under Partial Observability
Conference paper
Out of Control : Reducing Probabilistic Models by Control-State Elimination
Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen
Verification, Model Checking, and Abstract Interpretation
RWTH record for Out of Control : Reducing Probabilistic Models by Control-State Elimination BibTeX for Out of Control : Reducing Probabilistic Models by Control-State Elimination
Book
Nachhaltigen Wandel gestalten : Innovationsimpulse der RWTH
RWTH Aachen. Lehrstuhl für Planungstheorie und Stadtentwicklung, REVIERa – Transformationsplattform der RWTH, Thorsten Karbach, Agnes Förster, Eva Christine Strobel, Stefan Karl Josef Böschen, Peter Letmathe, Elisabeth Clausen, Rik W. de Doncker, Peter Lürkens, Albert Moser, Aaron Jonathan Praktiknjo, Fabian Roemer, Andreas Ulbig, Rainer Dahlmann, Thomas Fischöder, Stefanie Gottuck, Jürgen Klankermeyer, Felix Kunz, Regina Palkovits, Stefan Sterlepper, Peter Quicker, Matthias Jarke, Max C. Lemme, Saskia K. Nagel, Joost-Pieter Katoen, Rainer Waser, Matthias Brockmann, Melanie Sarah Katharina Buchsbaum, Christian Rüdiger Hinke, Patrick Mattfield, Edgar Dahl, Fabian Kiessling, Holger Jahr, Jonas Gesenhues, Joachim Jankowski, Mare Mechelinck, Heidi Noels, Irene Neuner, Rolf Rossaint, Stefan Uhlig, Tanja Veselinović, Emiel Petrus Carla van der Vorst, Maximilian Alfons Voshage, Dirk Abel, Claus Bonerz, Lutz Eckstein, Bastian Lehrheuer, Micha Lesemann, Tobias Ostermann, René Zweigel, Benjamin Daniels, Frank Lehmkuhl, Michael Leuchner, Frank Lohrberg, Henry Riße, Martina Roß-Nickoll, Thomas Josef Wintgens
RWTH Aachen University
PDF of Nachhaltigen Wandel gestalten : Innovationsimpulse der RWTH RWTH record for Nachhaltigen Wandel gestalten : Innovationsimpulse der RWTH BibTeX for Nachhaltigen Wandel gestalten : Innovationsimpulse der RWTH
Journal article
Synthesizing optimal bias in randomized self-stabilization
Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Saba Aflaki
Distributed computing
PDF of Synthesizing optimal bias in randomized self-stabilization RWTH record for Synthesizing optimal bias in randomized self-stabilization BibTeX for Synthesizing optimal bias in randomized self-stabilization
Journal article
The probabilistic model checker STORM
Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk
International journal on software tools for technology transfer
PDF of The probabilistic model checker STORM RWTH record for The probabilistic model checker STORM BibTeX for The probabilistic model checker STORM
Journal article
Markov automata with multiple objectives
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen
Formal methods in system design
RWTH record for Markov automata with multiple objectives BibTeX for Markov automata with multiple objectives

2021

Conference paper
Scalable Reliability Analysis by Lazy Verification
Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Marc Bouissou
NASA formal methods
RWTH record for Scalable Reliability Analysis by Lazy Verification BibTeX for Scalable Reliability Analysis by Lazy Verification
Conference paper
Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees
Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Ahmad Zafar, Falak Sher
2021 10th Latin-American Symposium on Dependable Computing (LADC)
RWTH record for Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees BibTeX for Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees
Conference paper
Synergising Reliability Modelling Languages : BDMPs and Repairable DFTs
Shahid Khan, Joost-Pieter Katoen
2021 IEEE 26th Pacific Rim International Symposium on Dependable Computing
RWTH record for Synergising Reliability Modelling Languages : BDMPs and Repairable DFTs BibTeX for Synergising Reliability Modelling Languages : BDMPs and Repairable DFTs
Conference paper
Automated Termination Analysis of Polynomial Probabilistic Programs
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
Programming languages and systems
RWTH record for Automated Termination Analysis of Polynomial Probabilistic Programs BibTeX for Automated Termination Analysis of Polynomial Probabilistic Programs
Conference paper
The Probabilistic Termination Tool Amber
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács
Formal Methods
RWTH record for The Probabilistic Termination Tool Amber BibTeX for The Probabilistic Termination Tool Amber
Journal article
Probabilistic Data with Continuous Distributions
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
ACM SIGMOD record
RWTH record for Probabilistic Data with Continuous Distributions BibTeX for Probabilistic Data with Continuous Distributions
Conference paper
Model Checking the Multi-Formalism Language FIGARO
Shahid Khan, Matthias Volk, Joost-Pieter Katoen, Alexis Braibant, Marc Bouissou
51st Annual IEEE/IFIP International Conference on Dependable Systems and Networks
RWTH record for Model Checking the Multi-Formalism Language FIGARO BibTeX for Model Checking the Multi-Formalism Language FIGARO
Conference paper
PAYNT : A Tool for Inductive Synthesis of Probabilistic Programs
Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Šimon Stupinský
Computer-Aided Verification
PDF of PAYNT : A Tool for Inductive Synthesis of Probabilistic Programs RWTH record for PAYNT : A Tool for Inductive Synthesis of Probabilistic Programs BibTeX for PAYNT : A Tool for Inductive Synthesis of Probabilistic Programs
Conference paper
Fine-Tuning the Odds in Bayesian Networks
Bahare Salmani Barzoki, Joost-Pieter Katoen
Symbolic and quantitative approaches to reasoning with uncertainty
PDF of Fine-Tuning the Odds in Bayesian Networks RWTH record for Fine-Tuning the Odds in Bayesian Networks BibTeX for Fine-Tuning the Odds in Bayesian Networks
Conference paper
Tweaking the Odds in Probabilistic Timed Automata
Arnd Hartmanns, Joost-Pieter Katoen, Bram Kohlen, Jip Josephine Spel
Quantitative evaluation of systems
RWTH record for Tweaking the Odds in Probabilistic Timed Automata BibTeX for Tweaking the Odds in Probabilistic Timed Automata
Conference paper
Latticed $k$-Induction with an Application to Probabilistic Programs
Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
Computer-Aided Verification
PDF of Latticed $k$-Induction with an Application to Probabilistic Programs RWTH record for Latticed $k$-Induction with an Application to Probabilistic Programs BibTeX for Latticed $k$-Induction with an Application to Probabilistic Programs
Conference paper
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen
Computer-Aided Verification
PDF of Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming RWTH record for Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming BibTeX for Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
Journal article
Counterexample-guided inductive synthesis for probabilistic systems
Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen
Formal aspects of computing
RWTH record for Counterexample-guided inductive synthesis for probabilistic systems BibTeX for Counterexample-guided inductive synthesis for probabilistic systems
Journal article
A pre-expectation calculus for probabilistic sensitivity
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Proceedings of the ACM on programming languages
PDF of A pre-expectation calculus for probabilistic sensitivity RWTH record for A pre-expectation calculus for probabilistic sensitivity BibTeX for A pre-expectation calculus for probabilistic sensitivity
Conference paper
Finding Provably Optimal Markov Chains
Jip Josephine Spel, Sebastian Junges, Joost-Pieter Katoen
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Finding Provably Optimal Markov Chains RWTH record for Finding Provably Optimal Markov Chains BibTeX for Finding Provably Optimal Markov Chains
Conference paper
Multi-objective Optimization of Long-run Average and Total Rewards
Tim Quatmann, Joost-Pieter Katoen
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Multi-objective Optimization of Long-run Average and Total Rewards RWTH record for Multi-objective Optimization of Long-run Average and Total Rewards BibTeX for Multi-objective Optimization of Long-run Average and Total Rewards
Journal article
Relatively complete verification of probabilistic programs : an expressive language for expectation-based reasoning
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Proceedings of the ACM on programming languages
PDF of Relatively complete verification of probabilistic programs : an expressive language for expectation-based reasoning RWTH record for Relatively complete verification of probabilistic programs : an expressive language for expectation-based reasoning BibTeX for Relatively complete verification of probabilistic programs : an expressive language for expectation-based reasoning
Journal article
The complexity of reachability in parametric Markov decision processes
Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, Tobias Winkler
Journal of computer and system sciences
RWTH record for The complexity of reachability in parametric Markov decision processes BibTeX for The complexity of reachability in parametric Markov decision processes
Book
Foundations of probabilistic programming
Cambridge University Press
PDF of Foundations of probabilistic programming RWTH record for Foundations of probabilistic programming BibTeX for Foundations of probabilistic programming
Conference paper
Generating Functions for Probabilistic Programs
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler
Logic-Based Program Synthesis and Transformation
RWTH record for Generating Functions for Probabilistic Programs BibTeX for Generating Functions for Probabilistic Programs
Journal article
Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker
IEEE transactions on automatic control
RWTH record for Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions BibTeX for Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions

2020

Conference paper
Verifying Probabilistic Programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Quantitative Evaluation of Systems
PDF of Verifying Probabilistic Programs RWTH record for Verifying Probabilistic Programs BibTeX for Verifying Probabilistic Programs
Preprint
Various Ways to Quantify BDMPs
Marc Bouissou, Shahid Khan, Joost-Pieter Katoen, Pavel Krcal
PDF of Various Ways to Quantify BDMPs RWTH record for Various Ways to Quantify BDMPs BibTeX for Various Ways to Quantify BDMPs
Conference paper
PrIC3: Property Directed Reachability for MDPs
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer
Computer Aided Verification
PDF of PrIC3: Property Directed Reachability for MDPs RWTH record for PrIC3: Property Directed Reachability for MDPs BibTeX for PrIC3: Property Directed Reachability for MDPs
Conference paper
Verification of Indefinite-Horizon POMDPs
Alexander Nikolai Bork, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann
Automated technology for verification and analysis
RWTH record for Verification of Indefinite-Horizon POMDPs BibTeX for Verification of Indefinite-Horizon POMDPs
Conference paper
A Compositional Semantics for Repairable BDMPs
Shahid Khan, Joost-Pieter Katoen, Marc Bouissou
Computer safety, reliability, and security
RWTH record for A Compositional Semantics for Repairable BDMPs BibTeX for A Compositional Semantics for Repairable BDMPs
Conference paper
Explaining Boolean-Logic Driven Markov Processes using GSPNs
Shahid Khan, Joost-Pieter Katoen, Marc Bouissou
16th European Dependable Computing Conference
RWTH record for Explaining Boolean-Logic Driven Markov Processes using GSPNs BibTeX for Explaining Boolean-Logic Driven Markov Processes using GSPNs
Conference paper
Benchmarking Software Model Checkers on Automotive Code
Lukas Westhofen, Philipp Berger, Joost-Pieter Katoen
NASA formal methods
RWTH record for Benchmarking Software Model Checkers on Automotive Code BibTeX for Benchmarking Software Model Checkers on Automotive Code
Conference paper
Interpretation-Based Violation Witness Validation for C : NITWIT
Jan Švejda, Philipp Berger, Joost-Pieter Katoen
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Interpretation-Based Violation Witness Validation for C : NITWIT RWTH record for Interpretation-Based Violation Witness Validation for C : NITWIT BibTeX for Interpretation-Based Violation Witness Validation for C : NITWIT
Conference paper
Bayesian Inference by Symbolic Model Checking
Bahare Salmani Barzoki, Joost-Pieter Katoen
Quantitative Evaluation of Systems
PDF of Bayesian Inference by Symbolic Model Checking RWTH record for Bayesian Inference by Symbolic Model Checking BibTeX for Bayesian Inference by Symbolic Model Checking
Conference paper
Probabilistic Model Checking of AODV
Mojgan Kamali, Joost-Pieter Katoen
Quantitative Evaluation of Systems
RWTH record for Probabilistic Model Checking of AODV BibTeX for Probabilistic Model Checking of AODV
Conference paper
Weakest Preexpectation Semantics for Bayesian Inference : Conditioning, Continuous Distributions and Divergence
Marcin Szymczak, Joost-Pieter Katoen
Engineering trustworthy software systems
RWTH record for Weakest Preexpectation Semantics for Bayesian Inference : Conditioning, Continuous Distributions and Divergence BibTeX for Weakest Preexpectation Semantics for Bayesian Inference : Conditioning, Continuous Distributions and Divergence
Technical report
UnRAVeL Research Training Group : Uncertainty and Randomness in Algorithms, Verification, and Logic
Joost-Pieter Katoen, Martin Ritzert, Richard Marlon Wilke, Katrin M. Dannert, Peter Lindner, Dennis Fischer, Janosch Fuchs, Björn Frederik Tauer, Vipin Ravindran Vijayalakshmi, Laura Vargas Koch, Nadine Friesen, Andreas Gabriel Klinger, Marcel Tobias Hark, Benjamin Lucien Kaminski, Sebastian Junges, Jip Josephine Spel, Anton Pirogov, Stefan Schupp, Till Hofmann, Daxin Liu, Martin Comis, Tabea Claudia Krabs, Stephan Zieger, Rebecca Haehn, Matthias Volk, Norman Weik, Helene-Maria Bolke-Hermanns
RWTH record for UnRAVeL Research Training Group : Uncertainty and Randomness in Algorithms, Verification, and Logic BibTeX for UnRAVeL Research Training Group : Uncertainty and Randomness in Algorithms, Verification, and Logic
Preprint
Relatively Complete Verification of Probabilistic Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
PDF of Relatively Complete Verification of Probabilistic Programs RWTH record for Relatively Complete Verification of Probabilistic Programs BibTeX for Relatively Complete Verification of Probabilistic Programs
Preprint
Generating Functions for Probabilistic Programs
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler
PDF of Generating Functions for Probabilistic Programs RWTH record for Generating Functions for Probabilistic Programs BibTeX for Generating Functions for Probabilistic Programs
Conference paper
Various Ways to Quantify BDMPs
Marc Bouissou, Shahid Khan, Joost-Pieter Katoen, Pavel Krcal
[The 4th Workshop on Models for Formal Analysis of Real Systems, MARS 2020, Dublin, Ireland]
PDF of Various Ways to Quantify BDMPs RWTH record for Various Ways to Quantify BDMPs BibTeX for Various Ways to Quantify BDMPs
Conference paper
Stochastic Games with Lexicographic Reachability-Safety Objectives
Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler
Computer Aided Verification
PDF of Stochastic Games with Lexicographic Reachability-Safety Objectives RWTH record for Stochastic Games with Lexicographic Reachability-Safety Objectives BibTeX for Stochastic Games with Lexicographic Reachability-Safety Objectives
Journal article
Multi-cost Bounded Tradeoff Analysis in MDP
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann
Journal of automated reasoning
PDF of Multi-cost Bounded Tradeoff Analysis in MDP RWTH record for Multi-cost Bounded Tradeoff Analysis in MDP BibTeX for Multi-cost Bounded Tradeoff Analysis in MDP
Conference paper
Generative Datalog with Continuous Distributions
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner
PODS'20
RWTH record for Generative Datalog with Continuous Distributions BibTeX for Generative Datalog with Continuous Distributions
Conference paper
Scenario-Based Verification of Uncertain MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu
Tools and Algorithms for the Construction and Analysis of Systems
RWTH record for Scenario-Based Verification of Uncertain MDPs BibTeX for Scenario-Based Verification of Uncertain MDPs
Journal article
Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
Christel Baier, Hans Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein
Information and computation
RWTH record for Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination BibTeX for Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination
Conference paper
Simple Strategies in Multi-Objective MDPs
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Simple Strategies in Multi-Objective MDPs RWTH record for Simple Strategies in Multi-Objective MDPs BibTeX for Simple Strategies in Multi-Objective MDPs
Preprint
PrIC3: Property Directed Reachability for MDPs
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer
PDF of PrIC3: Property Directed Reachability for MDPs RWTH record for PrIC3: Property Directed Reachability for MDPs BibTeX for PrIC3: Property Directed Reachability for MDPs
Journal article
Aiming low is harder: induction for lower bounds in probabilistic program verification
Marcel Tobias Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen
Proceedings of the ACM on programming languages
RWTH record for Aiming low is harder: induction for lower bounds in probabilistic program verification BibTeX for Aiming low is harder: induction for lower bounds in probabilistic program verification
Journal article
IC3 software model checking
Tim Felix Lange, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen
International journal on software tools for technology transfer
RWTH record for IC3 software model checking BibTeX for IC3 software model checking

2019

Conference paper
COMPASS 3.0
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
Tools and algorithms for the construction and analysis of systems
PDF of COMPASS 3.0 RWTH record for COMPASS 3.0 BibTeX for COMPASS 3.0
Conference paper
Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs
Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Marc Bouissou
2019 IEEE 24th Pacific Rim International Symposium on Dependable Computing
RWTH record for Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs BibTeX for Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs
Conference paper
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen
Formal methods - the next 30 years
RWTH record for Counterexample-Driven Synthesis for Probabilistic Program Sketches BibTeX for Counterexample-Driven Synthesis for Probabilistic Program Sketches
Proceedings
Dependable software engineering: theories, tools, and applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019 : proceedings
Springer International Publishing
RWTH record for Dependable software engineering: theories, tools, and applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019 : proceedings BibTeX for Dependable software engineering: theories, tools, and applications : 5th International Symposium, SETTA 2019, Shanghai, China, November 27-29, 2019 : proceedings
Conference paper
Shepherding Hordes of Markov Chains
Milan Češka, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Shepherding Hordes of Markov Chains RWTH record for Shepherding Hordes of Markov Chains BibTeX for Shepherding Hordes of Markov Chains
Conference paper
Are Parametric Markov Chains Monotonic?
Jip Josephine Spel, Sebastian Junges, Joost-Pieter Katoen
Automated technology for verification and analysis
RWTH record for Are Parametric Markov Chains Monotonic?BibTeX for Are Parametric Markov Chains Monotonic?
Conference paper
On the Complexity of Reachability in Parametric Markov Decision Processes
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, Joost-Pieter Katoen
30th International Conference on Concurrency Theory
PDF of On the Complexity of Reachability in Parametric Markov Decision Processes RWTH record for On the Complexity of Reachability in Parametric Markov Decision Processes BibTeX for On the Complexity of Reachability in Parametric Markov Decision Processes
Journal article
Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
Mingzhang Huang, Hongfei Fu, Joost-Pieter Katoen
Information and computation
RWTH record for Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems BibTeX for Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems
Book chapter
Model Repair Revamped
Milan Češka, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
From Reactive Systems to Cyber-Physical Systems
RWTH record for Model Repair Revamped BibTeX for Model Repair Revamped
Book chapter
The 10,000 Facets of MDP Model Checking
Christel Baier, Holger Hermanns, Joost-Pieter Katoen
Computing and software science
RWTH record for The 10,000 Facets of MDP Model Checking BibTeX for The 10,000 Facets of MDP Model Checking
Proceedings
44th International Symposium on Mathematical Foundations of Computer Science : MFCS 2019, August 26-30, 2019, Aachen, Germany
Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing
PDF of 44th International Symposium on Mathematical Foundations of Computer Science : MFCS 2019, August 26-30, 2019, Aachen, Germany RWTH record for 44th International Symposium on Mathematical Foundations of Computer Science : MFCS 2019, August 26-30, 2019, Aachen, Germany BibTeX for 44th International Symposium on Mathematical Foundations of Computer Science : MFCS 2019, August 26-30, 2019, Aachen, Germany
Conference paper
Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development
Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow
Formal methods for industrial critical systems ; 24th international conference, FMICS 2019, Amsterdam, The Netherlands, August 30-31, 2019
RWTH record for Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development BibTeX for Multiple Analyses, Requirements Once : Simplifying Testing and Verification in Automotive Model-Based Development
Conference paper
Formal Verification of Rewriting Rules for Dynamic Fault Trees
Yassmeen Elderhalli, Matthias Volk, Osman Hasan, Joost-Pieter Katoen, Sofiène Tahar
Software Engineering and Formal Methods
RWTH record for Formal Verification of Rewriting Rules for Dynamic Fault Trees BibTeX for Formal Verification of Rewriting Rules for Dynamic Fault Trees
Conference paper
A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas
Matthias Volk, Norman Weik, Joost-Pieter Katoen, Nils Nießen
Formal methods for industrial critical systems ; 24th international conference, FMICS 2019, Amsterdam, The Netherlands, August 30-31, 2019
RWTH record for A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas BibTeX for A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas
Conference paper
Correct-by-construction policies for POMDPs
Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer
Proceedings of the Fifth International Workshop on Symbolic-Numeric methods for Reasoning about CPS and IoT
RWTH record for Correct-by-construction policies for POMDPs BibTeX for Correct-by-construction policies for POMDPs
Journal article
Safety analysis for vehicle guidance systems with dynamic fault trees
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk
Reliability engineering & system safety
RWTH record for Safety analysis for vehicle guidance systems with dynamic fault trees BibTeX for Safety analysis for vehicle guidance systems with dynamic fault trees
Journal article
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
Proceedings of the ACM on programming languages
PDF of Quantitative separation logic: a logic for reasoning about probabilistic pointer programs RWTH record for Quantitative separation logic: a logic for reasoning about probabilistic pointer programs BibTeX for Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
Journal article
On the hardness of analyzing probabilistic programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Acta informatica
RWTH record for On the hardness of analyzing probabilistic programs BibTeX for On the hardness of analyzing probabilistic programs

2018

Conference paper
Finite-State Controllers of POMDPs using Parameter Synthesis
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker
34th Conference on Uncertainty in Artificial Intelligence 2018
RWTH record for Finite-State Controllers of POMDPs using Parameter Synthesis BibTeX for Finite-State Controllers of POMDPs using Parameter Synthesis
Conference paper
Parameter-Independent Strategies for pMDPs via POMDPs
Sebastian Arming, Ezio Bartocci, Krishnendu Chatterjee, Joost-Pieter Katoen, Ana Sokolova
Quantitative evaluation of systems
RWTH record for Parameter-Independent Strategies for pMDPs via POMDPs BibTeX for Parameter-Independent Strategies for pMDPs via POMDPs
Conference paper
Finite-State Controllers of POMDPs using Parameter Synthesis
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker
Uncertainty in Artificial Intelligence
PDF of Finite-State Controllers of POMDPs using Parameter Synthesis RWTH record for Finite-State Controllers of POMDPs using Parameter Synthesis BibTeX for Finite-State Controllers of POMDPs using Parameter Synthesis
Conference paper
Model Checking for Safe Navigation Among Humans
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe
Quantitative evaluation of systems
RWTH record for Model Checking for Safe Navigation Among Humans BibTeX for Model Checking for Safe Navigation Among Humans
Conference paper
Synthesis in pMDPs : A Tale of 1001 Parameters
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu
Automated Technology for Verification and Analysis
RWTH record for Synthesis in pMDPs : A Tale of 1001 Parameters BibTeX for Synthesis in pMDPs : A Tale of 1001 Parameters
Conference paper
Rule-Based Conditioning of Probabilistic Data
Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen
Scalable Uncertainty Management
RWTH record for Rule-Based Conditioning of Probabilistic Data BibTeX for Rule-Based Conditioning of Probabilistic Data
Conference paper
Improving Generalization in Software IC3
Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen
Model checking software
RWTH record for Improving Generalization in Software IC3 BibTeX for Improving Generalization in Software IC3
Conference paper
Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen
Formal Methods
RWTH record for Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations BibTeX for Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations
Conference paper
Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain
Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow
Formal Methods
RWTH record for Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain BibTeX for Verifying Auto-generated C Code from Simulink : An Experience Report in the Automotive Domain
Conference paper
Sound Value Iteration
Tim Quatmann, Joost-Pieter Katoen
Computer Aided Verification
PDF of Sound Value Iteration RWTH record for Sound Value Iteration BibTeX for Sound Value Iteration
Conference paper
Monitoring CTMCs by Multi-clock Timed Automata
Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan
Computer Aided Verification
PDF of Monitoring CTMCs by Multi-clock Timed Automata RWTH record for Monitoring CTMCs by Multi-clock Timed Automata BibTeX for Monitoring CTMCs by Multi-clock Timed Automata
Journal article
Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
Journal of the ACM
RWTH record for Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms BibTeX for Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms
Conference paper
Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs
Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
Computer Aided Verification
RWTH record for Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs BibTeX for Let this Graph Be Your Witness! : An Attestor for Verifying Java Pointer Programs
Conference paper
Branching Bisimulation and Concurrent Object Verification
Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, Hao Wu
48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks
RWTH record for Branching Bisimulation and Concurrent Object Verification BibTeX for Branching Bisimulation and Concurrent Object Verification
Preprint
Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
PDF of Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs RWTH record for Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs BibTeX for Quantitative Separation Logic : A Logic for Reasoning about Probabilistic Programs
Conference paper
One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs
Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk
Application and theory of petri nets and concurrency
RWTH record for One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs BibTeX for One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs
Conference paper
How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling times
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Programming Languages and Systems
PDF of How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling times RWTH record for How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling times BibTeX for How long, O Bayesian network, will I sample thee? : A program analysis perspective on expected sampling times
Journal article
A new proof rule for almost-sure termination
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen
Proceedings of the ACM on Programming Languages
RWTH record for A new proof rule for almost-sure termination BibTeX for A new proof rule for almost-sure termination
Conference paper
Multi-cost Bounded Reachability in MDP
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann
Tools and Algorithms for the Construction and Analysis of Systems
PDF of Multi-cost Bounded Reachability in MDP RWTH record for Multi-cost Bounded Reachability in MDP BibTeX for Multi-cost Bounded Reachability in MDP
Journal article
Fast Dynamic Fault Tree Analysis by Model Checking Techniques
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen
IEEE transactions on industrial informatics
RWTH record for Fast Dynamic Fault Tree Analysis by Model Checking Techniques BibTeX for Fast Dynamic Fault Tree Analysis by Model Checking Techniques
Journal article
Conditioning in Probabilistic Programming
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle Mciver
ACM transactions on programming languages and systems
RWTH record for Conditioning in Probabilistic Programming BibTeX for Conditioning in Probabilistic Programming

2017

Book chapter
Synthesis and Verification of Self-aware Computing Systems
Radu Calinescu, Marco Autili, Javier Ciamara, Antinisca Di Marco, Simos Gerasimou, Paola Inverardi, Alexander Perucci, Nils Jansen, Joost-Pieter Katoen, Marta Kwiatkowska, Ole J. Mengshoel, Romina Spalazzese, Massimo Tivoli
Self-Aware Computing Systems
RWTH record for Synthesis and Verification of Self-aware Computing Systems BibTeX for Synthesis and Verification of Self-aware Computing Systems
Conference paper
Formal Methods for Aerospace Systems : Achievements and Challenges
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
Cyber-Physical System Design from an Architecture Analysis Viewpoint
RWTH record for Formal Methods for Aerospace Systems : Achievements and Challenges BibTeX for Formal Methods for Aerospace Systems : Achievements and Challenges
Book
ModelEd, TestEd, TrustEd : essays dedicated to Ed Brinksma on the occassion of his 60th birthday
Joost-Pieter Katoen, Rom Langerak, Arend Rensink
Springer
RWTH record for ModelEd, TestEd, TrustEd : essays dedicated to Ed Brinksma on the occassion of his 60th birthday BibTeX for ModelEd, TestEd, TrustEd : essays dedicated to Ed Brinksma on the occassion of his 60th birthday
Conference paper
Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract)
Joost-Pieter Katoen
Theoretical Aspects of Computing - ICTAC 2017
RWTH record for Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract)BibTeX for Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract)
Book chapter
Boosting Fault Tree Analysis by Formal Methods
Joost-Pieter Katoen, Marielle Stoelinga
ModelEd, TestEd, TrustEd
RWTH record for Boosting Fault Tree Analysis by Formal Methods BibTeX for Boosting Fault Tree Analysis by Formal Methods
Conference paper
Modal Stochastic Games : Abstraction-Refinement of Probabilistic Automata
Joost-Pieter Katoen, Falak Sher
Models, algorithms, logics and tools
RWTH record for Modal Stochastic Games : Abstraction-Refinement of Probabilistic Automata BibTeX for Modal Stochastic Games : Abstraction-Refinement of Probabilistic Automata
Conference paper
Motion planning under partial observability using game-based abstraction
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker
2017 IEEE 56th Annual Conference on Decision and Control (CDC)
RWTH record for Motion planning under partial observability using game-based abstraction BibTeX for Motion planning under partial observability using game-based abstraction
Conference paper
Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms
Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Arne Storjohann
2017 IEEE 36th International Symposium on Reliable Distributed Systems
RWTH record for Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms BibTeX for Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms
Conference paper
Model-based Safety Analysis for Vehicle Guidance Systems
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk
Computer safety, reliability, and security
RWTH record for Model-based Safety Analysis for Vehicle Guidance Systems BibTeX for Model-based Safety Analysis for Vehicle Guidance Systems
Conference paper
The COMPASS 3.0 Toolset
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
RWTH record for The COMPASS 3.0 Toolset BibTeX for The COMPASS 3.0 Toolset
Conference paper
Markov Automata with Multiple Objectives
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen
Computer aided verification
RWTH record for Markov Automata with Multiple Objectives BibTeX for Markov Automata with Multiple Objectives
Conference paper
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu
Tools and algorithms for the construction and analysis of systems
RWTH record for Sequential Convex Programming for the Efficient Verification of Parametric MDPs BibTeX for Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Conference paper
A Storm is Coming: A Modern Probabilistic Model Checker
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk
Computer aided verification
RWTH record for A Storm is Coming: A Modern Probabilistic Model Checker BibTeX for A Storm is Coming: A Modern Probabilistic Model Checker
Journal article
Missie: foutvrije software in de ruimte
Harold Yorick Bruintjes, Joost-Pieter Katoen
Bits en Chips
RWTH record for Missie: foutvrije software in de ruimte BibTeX for Missie: foutvrije software in de ruimte
Preprint
A storm is Coming: A Modern Probabilistic Model Checker
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk
PDF of A storm is Coming: A Modern Probabilistic Model Checker RWTH record for A storm is Coming: A Modern Probabilistic Model Checker BibTeX for A storm is Coming: A Modern Probabilistic Model Checker
Conference paper
A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations
Benjamin Lucien Kaminski, Joost-Pieter Katoen
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
RWTH record for A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations BibTeX for A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations
Journal article
Fault trees on a diet: automated reduction by graph rewriting
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga
Formal aspects of computing
RWTH record for Fault trees on a diet: automated reduction by graph rewriting BibTeX for Fault trees on a diet: automated reduction by graph rewriting
Journal article
Quantitative model-checking of controlled discrete-time Markov processes
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate
Information and Computation
RWTH record for Quantitative model-checking of controlled discrete-time Markov processes BibTeX for Quantitative model-checking of controlled discrete-time Markov processes

2016

Conference paper
Probabilistic Verification for Cognitive Models
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu
[Cross-Disciplinary Challenges for Autonomous Systems
RWTH record for Probabilistic Verification for Cognitive Models BibTeX for Probabilistic Verification for Cognitive Models
Conference paper
Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen
Computer safety, reliability, and security
RWTH record for Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates BibTeX for Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates
Conference paper
Uncovering Dynamic Fault Trees
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga
DSN 2016
RWTH record for Uncovering Dynamic Fault Trees BibTeX for Uncovering Dynamic Fault Trees
Conference paper
Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo Beron
Programming languages and systems
RWTH record for Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs BibTeX for Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs
Conference paper
Safety-constrained Reinforcement Learning for MDPs
Sebastian Junges, Nils Jansen, Hans Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen
Tools and algorithms for the construction and analysis of systems
RWTH record for Safety-constrained Reinforcement Learning for MDPs BibTeX for Safety-constrained Reinforcement Learning for MDPs
Conference paper
On the Semantic Intricacies of Conditioning
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo Beron
[1st Workshop on Probabilistic Programming Semantics, PPS 2016, 20.01.2016-23.01.2016, St. Petersburg, Florida, USA
PDF of On the Semantic Intricacies of Conditioning RWTH record for On the Semantic Intricacies of Conditioning BibTeX for On the Semantic Intricacies of Conditioning
Journal article
Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow
Joost-Pieter Katoen, Hao Wu
ACM Transactions on Embedded Computing Systems
RWTH record for Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow BibTeX for Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow
Conference paper
Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks
Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, James Gross
2016 IEEE 35th Symposium on Reliable Distributed Systems (SRDS 2016)
RWTH record for Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks BibTeX for Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks
Journal article
Confluence reduction for Markov automata
Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Mariëlle Stoelinga
Theoretical computer science
RWTH record for Confluence reduction for Markov automata BibTeX for Confluence reduction for Markov automata
Conference paper
Parameter synthesis for probabilistic systems
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám
MBMV 2016
PDF of Parameter synthesis for probabilistic systems RWTH record for Parameter synthesis for probabilistic systems BibTeX for Parameter synthesis for probabilistic systems
Conference paper
Bounded Model Checking for Probabilistic Programs
Nils Jansen, Hans Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen
Automated Technology for Verification and Analysis
RWTH record for Bounded Model Checking for Probabilistic Programs BibTeX for Bounded Model Checking for Probabilistic Programs
Conference paper
Parameter Synthesis for Markov Models: Faster Than Ever
Tim Quatmann, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen
Automated Technology for Verification and Analysis
RWTH record for Parameter Synthesis for Markov Models: Faster Than Ever BibTeX for Parameter Synthesis for Markov Models: Faster Than Ever
Conference paper
Performance Evaluation of Concurrent Data Structures
Hao Wu, Xiaoxiao Yang, Joost-Pieter Katoen
Dependable software engineering
RWTH record for Performance Evaluation of Concurrent Data Structures BibTeX for Performance Evaluation of Concurrent Data Structures
Conference paper
Inferring Covariances for Probabilistic Programs
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Quantitative evaluation of systems
RWTH record for Inferring Covariances for Probabilistic Programs BibTeX for Inferring Covariances for Probabilistic Programs
Conference paper
Reasoning about Recursive Probabilistic Programs
Federico Olmedo Beron, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)
RWTH record for Reasoning about Recursive Probabilistic Programs BibTeX for Reasoning about Recursive Probabilistic Programs
Conference paper
On the Satisfiability of Some Simple Probabilistic Logics
Souymodip Chakraborty, Joost-Pieter Katoen
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)
RWTH record for On the Satisfiability of Some Simple Probabilistic Logics BibTeX for On the Satisfiability of Some Simple Probabilistic Logics
Conference paper
The Probabilistic Model Checking Landscape
Joost-Pieter Katoen
Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS 2016)
RWTH record for The Probabilistic Model Checking Landscape BibTeX for The Probabilistic Model Checking Landscape
Journal article
Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components
Anton Wijs, Joost-Pieter Katoen, Dragan Bošnački
Formal methods in system design
PDF of Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components RWTH record for Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components BibTeX for Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components

2015

Conference paper
Probabilistic Programs - A Natural Model for Approximate Computations
Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo
[Workshop on Approximate Computing, AC15, 2015-10-15 - 2015-10-16, Paderborn, Germany]
RWTH record for Probabilistic Programs - A Natural Model for Approximate Computations BibTeX for Probabilistic Programs - A Natural Model for Approximate Computations
Conference paper
P-Automata for Markov Decision Processes
Souymodip Chakraborty, Joost-Pieter Katoen
[3rd International Workshop on Strategic Reasoning. J. Gutierrez, F. Mogavero, A. Murano, and M. Wooldridge (Eds.)]
RWTH record for P-Automata for Markov Decision Processes BibTeX for P-Automata for Markov Decision Processes
Conference paper
Compositional Analysis Using Component-Oriented Interpolation
Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, Thomas Noll
Formal aspects of component software
RWTH record for Compositional Analysis Using Component-Oriented Interpolation BibTeX for Compositional Analysis Using Component-Oriented Interpolation
Conference paper
Understanding Probabilistic Programs
Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo Beron
Correct system design
RWTH record for Understanding Probabilistic Programs BibTeX for Understanding Probabilistic Programs
Journal article
Juggrnaut: using graph grammars for abstracting unbounded heap structures
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll
Formal methods in system design
RWTH record for Juggrnaut: using graph grammars for abstracting unbounded heap structures BibTeX for Juggrnaut: using graph grammars for abstracting unbounded heap structures
Conference paper
Fault Trees on a Diet
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga
Dependable Software Engineering: Theories, Tools, and Applications
RWTH record for Fault Trees on a Diet BibTeX for Fault Trees on a Diet
Conference paper
On the Hardness of Almost–Sure Termination
Benjamin Lucien Kaminski, Joost-Pieter Katoen
Mathematical foundations of computer science 2015
RWTH record for On the Hardness of Almost–Sure Termination BibTeX for On the Hardness of Almost–Sure Termination
Conference paper
Probabilistic Programming: A True Verification Challenge
Joost-Pieter Katoen
Automated Technology for Verification and Analysis
RWTH record for Probabilistic Programming: A True Verification Challenge BibTeX for Probabilistic Programming: A True Verification Challenge
Journal article
Conditioning in Probabilistic Programming
Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver
Electronic notes in theoretical computer science
PDF of Conditioning in Probabilistic Programming RWTH record for Conditioning in Probabilistic Programming BibTeX for Conditioning in Probabilistic Programming
Conference paper
A Statistical Approach for Timed Reachability in AADL Models
Harold Yorick Bruintjes, Joost-Pieter Katoen, David Lesens
2015 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2015)
RWTH record for A Statistical Approach for Timed Reachability in AADL Models BibTeX for A Statistical Approach for Timed Reachability in AADL Models
Conference paper
PROPhESY : A PRObabilistic ParamEter SYnthesis Tool
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám
Computer aided verification
RWTH record for PROPhESY : A PRObabilistic ParamEter SYnthesis Tool BibTeX for PROPhESY : A PRObabilistic ParamEter SYnthesis Tool
Conference paper
A Greedy Approach for the Efficient Repair of Stochastic Models
Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen
NASA Formal Methods
RWTH record for A Greedy Approach for the Efficient Repair of Stochastic Models BibTeX for A Greedy Approach for the Efficient Repair of Stochastic Models
Conference paper
Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems
Martin Fränzle, Sebastian Gerwinn, Paul Kröger, Alessandro Abate, Joost-Pieter Katoen
Formal modeling and analysis of timed systems
RWTH record for Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems BibTeX for Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems
Conference paper
Model Checking of Open Interval Markov Chains
Souymodip Chakraborty, Joost-Pieter Katoen
Analytical and stochastic modelling techniques and applications
RWTH record for Model Checking of Open Interval Markov Chains BibTeX for Model Checking of Open Interval Markov Chains
Conference paper
Counterexamples for Expected Rewards
Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
FM 2015: formal methods
RWTH record for Counterexamples for Expected Rewards BibTeX for Counterexamples for Expected Rewards
Journal article
High-level Counterexamples for Probabilistic Automata
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen
Logical methods in computer science
PDF of High-level Counterexamples for Probabilistic Automata RWTH record for High-level Counterexamples for Probabilistic Automata BibTeX for High-level Counterexamples for Probabilistic Automata
Journal article
Modelling and statistical model checking of a microgrid
Souymodip Chakraborty, Joost-Pieter Katoen, Falak Sher, Martin Strelec
International journal on software tools for technology transfer
RWTH record for Modelling and statistical model checking of a microgrid BibTeX for Modelling and statistical model checking of a microgrid
Journal article
Verifying pointer programs using graph grammars
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll
Science of computer programming
RWTH record for Verifying pointer programs using graph grammars BibTeX for Verifying pointer programs using graph grammars

2014

Conference paper
Accelerating Parametric Probabilistic Verification
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Quantitative evaluation of systems
RWTH record for Accelerating Parametric Probabilistic Verification BibTeX for Accelerating Parametric Probabilistic Verification
Book chapter
Formal Validation Methods in Model-Based Spacecraft Systems Engineering
Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll
Modeling and simulation-based systems engineering handbook
RWTH record for Formal Validation Methods in Model-Based Spacecraft Systems Engineering BibTeX for Formal Validation Methods in Model-Based Spacecraft Systems Engineering
Journal article
Analysis of Timed and Long-Run Objectives in Markov Automata
Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer
Logical methods in computer science
RWTH record for Analysis of Timed and Long-Run Objectives in Markov Automata BibTeX for Analysis of Timed and Long-Run Objectives in Markov Automata
Conference paper
GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
Anton J. Wijs, Joost-Pieter Katoen, Dragan Bosnacki
Computer aided verification
RWTH record for GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components BibTeX for GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components
Conference paper
Layered Reduction for Modal Specification Theories
Arpit Sharma, Joost-Pieter Katoen
Formal aspects of component software
RWTH record for Layered Reduction for Modal Specification Theories BibTeX for Layered Reduction for Modal Specification Theories
Conference paper
Tight Game Abstractions of Probabilistic Automata
Falak Sher Vira, Joost-Pieter Katoen
CONCUR 2014 - concurrency theory
RWTH record for Tight Game Abstractions of Probabilistic Automata BibTeX for Tight Game Abstractions of Probabilistic Automata
Conference paper
Layered Reduction for Abstract Probabilistic Automata
Arpit Sharma, Joost-Pieter Katoen
ACSD 2014
RWTH record for Layered Reduction for Abstract Probabilistic Automata BibTeX for Layered Reduction for Abstract Probabilistic Automata
Conference paper
Probably Safe or Live
Joost-Pieter Katoen, Lei Song, Lijun Zhang
CSL-LICS '14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
RWTH record for Probably Safe or Live BibTeX for Probably Safe or Live
Conference paper
Performance Analysis of Computing Servers : a case study exploiting a new GSPN semantics
Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu
Measurement, modelling, and evaluation of computing systems and dependability and fault-tolerance
RWTH record for Performance Analysis of Computing Servers : a case study exploiting a new GSPN semantics BibTeX for Performance Analysis of Computing Servers : a case study exploiting a new GSPN semantics
Conference paper
Model Checking Gigantic Markov Models
Joost-Pieter Katoen
Software engineering and formal methods
RWTH record for Model Checking Gigantic Markov Models BibTeX for Model Checking Gigantic Markov Models
Conference paper
Exponentially timed SADF : Compositional Semantics, Reduction, and Analysis
Joost-Pieter Katoen, Hao Wu
2014 proceedings of the International Conference on Embedded Software (EMSOFT)
RWTH record for Exponentially timed SADF : Compositional Semantics, Reduction, and Analysis BibTeX for Exponentially timed SADF : Compositional Semantics, Reduction, and Analysis
Conference paper
Smart Railroad Maintenance Engineering with Stochastic Model Checking
Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga, Ted Luiten, Judi Romijn
Proceedings of the Second International Conference on Railway Technology: Research, Development and Maintenance
RWTH record for Smart Railroad Maintenance Engineering with Stochastic Model Checking BibTeX for Smart Railroad Maintenance Engineering with Stochastic Model Checking
Conference paper
Parametric LTL on Markov Chains
Souymodip Chakraborty, Joost-Pieter Katoen
Theoretical computer science
RWTH record for Parametric LTL on Markov Chains BibTeX for Parametric LTL on Markov Chains
Conference paper
Zero-Reachability in Probabilistic Multi-Counter Automata
Tomáš Brázdil, Stefan Kiefer, Antonín Kucera, Petr Novotný, Joost-Pieter Katoen
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
RWTH record for Zero-Reachability in Probabilistic Multi-Counter Automata BibTeX for Zero-Reachability in Probabilistic Multi-Counter Automata
Conference paper
Fast Debugging of PRISM Models
Hans Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen
Automated technology for verification and analysis
RWTH record for Fast Debugging of PRISM Models BibTeX for Fast Debugging of PRISM Models
Journal article
Minimal counterexamples for linear-time probabilistic verification
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Theoretical computer science
RWTH record for Minimal counterexamples for linear-time probabilistic verification BibTeX for Minimal counterexamples for linear-time probabilistic verification
Journal article
Spacecraft early design validation using formal methods
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Panagiotis Katsaros, Konstantinos Mokos, Viet Yen Nguyen, Thomas Noll, Bart Postma, Marco Roveri
Reliability engineering & system safety
RWTH record for Spacecraft early design validation using formal methods BibTeX for Spacecraft early design validation using formal methods
Journal article
Symbolic counterexample generation for large discrete-time Markov chains
Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster
Science of computer programming
RWTH record for Symbolic counterexample generation for large discrete-time Markov chains BibTeX for Symbolic counterexample generation for large discrete-time Markov chains
Conference paper
Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey
Erika Ábrahám, Bernd Becker, Hans Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer
Formal methods for executable software models
RWTH record for Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey BibTeX for Counterexample Generation for Discrete-Time Markov Models : An Introductory Survey
Journal article
Operational versus weakest pre-expectation semantics for the probabilistic guarded command language
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver
Performance evaluation
RWTH record for Operational versus weakest pre-expectation semantics for the probabilistic guarded command language BibTeX for Operational versus weakest pre-expectation semantics for the probabilistic guarded command language

2013

Journal article
Abstract Probabilistic Automata
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski
Information and computation
RWTH record for Abstract Probabilistic Automata BibTeX for Abstract Probabilistic Automata
Journal article
Model checking for performability
Christel Baier, E. Moritz Hahn, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Mathematical structures in computer science
RWTH record for Model checking for performability BibTeX for Model checking for performability
Journal article
A compositional modelling and analysis framework for stochastic hybrid systems
Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, Joost-Pieter Katoen
Formal methods in system design
RWTH record for A compositional modelling and analysis framework for stochastic hybrid systems BibTeX for A compositional modelling and analysis framework for stochastic hybrid systems
Preprint
Accelerating Parametric Probabilistic Verification
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
PDF of Accelerating Parametric Probabilistic Verification RWTH record for Accelerating Parametric Probabilistic Verification BibTeX for Accelerating Parametric Probabilistic Verification
Book chapter
Model Checking Meets Probability : A Gentle Introduction
Joost-Pieter Katoen
Engineering Dependable Software Systems. - 34
RWTH record for Model Checking Meets Probability : A Gentle Introduction BibTeX for Model Checking Meets Probability : A Gentle Introduction
Conference paper
Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate
Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control
RWTH record for Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems BibTeX for Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems
Conference paper
PRINSYS : - on a Quest for Probabilistic Loop Invariants
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver
Quantitative evaluation of systems
RWTH record for PRINSYS : - on a Quest for Probabilistic Loop Invariants BibTeX for PRINSYS : - on a Quest for Probabilistic Loop Invariants
Conference paper
High-level Counterexamples for Probabilistic Automata
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Quantitative evaluation of systems
RWTH record for High-level Counterexamples for Probabilistic Automata BibTeX for High-level Counterexamples for Probabilistic Automata
Conference paper
Concurrency meets Probability: Theory and Practice
Joost-Pieter Katoen
CONCUR 2013 - concurrency theory
RWTH record for Concurrency meets Probability: Theory and Practice BibTeX for Concurrency meets Probability: Theory and Practice
Conference paper
Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems
Joost-Pieter Katoen, Doron Peled
Programming languages and systems
RWTH record for Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems BibTeX for Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems
Conference paper
Model-Based Energy Optimization of Automotive Control Systems
Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu
2013 Design, Automation & Test in Europe Conference & Exhibition (DATE 2013)
RWTH record for Model-Based Energy Optimization of Automotive Control Systems BibTeX for Model-Based Energy Optimization of Automotive Control Systems
Conference paper
SMT-based Bisimulation Minimisation of Markov Models
Hans Christian Dehnert, David Parker, Joost-Pieter Katoen
Verification, Model Checking, and Abstract Interpretation [Elektronische Ressource]
RWTH record for SMT-based Bisimulation Minimisation of Markov Models BibTeX for SMT-based Bisimulation Minimisation of Markov Models
Conference paper
A Semantics for Every GSPN
Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, Lijun Zhang
Application and theory of Petri nets and concurrency
RWTH record for A Semantics for Every GSPN BibTeX for A Semantics for Every GSPN
Conference paper
Modelling, Reduction and Analysis of Markov Automata
Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer
Quantitative evaluation of systems
RWTH record for Modelling, Reduction and Analysis of Markov Automata BibTeX for Modelling, Reduction and Analysis of Markov Automata
Preprint
High-level Counterexamples for Probabilistic Automata
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
PDF of High-level Counterexamples for Probabilistic Automata RWTH record for High-level Counterexamples for Probabilistic Automata BibTeX for High-level Counterexamples for Probabilistic Automata

2012

Conference paper
Weighted Lumpability on Markov Chains
Arpit Sharma, Joost-Pieter Katoen
Perspectives of system informatics
RWTH record for Weighted Lumpability on Markov Chains BibTeX for Weighted Lumpability on Markov Chains
Conference paper
The COMICS Tool : Computing Minimal Counterexamples for DTMCs
Nils Jansen, Erika Ábrahám, Matthias Volk, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Automated technology for verification and analysis
RWTH record for The COMICS Tool : Computing Minimal Counterexamples for DTMCs BibTeX for The COMICS Tool : Computing Minimal Counterexamples for DTMCs
Conference paper
Symbolic Counterexample Generation for Discrete-time Markov Chains
Nils Jansen, Erika Ábrahám, Barna Zajzon, Ralf Wimmer, Johann Schuster, Joost-Pieter Katoen, Bernd Becker
Formal aspects of component software
RWTH record for Symbolic Counterexample Generation for Discrete-time Markov Chains BibTeX for Symbolic Counterexample Generation for Discrete-time Markov Chains
Technical report
The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains
Nils Jansen, Erika Ábrahám, Maik Scheffler, Matthias Volk, Andreas Vorpahl, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
PDF of The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains RWTH record for The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains BibTeX for The COMICS Tool : Computing Minimal Counterexamples for Discrete-time Markov Chains
Conference paper
Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen
RWTH record for Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties BibTeX for Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties
Conference paper
Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver
2012 Ninth International Conference on Quantitative Evaluation of Systems (QEST), London, UK 17-20 September 2012,
RWTH record for Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language BibTeX for Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language
Conference paper
GSPNs Revisited: Simple Semantics and New Analysis Algorithms
Joost-Pieter Katoen
12th International Conference on Application of Concurrency to System Design - ACSD 2012, Hamburg, June 25-29, 2012
RWTH record for GSPNs Revisited: Simple Semantics and New Analysis Algorithms BibTeX for GSPNs Revisited: Simple Semantics and New Analysis Algorithms
Conference paper
Compositional Abstraction Techniques for Probabilistic Automata
Falak Sher, Joost-Pieter Katoen
Theoretical computer science
RWTH record for Compositional Abstraction Techniques for Probabilistic Automata BibTeX for Compositional Abstraction Techniques for Probabilistic Automata
Conference paper
Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite
Marie-Aude Esteve, Joost-Pieter Katoen, Viet Yen Nguyen, Bart Postma, Yuri Yushtein
2012 34th International Conference on Software Engineering (ICSE 2012)
RWTH record for Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite BibTeX for Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite
Conference paper
Robust PCTL Model Checking
Alessandro D'Innocenzo, Alessandro Abate, Joost-Pieter Katoen
Proceedings of the 15th International Conference on Hybrid Systems: Computation and Control
RWTH record for Robust PCTL Model Checking BibTeX for Robust PCTL Model Checking
Conference paper
Efficient Modelling and Generation of Markov Automata
Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga
CONCUR 2012 - concurrency theory
RWTH record for Efficient Modelling and Generation of Markov Automata BibTeX for Efficient Modelling and Generation of Markov Automata
Technical report
Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker
PDF of Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes RWTH record for Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes BibTeX for Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes
Journal article
Layered Reasoning for Randomized Distributed Algorithms
Mani Swaminathan, Joost-Pieter Katoen, Ernst-Rüdiger Olderog
Formal aspects of computing
RWTH record for Layered Reasoning for Randomized Distributed Algorithms BibTeX for Layered Reasoning for Randomized Distributed Algorithms
Journal article
Three-Valued Abstraction for Probabilistic Systems
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
The journal of logic and algebraic programming
RWTH record for Three-Valued Abstraction for Probabilistic Systems BibTeX for Three-Valued Abstraction for Probabilistic Systems
Journal article
A linear process-algebraic format with data for probabilistic automata
Joost-Pieter Katoen, Jaco van de Pol, Mariëlle Stoelinga, Mark Timmer
Theoretical computer science
RWTH record for A linear process-algebraic format with data for probabilistic automata BibTeX for A linear process-algebraic format with data for probabilistic automata
Conference paper
Quantitative Timed Analysis of Interactive Markov Chains
Dennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer
NASA formal methods
RWTH record for Quantitative Timed Analysis of Interactive Markov Chains BibTeX for Quantitative Timed Analysis of Interactive Markov Chains
Conference paper
Model Checking: One Can Do Much More Than You Think!
Joost-Pieter Katoen
Fundamentals of software engineering
RWTH record for Model Checking: One Can Do Much More Than You Think!BibTeX for Model Checking: One Can Do Much More Than You Think!
Conference paper
Minimal Critical Subsystems for Discrete-Time Markov Models
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen
Tools and algorithms for the construction and analysis of systems
RWTH record for Minimal Critical Subsystems for Discrete-Time Markov Models BibTeX for Minimal Critical Subsystems for Discrete-Time Markov Models
Conference paper
Model checking of scenario-aware dataflow with cadp
Bart Theelen, Joost-Pieter Katoen, Hao Wu
2012 Design, Automation & Test in Europe Conference & Exhibition (DATE 2012)
RWTH record for Model checking of scenario-aware dataflow with cadp BibTeX for Model checking of scenario-aware dataflow with cadp

2011

Conference paper
New Results on Abstract Probabilistic Automata
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski
2011 Eleventh International Conference on Application of Concurrency to System Design (ACSD 2011)
RWTH record for New Results on Abstract Probabilistic Automata BibTeX for New Results on Abstract Probabilistic Automata
Conference paper
Analysing and Improving Energy Efficiency of Distributed Slotted Aloha
Haidi Yue, Henrik Bohnenkamp, Malte Kampschulte, Joost-Pieter Katoen
Smart spaces and next generation wired/wireless networking
RWTH record for Analysing and Improving Energy Efficiency of Distributed Slotted Aloha BibTeX for Analysing and Improving Energy Efficiency of Distributed Slotted Aloha
Conference paper
System-Software Co-Engineering: Dependability and Safety Perspective
Yuri Yushtein, Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive, Marco Roveri
Proceedings, Fourth IEEE International Conference on Space Mission Challenges for Information Technology
RWTH record for System-Software Co-Engineering: Dependability and Safety Perspective BibTeX for System-Software Co-Engineering: Dependability and Safety Perspective
Conference paper
A two-step scheme for approximate model checking of stochastic hybrid systems
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, Maria Prandini
[Proceedings 18th IFAC World Congress 2011
RWTH record for A two-step scheme for approximate model checking of stochastic hybrid systems BibTeX for A two-step scheme for approximate model checking of stochastic hybrid systems
Conference paper
Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems
Hongfei Fu, Joost-Pieter Katoen
IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011) [Elektronische Ressource]
RWTH record for Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems BibTeX for Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems
Journal article
Time-bounded reachability in tree-structured QBDs by abstraction
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen
Performance evaluation
RWTH record for Time-bounded reachability in tree-structured QBDs by abstraction BibTeX for Time-bounded reachability in tree-structured QBDs by abstraction
Journal article
The Ins and Outs of the Probabilistic Model Checker MRMC
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen
Performance evaluation
RWTH record for The Ins and Outs of the Probabilistic Model Checker MRMC BibTeX for The Ins and Outs of the Probabilistic Model Checker MRMC
Journal article
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
Logical methods in computer science
PDF of Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications RWTH record for Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications BibTeX for Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Journal article
Trustworthy Aerospace Systems
Joost-Pieter Katoen, Thomas Noll
Public service review
RWTH record for Trustworthy Aerospace Systems BibTeX for Trustworthy Aerospace Systems
Conference paper
Hierarchical counterexamples for discrete-time markov chains
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Automated technolgoy for verification and analysis
RWTH record for Hierarchical counterexamples for discrete-time markov chains BibTeX for Hierarchical counterexamples for discrete-time markov chains
Conference paper
Reachability probabilities in markovian timed automata
Taolue Chen, Tingting Han, Joost-Pieter Katoen, A. Mereacre
2011 50th IEEE Conference on Decision and Control and European Control Conference
RWTH record for Reachability probabilities in markovian timed automata BibTeX for Reachability probabilities in markovian timed automata
Conference paper
A Local Greibach Normal Form for Hyperedge Replacement Grammars
Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll
Language and automata theory and applications
RWTH record for A Local Greibach Normal Form for Hyperedge Replacement Grammars BibTeX for A Local Greibach Normal Form for Hyperedge Replacement Grammars
Conference paper
Abstract Probabilistic Automata
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski
Verification, model checking, and abstract interpretation
RWTH record for Abstract Probabilistic Automata BibTeX for Abstract Probabilistic Automata
Conference paper
Efficient CTMC Model Checking of Linear Real-Time Objectives
Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
Tools and algorithms for the construction and analysis of systems
RWTH record for Efficient CTMC Model Checking of Linear Real-Time Objectives BibTeX for Efficient CTMC Model Checking of Linear Real-Time Objectives
Conference paper
Quantitative Automata Model Checking of Autonomous Stochastic Hybrid Systems
Alessandro Abate, Joost-Pieter Katoen, Alexandru Mereacre
HSCC'11
RWTH record for Quantitative Automata Model Checking of Autonomous Stochastic Hybrid Systems BibTeX for Quantitative Automata Model Checking of Autonomous Stochastic Hybrid Systems
Conference paper
Observing Continuous-Time MDPs by 1-Clock Timed Automata
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
Reachability problems
RWTH record for Observing Continuous-Time MDPs by 1-Clock Timed Automata BibTeX for Observing Continuous-Time MDPs by 1-Clock Timed Automata
Conference paper
Towards trustworthy aerospace systems: an experience report
Joost-Pieter Katoen
Formal methods for industrial critical systems
RWTH record for Towards trustworthy aerospace systems: an experience report BibTeX for Towards trustworthy aerospace systems: an experience report
Proceedings
CONCUR 2011 - concurrency theory : 22nd international conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011 ; proceedings
Springer
RWTH record for CONCUR 2011 - concurrency theory : 22nd international conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011 ; proceedings BibTeX for CONCUR 2011 - concurrency theory : 22nd international conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011 ; proceedings

2010

Journal article
Approximate model checking of stochastic hybrid systems
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, Maria Prandini
European journal of control
RWTH record for Approximate model checking of stochastic hybrid systems BibTeX for Approximate model checking of stochastic hybrid systems
Journal article
Performability Assessment by Model Checking of Markov Reward Models
Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Formal methods in system design
RWTH record for Performability Assessment by Model Checking of Markov Reward Models BibTeX for Performability Assessment by Model Checking of Markov Reward Models
Journal article
Performance Evaluation and Model Checking Join Forces
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Communications of the ACM
RWTH record for Performance Evaluation and Model Checking Join Forces BibTeX for Performance Evaluation and Model Checking Join Forces
Journal article
Learning Communicating Automata from MSCs
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker
IEEE transactions on software engineering
RWTH record for Learning Communicating Automata from MSCs BibTeX for Learning Communicating Automata from MSCs
Journal article
SMA: The Smyle Modeling Approach
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker
Computing and informatics
RWTH record for SMA: The Smyle Modeling Approach BibTeX for SMA: The Smyle Modeling Approach
Journal article
Safety, Dependability, and Performance Analysis of Extended AADL Models
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri
Computer journal
RWTH record for Safety, Dependability, and Performance Analysis of Extended AADL Models BibTeX for Safety, Dependability, and Performance Analysis of Extended AADL Models
Journal article
Computing Optimal Schedules for Battery Usage in Embedded Systems
Marijn R. Jongerden, Alexandru Mereacre, Henrik Bohnenkamp, Boudewijn R. Haverkort, Joost-Pieter Katoen
IEEE transactions on industrial informatics
RWTH record for Computing Optimal Schedules for Battery Usage in Embedded Systems BibTeX for Computing Optimal Schedules for Battery Usage in Embedded Systems
Conference paper
A Model Checker for AADL
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer
Computer aided verification
RWTH record for A Model Checker for AADL BibTeX for A Model Checker for AADL
Conference paper
The How and Why of Interactive Markov Chains
Holger Hermanns, Joost-Pieter Katoen
Formal methods for components and objects
RWTH record for The How and Why of Interactive Markov Chains BibTeX for The How and Why of Interactive Markov Chains
Conference paper
A Linear Process Algebraic Format for Probabilistic Systems with Data
Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga, Mark Timmer
Tenth International Conference on Application of Concurrency to System Design
RWTH record for A Linear Process Algebraic Format for Probabilistic Systems with Data BibTeX for A Linear Process Algebraic Format for Probabilistic Systems with Data
Conference paper
Advances in Probabilistic Model Checking
Joost-Pieter Katoen
Verification, model checking, and abstract interpretation
RWTH record for Advances in Probabilistic Model Checking BibTeX for Advances in Probabilistic Model Checking
Conference paper
Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods
Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, Carroll Morgan
Static analysis
RWTH record for Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods BibTeX for Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods
Conference paper
Analyzing Energy Consumption in a Gossiping MAC Protocol
Haidi Yue, Henrik Bohnenkamp, Joost-Pieter Katoen
Measurement, modelling and evaluation of computing systems and dependability in fault tolerance
RWTH record for Analyzing Energy Consumption in a Gossiping MAC Protocol BibTeX for Analyzing Energy Consumption in a Gossiping MAC Protocol
Conference paper
Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption
Haidi Yue, Joost-Pieter Katoen
Analytical and stochastic modeling techniques and applications
RWTH record for Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption BibTeX for Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption
Conference paper
Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report
Falko Dulat, Joost-Pieter Katoen, Viet Yen Nguyen
Computer performance engineering
RWTH record for Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report BibTeX for Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report
Conference paper
DTMC Model Checking by SCC Reduction
Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker
Proceedings
RWTH record for DTMC Model Checking by SCC Reduction BibTeX for DTMC Model Checking by SCC Reduction
Conference paper
libalf: The Automata Learning Framework
Benedikt Bollig, Carsten Kern, Joost-Pieter Katoen, Daniel Neider, David R. Piegdon
Computer aided verification
RWTH record for libalf: The Automata Learning Framework BibTeX for libalf: The Automata Learning Framework
Technical report
Computing Maximum Reachability Probabilities in Markovian Timed Automata
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
PDF of Computing Maximum Reachability Probabilities in Markovian Timed Automata RWTH record for Computing Maximum Reachability Probabilities in Markovian Timed Automata BibTeX for Computing Maximum Reachability Probabilities in Markovian Timed Automata

2009

Journal article
Counterexample Generation in Probabilistic Model Checking
Tingting Han, Joost-Pieter Katoen, Berteun Damman
IEEE transactions on software engineering
RWTH record for Counterexample Generation in Probabilistic Model Checking BibTeX for Counterexample Generation in Probabilistic Model Checking
Conference paper
The Ins and Outs of The Probabilistic Model Checker MRMC
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen
Sixth International Conference on the Quantitative Evaluation of Systems, 2009
RWTH record for The Ins and Outs of The Probabilistic Model Checker MRMC BibTeX for The Ins and Outs of The Probabilistic Model Checker MRMC
Conference paper
Time-Bounded Reachability in Tree-Structured QBDs by Abstraction
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen
Sixth International Conference on the Quantitative Evaluation of Systems, 2009
RWTH record for Time-Bounded Reachability in Tree-Structured QBDs by Abstraction BibTeX for Time-Bounded Reachability in Tree-Structured QBDs by Abstraction
Conference paper
Simulation-based CTMC Model Checking: An Empirical Evaluation
Joost-Pieter Katoen, Ivan S. Zapreev
QUEST 2009
RWTH record for Simulation-based CTMC Model Checking: An Empirical Evaluation BibTeX for Simulation-based CTMC Model Checking: An Empirical Evaluation
Conference paper
Maximizing System Lifetime by Battery Scheduling
Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik Bohnenkamp, Joost-Pieter Katoen
2009 IEEE/IFIP International Conference on Dependable Systems & Networks
RWTH record for Maximizing System Lifetime by Battery Scheduling BibTeX for Maximizing System Lifetime by Battery Scheduling
Conference paper
Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
2009 24th Annual IEEE Symposium on Logic in Computer Science
RWTH record for Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications BibTeX for Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
Conference paper
Verification and Performance Evaluation of AADL Models (Tool Demonstration)
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri
ESEC-FSE’09
RWTH record for Verification and Performance Evaluation of AADL Models (Tool Demonstration)BibTeX for Verification and Performance Evaluation of AADL Models (Tool Demonstration)
Conference paper
Model-Based Codesign of Critical Embedded Systems
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri
Workshop Proceedings
RWTH record for Model-Based Codesign of Critical Embedded Systems BibTeX for Model-Based Codesign of Critical Embedded Systems
Conference paper
Codesign of Dependable Systems: A Component-Based Modeling Language
Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll
Seventh ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009): Cambridge, Massachusetts, July 13-15, 2009
RWTH record for Codesign of Dependable Systems: A Component-Based Modeling Language BibTeX for Codesign of Dependable Systems: A Component-Based Modeling Language
Conference paper
Delayed Nondeterminism in Continuous-Time Markov Decision Processes
Martin R. Neuhäußer, Marielle Stoelinga, Joost-Pieter Katoen
Foundations of software science and computational structures
RWTH record for Delayed Nondeterminism in Continuous-Time Markov Decision Processes BibTeX for Delayed Nondeterminism in Continuous-Time Markov Decision Processes
Conference paper
Compositional Abstraction for Stochastic Systems
Joost-Pieter Katoen, Daniel Klink, Martin R. Neuhäußer
Formal modeling and analysis of timed systems
RWTH record for Compositional Abstraction for Stochastic Systems BibTeX for Compositional Abstraction for Stochastic Systems
Conference paper
LTL model checking of time-inhomogeneous Markov chains
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
Automated technology for verification and analysis
RWTH record for LTL model checking of time-inhomogeneous Markov chains BibTeX for LTL model checking of time-inhomogeneous Markov chains
Conference paper
The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri
Computer safety, reliability, and security
RWTH record for The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems BibTeX for The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems
Technical report
Compositional Abstraction for Stochastic Systems
Joost-Pieter Katoen, Daniel Klink, Martin R. Neuhäußer
PDF of Compositional Abstraction for Stochastic Systems RWTH record for Compositional Abstraction for Stochastic Systems BibTeX for Compositional Abstraction for Stochastic Systems
Technical report
Quantitative model checking of continuous-time Markov chains against timed automata specifications
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
PDF of Quantitative model checking of continuous-time Markov chains against timed automata specifications RWTH record for Quantitative model checking of continuous-time Markov chains against timed automata specifications BibTeX for Quantitative model checking of continuous-time Markov chains against timed automata specifications

2008

Conference paper
The Surprising Robustness of (Closed) Timed Automata against Clock-Drift
Mani Swaminathan, Martin Fränzle, Joost-Pieter Katoen
Fifth IFIP International Conference on Theoretical Computer Science - TCS 2008
RWTH record for The Surprising Robustness of (Closed) Timed Automata against Clock-Drift BibTeX for The Surprising Robustness of (Closed) Timed Automata against Clock-Drift
Conference paper
Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques
Joost-Pieter Katoen
Design, automation and test in Europe, 2008
RWTH record for Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques BibTeX for Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques
Conference paper
Perspectives in Probabilistic Verification
Joost-Pieter Katoen
Proceedings
RWTH record for Perspectives in Probabilistic Verification BibTeX for Perspectives in Probabilistic Verification
Conference paper
How to model and analyze gossiping protocols?
Joost-Pieter Katoen
SIGMETRICS'08
RWTH record for How to model and analyze gossiping protocols?BibTeX for How to model and analyze gossiping protocols?
Conference paper
Approximate parameter synthesis for probabilistic time-bounded reachability
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
Proceedings
RWTH record for Approximate parameter synthesis for probabilistic time-bounded reachability BibTeX for Approximate parameter synthesis for probabilistic time-bounded reachability
Conference paper
Regular Expressions for PCTL Counterexamples
Berteun Damman, Tingting Han, Joost-Pieter Katoen
Quantitative evaluation of systems
RWTH record for Regular Expressions for PCTL Counterexamples BibTeX for Regular Expressions for PCTL Counterexamples
Conference paper
Time-Abstracting Bisimulation for Probabilistic Timed Automata
Taolue Chen, Tingting Han, Joost-Pieter Katoen
Proceedings
RWTH record for Time-Abstracting Bisimulation for Probabilistic Timed Automata BibTeX for Time-Abstracting Bisimulation for Probabilistic Timed Automata
Conference paper
Symmetry reduction for stochastic hybrid systems
Manuela Bujorianu, Joost-Pieter Katoen
2008 47th IEEE Conference on Decision and Control
RWTH record for Symmetry reduction for stochastic hybrid systems BibTeX for Symmetry reduction for stochastic hybrid systems
Book
Principles of model checking
Christel Baier, Joost-Pieter Katoen
MIT Press
RWTH record for Principles of model checking BibTeX for Principles of model checking
Conference paper
Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains
Joost-Pieter Katoen, Alexandru Mereacre
Formal modeling and analysis of timed systems
RWTH record for Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains BibTeX for Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains
Conference paper
Abstraction for Stochastic Systems by Erlang's Method of Stages
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
CONCUR 2008 - concurrency theory
RWTH record for Abstraction for Stochastic Systems by Erlang's Method of Stages BibTeX for Abstraction for Stochastic Systems by Erlang's Method of Stages
Conference paper
How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison
David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Marielle Stoelinga, Ivan S. Zapreev
Hardware and software: verification and testing
RWTH record for How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison BibTeX for How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison
Conference paper
Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
Hybrid systems: computation and control ; 11th international workshop, HSCC 2008, St. Louis, MO, USA, April 22-24, 2008 ; proceedings
RWTH record for Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains BibTeX for Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains
Conference paper
Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning
Benedikt Bollig, Carsten Kern, Joost-Pieter Katoen, Martin Leucker
CONCUR 2008 - concurrency theory
RWTH record for Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning BibTeX for Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning
Book chapter
Reachability in continuous-time Markov reward decision processes
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Logic and automata
RWTH record for Reachability in continuous-time Markov reward decision processes BibTeX for Reachability in continuous-time Markov reward decision processes
Technical report
Abstraction for stochastic systems by Erlangs method of stages
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
PDF of Abstraction for stochastic systems by Erlangs method of stages RWTH record for Abstraction for stochastic systems by Erlangs method of stages BibTeX for Abstraction for stochastic systems by Erlangs method of stages
Technical report
SMA - the Smyle modeling approach
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker
RWTH record for SMA - the Smyle modeling approach BibTeX for SMA - the Smyle modeling approach

2007

Journal article
Model checking mobile stochastic logic
Rocco de Nicola, Joost-Pieter Katoen, Diego Latella, Michele Loreti, Mieke Massink
Theoretical computer science
RWTH record for Model checking mobile stochastic logic BibTeX for Model checking mobile stochastic logic
Conference paper
Bisimulation minimisation mostly speeds up probabilistic model checking
Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen
Tools and algorithms for the construction and analysis of systems
RWTH record for Bisimulation minimisation mostly speeds up probabilistic model checking BibTeX for Bisimulation minimisation mostly speeds up probabilistic model checking
Conference paper
Verifying concurrent list-manipulating programs by LTL model checking
Joost-Pieter Katoen, Thomas Noll, Stefan Rieger
HAV 2007
PDF of Verifying concurrent list-manipulating programs by LTL model checking RWTH record for Verifying concurrent list-manipulating programs by LTL model checking BibTeX for Verifying concurrent list-manipulating programs by LTL model checking
Technical report
Verifying concurrent list-manipulating programs by LTL model checking
Joost-Pieter Katoen, Thomas Noll, Stefan Rieger
PDF of Verifying concurrent list-manipulating programs by LTL model checking RWTH record for Verifying concurrent list-manipulating programs by LTL model checking BibTeX for Verifying concurrent list-manipulating programs by LTL model checking
Conference paper
Replaying play in and play out : synthesis of design models from scenarios by learning
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker
Tools and algorithms for the construction and analysis of systems
RWTH record for Replaying play in and play out : synthesis of design models from scenarios by learning BibTeX for Replaying play in and play out : synthesis of design models from scenarios by learning
Conference paper
Counterexamples in probabilistic model checking
Tingting Han, Joost-Pieter Katoen
Tools and algorithms for the construction and analysis of systems
RWTH record for Counterexamples in probabilistic model checking BibTeX for Counterexamples in probabilistic model checking
Conference paper
Abstraction of probabilistic systems
Joost-Pieter Katoen
Formal modeling and analysis of timed systems
RWTH record for Abstraction of probabilistic systems BibTeX for Abstraction of probabilistic systems
Conference paper
Providing evidence of likely being on time : counterexample generation for CTMC model checking
Tingting Han, Joost-Pieter Katoen
Automated technology for verification and analysis
RWTH record for Providing evidence of likely being on time : counterexample generation for CTMC model checking BibTeX for Providing evidence of likely being on time : counterexample generation for CTMC model checking
Conference paper
Three-Valued Abstraction for Continuous-Time Markov Chains
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
Computer aided verification
RWTH record for Three-Valued Abstraction for Continuous-Time Markov Chains BibTeX for Three-Valued Abstraction for Continuous-Time Markov Chains
Conference paper
Bisimulation and logical preservation for continuous-time Markov decision processes
Martin R. Neuhäußer, Joost-Pieter Katoen
CONCUR 2007 - concurrency theory
RWTH record for Bisimulation and logical preservation for continuous-time Markov decision processes BibTeX for Bisimulation and logical preservation for continuous-time Markov decision processes
Conference paper
Motor : the MoDeST tool environment
Henrik Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen
Tools and algorithms for the construction and analysis of systems
RWTH record for Motor : the MoDeST tool environment BibTeX for Motor : the MoDeST tool environment
Book chapter
Stochastic model checking
Joost-Pieter Katoen
Stochastic Hybrid Systems
RWTH record for Stochastic model checking BibTeX for Stochastic model checking
Technical report
Compositional modeling and minimization of time-inhomogeneous Markov chains
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre
PDF of Compositional modeling and minimization of time-inhomogeneous Markov chains RWTH record for Compositional modeling and minimization of time-inhomogeneous Markov chains BibTeX for Compositional modeling and minimization of time-inhomogeneous Markov chains
Technical report
Three-valued abstraction for probabilistic systems
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf
PDF of Three-valued abstraction for probabilistic systems RWTH record for Three-valued abstraction for probabilistic systems BibTeX for Three-valued abstraction for probabilistic systems
Technical report
Bisimulation and logical preservation for continuous-time Markov decision processes
Martin R. Neuhäußer, Joost-Pieter Katoen
PDF of Bisimulation and logical preservation for continuous-time Markov decision processes RWTH record for Bisimulation and logical preservation for continuous-time Markov decision processes BibTeX for Bisimulation and logical preservation for continuous-time Markov decision processes

2006

Journal article
Guest editors introduction to the special section on the first International Conference on the Quantitative Evaluation of SysTems (QEST)
Giuliana Franceschinis, Joost-Pieter Katoen, Murray Woodside
IEEE transactions on software engineering
RWTH record for Guest editors introduction to the special section on the first International Conference on the Quantitative Evaluation of SysTems (QEST)BibTeX for Guest editors introduction to the special section on the first International Conference on the Quantitative Evaluation of SysTems (QEST)
Conference paper
Probably on time and within budget : on reachability in priced probabilistic timed automata
Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen
Third International Conference on the Quantitative Evaluation of Systems
RWTH record for Probably on time and within budget : on reachability in priced probabilistic timed automata BibTeX for Probably on time and within budget : on reachability in priced probabilistic timed automata
Conference paper
Safe on-the-fly steady-state detection for time-bounded reachability
Joost-Pieter Katoen, Ivan S. Zapreev
Third International Conference on the Quantitative Evaluation of Systems
RWTH record for Safe on-the-fly steady-state detection for time-bounded reachability BibTeX for Safe on-the-fly steady-state detection for time-bounded reachability
Journal article
Towards a logic for performance and mobility
Rocco de Nicola, Joost-Pieter Katoen, Diego Latella, Mieke Massink
Electronic notes in theoretical computer science
RWTH record for Towards a logic for performance and mobility BibTeX for Towards a logic for performance and mobility
Journal article
YMCA : why Markov chain algebra?
Mario Bravetti, Holger Hermanns, Joost-Pieter Katoen
Electronic notes in theoretical computer science
RWTH record for YMCA : why Markov chain algebra?BibTeX for YMCA : why Markov chain algebra?
Journal article
MoDeST : a compositional modeling formalism for real-time and stochastic systems
Henrik Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen
IEEE transactions on software engineering
RWTH record for MoDeST : a compositional modeling formalism for real-time and stochastic systems BibTeX for MoDeST : a compositional modeling formalism for real-time and stochastic systems
Conference paper
Safety and liveness in concurrent pointer programs
Dino Distefano, Joost-Pieter Katoen, Arend Rensink
Formal methods for components and objects
RWTH record for Safety and liveness in concurrent pointer programs BibTeX for Safety and liveness in concurrent pointer programs
Technical report
Counterexamples in probabilistic model checking
Tingting Han, Joost-Pieter Katoen
PDF of Counterexamples in probabilistic model checking RWTH record for Counterexamples in probabilistic model checking BibTeX for Counterexamples in probabilistic model checking
Technical report
Replaying play in and play out : synthesis of design models from scenarios by learning
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker
RWTH record for Replaying play in and play out : synthesis of design models from scenarios by learning BibTeX for Replaying play in and play out : synthesis of design models from scenarios by learning

2005

Journal article
Model checking meets performance evaluation
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Performance evaluation review
RWTH record for Model checking meets performance evaluation BibTeX for Model checking meets performance evaluation
Journal article
Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
Christel Baier, Holger Hermanns, Joost-Pieter Katoen, Boudewijn R. Haverkort
Theoretical computer science
RWTH record for Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes BibTeX for Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes
Journal article
A theory of stochastic systems. Part II: Process algebra
Pedro R. D'Argenio, Joost-Pieter Katoen
Information and computation
RWTH record for A theory of stochastic systems. Part II: Process algebra BibTeX for A theory of stochastic systems. Part II: Process algebra
Journal article
Comparative branching-time semantics for Markov chains
Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Verena Wolf
Information and computation
RWTH record for Comparative branching-time semantics for Markov chains BibTeX for Comparative branching-time semantics for Markov chains
Journal article
A theory of stochastic systems. Part I: Stochastic automata
Pedro R. D'Argenio, Joost-Pieter Katoen
Information and computation
RWTH record for A theory of stochastic systems. Part I: Stochastic automata BibTeX for A theory of stochastic systems. Part I: Stochastic automata
Conference paper
Model checking Markov reward models with impulse rewards
Lucia Cloth, Joost-Pieter Katoen, Maneesh Khattri, Reza Pulungan
Proceedings
RWTH record for Model checking Markov reward models with impulse rewards BibTeX for Model checking Markov reward models with impulse rewards
Conference paper
A Markov reward model checker
Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev
Proceedings
RWTH record for A Markov reward model checker BibTeX for A Markov reward model checker
Conference paper
Are you still there? : a lightweight algorithm to monitor node presence in self-configuring networks
Henrik Bohnenkamp, Johan Gorter, Jarno Guidi, Joost-Pieter Katoen
Proceedings
RWTH record for Are you still there? : a lightweight algorithm to monitor node presence in self-configuring networks BibTeX for Are you still there? : a lightweight algorithm to monitor node presence in self-configuring networks
Book
Model-based testing of reactive systems : advanced lectures ; [outcome of a research seminar held in Schloss Dagstuhl in January 2004]
Springer
RWTH record for Model-based testing of reactive systems : advanced lectures ; [outcome of a research seminar held in Schloss Dagstuhl in January 2004]BibTeX for Model-based testing of reactive systems : advanced lectures ; [outcome of a research seminar held in Schloss Dagstuhl in January 2004]

2002

Conference paper
Automated performance and dependability evaluation using model checking
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Performance evaluation of complex systems
RWTH record for Automated performance and dependability evaluation using model checking BibTeX for Automated performance and dependability evaluation using model checking
Conference paper
Model checking performability properties
Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, Christel Baier
Proceedings
RWTH record for Model checking performability properties BibTeX for Model checking performability properties

2000

Conference paper
On the Logical Characterisation of Performability Properties
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Automata, languages and programming
RWTH record for On the Logical Characterisation of Performability Properties BibTeX for On the Logical Characterisation of Performability Properties
Conference paper
On the use of model checking techniques for dependability evaluation
Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen
Proceedings
RWTH record for On the use of model checking techniques for dependability evaluation BibTeX for On the use of model checking techniques for dependability evaluation
Conference paper
Model checking continuous-time Markov chains by transient analysis
C. Baier, Boudewijn R. Haverkort, H. Hermanns, Joost-Pieter Katoen
Computer aided verification
RWTH record for Model checking continuous-time Markov chains by transient analysis BibTeX for Model checking continuous-time Markov chains by transient analysis

Supervised theses

2026

Bachelor’s thesis
Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Ole Dannemeyer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Tobias Winkler, Lisa Pühl
RWTH record for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers BibTeX for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Bachelor’s thesis
Distribution transformers for probabilistic programs: a study of inductive definability
Felix Euting
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Distribution transformers for probabilistic programs: a study of inductive definability BibTeX for Distribution transformers for probabilistic programs: a study of inductive definability
Bachelor’s thesis
Semantic equivalences of probabilistic programs and their underlying Markov chains
Philip Strüwer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Daniel Johannes Zilken, Jan-Gustav Michnia
RWTH record for Semantic equivalences of probabilistic programs and their underlying Markov chains BibTeX for Semantic equivalences of probabilistic programs and their underlying Markov chains
Bachelor’s thesis
Predicate transformers for nondeterministic quantum programs
Xi Wang
RWTH Aachen University
Advisers: Dominique Unruh, Joost-Pieter Katoen
Consultants: Christina Gehnen
PDF of Predicate transformers for nondeterministic quantum programs RWTH record for Predicate transformers for nondeterministic quantum programs BibTeX for Predicate transformers for nondeterministic quantum programs
Master’s thesis
A formal language for expressing quantum predicates
Umut Yigit Dural
RWTH Aachen University
Advisers: Dominique Unruh, Joost-Pieter Katoen
Consultants: Christina Gehnen
PDF of A formal language for expressing quantum predicates RWTH record for A formal language for expressing quantum predicates BibTeX for A formal language for expressing quantum predicates
Master’s thesis
Bounds for quantum weakest preconditions
Jonas Deutsch
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dominique Unruh
Consultants: Christina Gehnen
PDF of Bounds for quantum weakest preconditions RWTH record for Bounds for quantum weakest preconditions BibTeX for Bounds for quantum weakest preconditions
Master’s thesis
Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning
Jonas Seidel
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
PDF of Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning RWTH record for Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning BibTeX for Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning
Bachelor’s thesis
Which probabalistic programs are modelcheckable?
Samuel Akinlaja
Rheinisch-Westfälische Technische Hochschule Aachen
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Which probabalistic programs are modelcheckable?BibTeX for Which probabalistic programs are modelcheckable?

2025

PhD thesis
Deductive reasoning about concurrent probabilistic programs
Ira Justus Fesefeldt
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Lars Birkedal
PDF of Deductive reasoning about concurrent probabilistic programs RWTH record for Deductive reasoning about concurrent probabilistic programs BibTeX for Deductive reasoning about concurrent probabilistic programs
Master’s thesis
Multi‐agent path finding for reversible conveyors
Dominic Sebastian Meiser
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Roy Hermanns
PDF of Multi‐agent path finding for reversible conveyors RWTH record for Multi‐agent path finding for reversible conveyors BibTeX for Multi‐agent path finding for reversible conveyors
Bachelor’s thesis
Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies
Muhammad Asad Murtaza Butt
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Hannah Mertens
RWTH record for Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies BibTeX for Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies
Master’s thesis
Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates
Rico Stanosek
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates BibTeX for Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates
Bachelor’s thesis
Scalable qubit routing on the conveyor-based SpinBus architecture
Dobromir Panayotov
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Roy Hermanns
RWTH record for Scalable qubit routing on the conveyor-based SpinBus architecture BibTeX for Scalable qubit routing on the conveyor-based SpinBus architecture
Bachelor’s thesis
Evaluating tool support for fault tree analysis of satellite constellations
Mareike Metzler
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
PDF of Evaluating tool support for fault tree analysis of satellite constellations RWTH record for Evaluating tool support for fault tree analysis of satellite constellations BibTeX for Evaluating tool support for fault tree analysis of satellite constellations
Bachelor’s thesis
Exploration of certificate sharing for neural network verification
Glen Jordan Grant
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix, Xaver Fink
RWTH record for Exploration of certificate sharing for neural network verification BibTeX for Exploration of certificate sharing for neural network verification
Bachelor’s thesis
On the relation of rely-guarantee and assume-guarantee reasoning
Marcel Eissing
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Lena Verscht, Hannah Mertens
PDF of On the relation of rely-guarantee and assume-guarantee reasoning RWTH record for On the relation of rely-guarantee and assume-guarantee reasoning BibTeX for On the relation of rely-guarantee and assume-guarantee reasoning
Bachelor’s thesis
Modeling non-deterministic quantum programs for model checking
Kaleb Kierner
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dominique Unruh
Consultants: Christina Gehnen
PDF of Modeling non-deterministic quantum programs for model checking RWTH record for Modeling non-deterministic quantum programs for model checking BibTeX for Modeling non-deterministic quantum programs for model checking
Bachelor’s thesis
Implementing the denotational semantics of probabilistic programs
Elbeck Lazaridi
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Implementing the denotational semantics of probabilistic programs BibTeX for Implementing the denotational semantics of probabilistic programs
PhD thesis
Analysis of probabilistic programs using generating functions
Lutz Klinkenberg
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Laura Kovacs
PDF of Analysis of probabilistic programs using generating functions RWTH record for Analysis of probabilistic programs using generating functions BibTeX for Analysis of probabilistic programs using generating functions
Master’s thesis
Effective quantifier-based reasoning for quantitative deductive verification
Emil Beothy-Elo
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Philipp Schroer, Darion Haase
PDF of Effective quantifier-based reasoning for quantitative deductive verification RWTH record for Effective quantifier-based reasoning for quantitative deductive verification BibTeX for Effective quantifier-based reasoning for quantitative deductive verification
Master’s thesis
Automata-based semantics for the probabilistic programming language ReDiP
Dominik Geißler
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Automata-based semantics for the probabilistic programming language ReDiP RWTH record for Automata-based semantics for the probabilistic programming language ReDiP BibTeX for Automata-based semantics for the probabilistic programming language ReDiP

2024

Master’s thesis
MARVEL: A stepwise debugging tool for Markov models in the PRISM-language
Patrick Arens
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for MARVEL: A stepwise debugging tool for Markov models in the PRISM-language BibTeX for MARVEL: A stepwise debugging tool for Markov models in the PRISM-language
Bachelor’s thesis
Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks
Yejun Tang
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks BibTeX for Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks
PhD thesis
Automated deductive verification of probabilistic programs
Kevin Batz
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Ichiro Hasuo
PDF of Automated deductive verification of probabilistic programs RWTH record for Automated deductive verification of probabilistic programs BibTeX for Automated deductive verification of probabilistic programs
PhD thesis
Probabilistic model checking and parameter tuning for Bayesian networks
Bahare Salmani Barzoki
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Luc de Raedt
PDF of Probabilistic model checking and parameter tuning for Bayesian networks RWTH record for Probabilistic model checking and parameter tuning for Bayesian networks BibTeX for Probabilistic model checking and parameter tuning for Bayesian networks
Master’s thesis
A deductive verifier for probabilistic programs
Philipp Schroer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Peter Müller
Consultants: Kevin Batz, Benjamin Kaminski, Christoph Matheja
PDF of A deductive verifier for probabilistic programs RWTH record for A deductive verifier for probabilistic programs BibTeX for A deductive verifier for probabilistic programs
PhD thesis
Applying software model checking: experiences and advancements
Philipp Berger
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dirk Beyer
PDF of Applying software model checking: experiences and advancements RWTH record for Applying software model checking: experiences and advancements BibTeX for Applying software model checking: experiences and advancements
Master’s thesis
Distributional invariants for probabilistic programs
Daniel Johannes Zilken
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Kevin Batz, Tobias Winkler
RWTH record for Distributional invariants for probabilistic programs BibTeX for Distributional invariants for probabilistic programs
Master’s thesis
Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs
Patrick Nossol
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen, Ira Justus Fesefeldt
PDF of Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs RWTH record for Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs BibTeX for Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs
Bachelor’s thesis
Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm
Sven Büge
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Alexander Nikolai Bork
RWTH record for Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm BibTeX for Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm
Bachelor’s thesis
Heuristic synthesis of spare parts inventories using dynamic fault trees
Jakob van Sprang
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Heuristic synthesis of spare parts inventories using dynamic fault trees BibTeX for Heuristic synthesis of spare parts inventories using dynamic fault trees
Bachelor’s thesis
Semantics-preserving transformation of Java source code
Frederik Heigold
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Semantics-preserving transformation of Java source code BibTeX for Semantics-preserving transformation of Java source code
Bachelor’s thesis
Most probable explanations in Bayesian Networks via weighted programming
Dinis Vitorino
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler, Kevin Batz
PDF of Most probable explanations in Bayesian Networks via weighted programming RWTH record for Most probable explanations in Bayesian Networks via weighted programming BibTeX for Most probable explanations in Bayesian Networks via weighted programming
Bachelor’s thesis
Model checking pPDA vs unambiguous automata
Anastasiia Petrova
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Model checking pPDA vs unambiguous automata RWTH record for Model checking pPDA vs unambiguous automata BibTeX for Model checking pPDA vs unambiguous automata
Master’s thesis
Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning
Johannes Lehmann
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning RWTH record for Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning BibTeX for Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning
Bachelor’s thesis
Proving termination of probabilistic recursive programs via SMT-solving
Leo Mommers
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Erika Ábrahám
Consultants: Tobias Winkler
PDF of Proving termination of probabilistic recursive programs via SMT-solving RWTH record for Proving termination of probabilistic recursive programs via SMT-solving BibTeX for Proving termination of probabilistic recursive programs via SMT-solving
Bachelor’s thesis
Compositional control-flow reduction for probabilistic model checking
Naomi Barth
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Compositional control-flow reduction for probabilistic model checking RWTH record for Compositional control-flow reduction for probabilistic model checking BibTeX for Compositional control-flow reduction for probabilistic model checking
Master’s thesis
Invariant-based strategy synthesis for nondeterministic probabilistic programs
Tom Biskup
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
PDF of Invariant-based strategy synthesis for nondeterministic probabilistic programs RWTH record for Invariant-based strategy synthesis for nondeterministic probabilistic programs BibTeX for Invariant-based strategy synthesis for nondeterministic probabilistic programs
Master’s thesis
Complexity and decidability of multi-objective stochastic games
Tobias Winkler
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Jan Křetínský
Consultants: Maximilian Weininger
PDF of Complexity and decidability of multi-objective stochastic games RWTH record for Complexity and decidability of multi-objective stochastic games BibTeX for Complexity and decidability of multi-objective stochastic games
Bachelor’s thesis
Combining integer programs and graph grammars: Theory and implementation in Attestor
Alexander Ferber
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
PDF of Combining integer programs and graph grammars: Theory and implementation in Attestor RWTH record for Combining integer programs and graph grammars: Theory and implementation in Attestor BibTeX for Combining integer programs and graph grammars: Theory and implementation in Attestor

2023

Master’s thesis
Evaluation of out-of-distribution detection techniques for dataset filtering
Lasse van der Woude
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Evaluation of out-of-distribution detection techniques for dataset filtering BibTeX for Evaluation of out-of-distribution detection techniques for dataset filtering
Bachelor’s thesis
Automated assessment of regular expressions
Ebru Kusak
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Automated assessment of regular expressions BibTeX for Automated assessment of regular expressions
Master’s thesis
Architecture-oriented safety verification of transformer networks via program analysis
Daniel Alexander Heinen
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Architecture-oriented safety verification of transformer networks via program analysis BibTeX for Architecture-oriented safety verification of transformer networks via program analysis
Bachelor’s thesis
Slicing COBOL software for program understanding
Stefan Busch
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Slicing COBOL software for program understanding BibTeX for Slicing COBOL software for program understanding
Master’s thesis
Approximate probabilistic bisimulations and quotienting
Timm Spork
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Approximate probabilistic bisimulations and quotienting BibTeX for Approximate probabilistic bisimulations and quotienting
Master’s thesis
Representing Markov models by extending the intermediate model checking language
Jialei Yao
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Representing Markov models by extending the intermediate model checking language BibTeX for Representing Markov models by extending the intermediate model checking language
Bachelor’s thesis
Automatic algorithm selection for probabilistic model checking using machine learning
Umut Yigit Dural
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann, Alexander Nikolai Bork
RWTH record for Automatic algorithm selection for probabilistic model checking using machine learning BibTeX for Automatic algorithm selection for probabilistic model checking using machine learning
Bachelor’s thesis
Strategy computation for a Markovian disease spread model
Gergana Tropcheva
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Alexander Nikolai Bork
RWTH record for Strategy computation for a Markovian disease spread model BibTeX for Strategy computation for a Markovian disease spread model
PhD thesis
Monotonicity in Markov models
Jip Josephine Spel
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tatjana Petrov
PDF of Monotonicity in Markov models RWTH record for Monotonicity in Markov models BibTeX for Monotonicity in Markov models
Bachelor’s thesis
Comparison of symbolic maximal end component decomposition algorithms
Felix Faber
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Comparison of symbolic maximal end component decomposition algorithms BibTeX for Comparison of symbolic maximal end component decomposition algorithms
PhD thesis
Verification of multi-objective Markov models
Tim Quatmann
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Mickael Randour
PDF of Verification of multi-objective Markov models RWTH record for Verification of multi-objective Markov models BibTeX for Verification of multi-objective Markov models
PhD thesis
Synthesizing FDIR recovery strategies for space systems
Sascha Müller
RWTH Aachen University
Advisers: Thomas Noll, Andreas Gerndt, Joost-Pieter Katoen
PDF of Synthesizing FDIR recovery strategies for space systems RWTH record for Synthesizing FDIR recovery strategies for space systems BibTeX for Synthesizing FDIR recovery strategies for space systems
Bachelor’s thesis
On-the-fly data race detection for OpenSHMEM programs
Sven Klotz
RWTH Aachen University
Advisers: Matthias S. Müller, Joost-Pieter Katoen
Consultants: Simon Schwitanski
PDF of On-the-fly data race detection for OpenSHMEM programs RWTH record for On-the-fly data race detection for OpenSHMEM programs BibTeX for On-the-fly data race detection for OpenSHMEM programs

2022

Bachelor’s thesis
Implementation of an LTL model checker for probabilistic pushdown automata
Laura Bamberger
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
RWTH record for Implementation of an LTL model checker for probabilistic pushdown automata BibTeX for Implementation of an LTL model checker for probabilistic pushdown automata
Master’s thesis
Inference in discrete probabilistic programs using probability generating functions
Christian Blumenthal
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Lutz Klinkenberg, Tobias Winkler
RWTH record for Inference in discrete probabilistic programs using probability generating functions BibTeX for Inference in discrete probabilistic programs using probability generating functions
Bachelor’s thesis
Automatic verification of loop invariants in weighted programs
Ben Sturgis
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler, Kevin Batz
RWTH record for Automatic verification of loop invariants in weighted programs BibTeX for Automatic verification of loop invariants in weighted programs
Master’s thesis
Novelty-detection-based split selection heuristics for neural network verification
Caroline Jabs
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix, Marcel Moosbrugger
RWTH record for Novelty-detection-based split selection heuristics for neural network verification BibTeX for Novelty-detection-based split selection heuristics for neural network verification
Bachelor’s thesis
Comparison of heuristics for branching in neural network verification
Jonas Seidel
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Comparison of heuristics for branching in neural network verification BibTeX for Comparison of heuristics for branching in neural network verification
Master’s thesis
POMDP-based execution models for probabilistic programs with partial observability
Christina Gehnen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Alexander Nikolai Bork, Tobias Winkler
PDF of POMDP-based execution models for probabilistic programs with partial observability RWTH record for POMDP-based execution models for probabilistic programs with partial observability BibTeX for POMDP-based execution models for probabilistic programs with partial observability
Bachelor’s thesis
Verifying parametric Markov models using decision diagrams
Jan Erik Karuc
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Verifying parametric Markov models using decision diagrams BibTeX for Verifying parametric Markov models using decision diagrams
Master’s thesis
Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung
Denis Kuksaus
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung BibTeX for Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung
PhD thesis
Dynamic fault trees: semantics, analysis and applications
Matthias Volk
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Alessandro Cimatti
PDF of Dynamic fault trees: semantics, analysis and applications RWTH record for Dynamic fault trees: semantics, analysis and applications BibTeX for Dynamic fault trees: semantics, analysis and applications
Bachelor’s thesis
Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation
Dominic Sebastian Meiser
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation BibTeX for Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation
Bachelor’s thesis
Verification of leader election protocols for dynamic networks
Jan Jeremy Tugsbayar
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for Verification of leader election protocols for dynamic networks BibTeX for Verification of leader election protocols for dynamic networks
PhD thesis
Boolean-logic driven Markov processes : Explained. Analysed. Verified.
Shahid Khan
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Mariëlle Ida Antoinette Stoelinga
PDF of Boolean-logic driven Markov processes : Explained. Analysed. Verified.RWTH record for Boolean-logic driven Markov processes : Explained. Analysed. Verified.BibTeX for Boolean-logic driven Markov processes : Explained. Analysed. Verified.
Master’s thesis
Termination analysis of procedural pointer programs modelled by graph grammars
Mohamed Khalifa
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
PDF of Termination analysis of procedural pointer programs modelled by graph grammars RWTH record for Termination analysis of procedural pointer programs modelled by graph grammars BibTeX for Termination analysis of procedural pointer programs modelled by graph grammars
Bachelor’s thesis
Verification of neural networks using binary tree search for branching
Lisa Pühl
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Verification of neural networks using binary tree search for branching BibTeX for Verification of neural networks using binary tree search for branching
Master’s thesis
A unified slicing framework for probabilistic programs
Darion Haase
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for A unified slicing framework for probabilistic programs BibTeX for A unified slicing framework for probabilistic programs

2021

Bachelor’s thesis
Automata-based model checking of recursive systems
Christina Gehnen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Automata-based model checking of recursive systems RWTH record for Automata-based model checking of recursive systems BibTeX for Automata-based model checking of recursive systems
Master’s thesis
Underapproximations for indefinite-horizon POMDPS
Alexander Nikolai Bork
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Gerhard Lakemeyer
Consultants: Tim Quatmann
RWTH record for Underapproximations for indefinite-horizon POMDPS BibTeX for Underapproximations for indefinite-horizon POMDPS
Bachelor’s thesis
Analysis of concurrent probabilistic programs with shared variables
Fabian Gasser
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for Analysis of concurrent probabilistic programs with shared variables BibTeX for Analysis of concurrent probabilistic programs with shared variables
Master’s thesis
Decidability and complexity of entailment checking in quantitative separation logic
Marvin Jansen
RWTH Aachen University
Advisers: Kevin Batz, Ira Justus Fesefeldt, Christoph Matheja, Joost-Pieter Katoen, Thomas Noll
RWTH record for Decidability and complexity of entailment checking in quantitative separation logic BibTeX for Decidability and complexity of entailment checking in quantitative separation logic
Bachelor’s thesis
Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs
Patrick Arens
RWTH Aachen University
Advisers: Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll
RWTH record for Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs BibTeX for Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs
Master’s thesis
Efficient analysis of time-bounded reachability in markov automata
Mengying Xue
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Efficient analysis of time-bounded reachability in markov automata BibTeX for Efficient analysis of time-bounded reachability in markov automata
Bachelor’s thesis
Learning probabilistic automata with SMT solving
Dario Veltri
RWTH Aachen University
Advisers: Joshua Moerman, Joost-Pieter Katoen, Thomas Noll
PDF of Learning probabilistic automata with SMT solving RWTH record for Learning probabilistic automata with SMT solving BibTeX for Learning probabilistic automata with SMT solving

2020

Master’s thesis
Parameter synthesis in bayesian networks
Robin Drahovsky
RWTH Aachen University
Advisers: Bahare Salmani Barzoki, Joost-Pieter Katoen, Thomas Noll
RWTH record for Parameter synthesis in bayesian networks BibTeX for Parameter synthesis in bayesian networks
Master’s thesis
A petri net semantics for boolean-logic driven markov processes
Lars Beckers
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Shahid Khan
RWTH record for A petri net semantics for boolean-logic driven markov processes BibTeX for A petri net semantics for boolean-logic driven markov processes
Bachelor’s thesis
Dynamic fault tree analysis using binary decision diagrams
Daniel Basgöze
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Matthias Volk, Shahid Khan
PDF of Dynamic fault tree analysis using binary decision diagrams RWTH record for Dynamic fault tree analysis using binary decision diagrams BibTeX for Dynamic fault tree analysis using binary decision diagrams
Master’s thesis
Parameter synthesis in probabilistic timed automata
Bram Kohlen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Erika Ábrahám
Consultants: Jip Josephine Spel
RWTH record for Parameter synthesis in probabilistic timed automata BibTeX for Parameter synthesis in probabilistic timed automata
Bachelor’s thesis
RPrIC3: PrIC3 for expected rewards
Adrian Gallus
RWTH Aachen University
Advisers: Kevin Batz, Joost-Pieter Katoen, Thomas Noll
RWTH record for RPrIC3: PrIC3 for expected rewards BibTeX for RPrIC3: PrIC3 for expected rewards
Bachelor’s thesis
Implementation of a Predicate-Guided Termination Analysis for Pointer Programs
Mohamed Khalifa
RWTH Aachen University
Advisers: Ira Justus Fesefeldt, Thomas Noll, Joost-Pieter Katoen
PDF of Implementation of a Predicate-Guided Termination Analysis for Pointer Programs RWTH record for Implementation of a Predicate-Guided Termination Analysis for Pointer Programs BibTeX for Implementation of a Predicate-Guided Termination Analysis for Pointer Programs
Bachelor’s thesis
Gradient descent on parametric Markov Chains
Linus Heck
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll, Jip Josephine Spel
PDF of Gradient descent on parametric Markov Chains RWTH record for Gradient descent on parametric Markov Chains BibTeX for Gradient descent on parametric Markov Chains
Master’s thesis
Design and implementation of an interactive exploration tool for probabilistic programs
Alexander Hoppen
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Design and implementation of an interactive exploration tool for probabilistic programs BibTeX for Design and implementation of an interactive exploration tool for probabilistic programs
Bachelor’s thesis
Quantitative Analysis of Counterexample Generation for Automata Learning
Dan-Tuong Le
RWTH Aachen University
Advisers: Joshua Moerman, Joost-Pieter Katoen, Thomas Noll
PDF of Quantitative Analysis of Counterexample Generation for Automata Learning RWTH record for Quantitative Analysis of Counterexample Generation for Automata Learning BibTeX for Quantitative Analysis of Counterexample Generation for Automata Learning
Bachelor’s thesis
Learning RFSA in Reverse
Thomas Vogt
RWTH Aachen University
Advisers: Joshua Moerman, Joost-Pieter Katoen, Thomas Noll
RWTH record for Learning RFSA in Reverse BibTeX for Learning RFSA in Reverse
PhD thesis
Parameter synthesis in Markov models
Sebastian Junges
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Alessandro Abate, Javier Esparza
PDF of Parameter synthesis in Markov models RWTH record for Parameter synthesis in Markov models BibTeX for Parameter synthesis in Markov models
PhD thesis
Automated reasoning and randomization in separation logic
Christoph Matheja
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Radu Iosif
PDF of Automated reasoning and randomization in separation logic RWTH record for Automated reasoning and randomization in separation logic BibTeX for Automated reasoning and randomization in separation logic

2019

2018

PhD thesis
Model-based reliability analysis of aerospace systems
Harold Yorick Bruintjes
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Alessandro Cimatti
PDF of Model-based reliability analysis of aerospace systems RWTH record for Model-based reliability analysis of aerospace systems BibTeX for Model-based reliability analysis of aerospace systems
PhD thesis
IC3 software model checking
Tim Felix Lange
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Georg Weissenbacher, Martin R. Neuhäußer
PDF of IC3 software model checking RWTH record for IC3 software model checking BibTeX for IC3 software model checking
PhD thesis
The probabilistic model checker Storm : symbolic methods for probabilistic model checking
Hans Christian Hensel
RWTH Aachen University
Advisers: Joost-Pieter Katoen, David Parker
PDF of The probabilistic model checker Storm : symbolic methods for probabilistic model checking RWTH record for The probabilistic model checker Storm : symbolic methods for probabilistic model checking BibTeX for The probabilistic model checker Storm : symbolic methods for probabilistic model checking

2017

2016

PhD thesis
Semantics and loop invariant synthesis for probabilistic programs
Friedrich Gretz
Aachen, Techn. Hochsch.
Advisers: Joost-Pieter Katoen, Sriram Sankaranarayanan
PDF of Semantics and loop invariant synthesis for probabilistic programs RWTH record for Semantics and loop invariant synthesis for probabilistic programs BibTeX for Semantics and loop invariant synthesis for probabilistic programs

2015

PhD thesis
Verifying Java programs : a graph grammar approach
Jonathan Heinen
Verl. Dr. Hut
Advisers: Joost-Pieter Katoen, Arend Rensink
RWTH record for Verifying Java programs : a graph grammar approach BibTeX for Verifying Java programs : a graph grammar approach
PhD thesis
Counterexamples in probabilistic verification
Nils Jansen
Aachen, Techn. Hochsch.
Advisers: Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen
PDF of Counterexamples in probabilistic verification RWTH record for Counterexamples in probabilistic verification BibTeX for Counterexamples in probabilistic verification
PhD thesis
Abstraction and refinement of probabilistic automata using modal stochastic games
Falak Sher
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Lijun Zhang
PDF of Abstraction and refinement of probabilistic automata using modal stochastic games RWTH record for Abstraction and refinement of probabilistic automata using modal stochastic games BibTeX for Abstraction and refinement of probabilistic automata using modal stochastic games
PhD thesis
Reduction Techniques for Nondeterministic and Probabilistic Systems
Arpit Sharma
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Holger Hermanns
PDF of Reduction Techniques for Nondeterministic and Probabilistic Systems RWTH record for Reduction Techniques for Nondeterministic and Probabilistic Systems BibTeX for Reduction Techniques for Nondeterministic and Probabilistic Systems

2014

PhD thesis
Verifying probabilistic systems : new algorithms and complexity results
Hongfei Fu
Zugl.: Aachen, Techn. Hochsch.
Advisers: Joost-Pieter Katoen
PDF of Verifying probabilistic systems : new algorithms and complexity results RWTH record for Verifying probabilistic systems : new algorithms and complexity results BibTeX for Verifying probabilistic systems : new algorithms and complexity results

2013

PhD thesis
Trustworthy spacecraft design using formal methods
Viet Yen Nguyen
Dep. of Computer Science, RWTH Aachen
Advisers: Joost-Pieter Katoen
PDF of Trustworthy spacecraft design using formal methods RWTH record for Trustworthy spacecraft design using formal methods BibTeX for Trustworthy spacecraft design using formal methods
PhD thesis
Analyzing energy consumption of wireless networks : a model-based approach
Haidi Yue
Publikationsserver der RWTH Aachen University
Advisers: Joost-Pieter Katoen
PDF of Analyzing energy consumption of wireless networks : a model-based approach RWTH record for Analyzing energy consumption of wireless networks : a model-based approach BibTeX for Analyzing energy consumption of wireless networks : a model-based approach

2012

PhD thesis
Verification of continuous space stochastic systems
Alexandru Mereacre
Publikationsserver der RWTH Aachen University
Advisers: Joost-Pieter Katoen
PDF of Verification of continuous space stochastic systems RWTH record for Verification of continuous space stochastic systems BibTeX for Verification of continuous space stochastic systems

2010

PhD thesis
Three-valued abstraction for stochastic systems
Daniel Klink
Hut
Advisers: Joost-Pieter Katoen
PDF of Three-valued abstraction for stochastic systems RWTH record for Three-valued abstraction for stochastic systems BibTeX for Three-valued abstraction for stochastic systems
PhD thesis
Model checking nondeterministic and randomly timed systems
Martin R. Neuhäußer
Univ. Twente
Advisers: Joost-Pieter Katoen
PDF of Model checking nondeterministic and randomly timed systems RWTH record for Model checking nondeterministic and randomly timed systems BibTeX for Model checking nondeterministic and randomly timed systems

2009

PhD thesis
Diagnosis, synthesis and analysis of probabilistic models
Tingting Han
Univ. Twente
Advisers: Joost-Pieter Katoen
PDF of Diagnosis, synthesis and analysis of probabilistic models RWTH record for Diagnosis, synthesis and analysis of probabilistic models BibTeX for Diagnosis, synthesis and analysis of probabilistic models
PhD thesis
Verification of pointer programs
Stefan Rieger
Publikationsserver der RWTH Aachen University
Advisers: Joost-Pieter Katoen
PDF of Verification of pointer programs RWTH record for Verification of pointer programs BibTeX for Verification of pointer programs
PhD thesis
Learning communicating and nondeterministic automata
Carsten Kern
RWTH Aachen, Department of Computer Science
Advisers: Joost-Pieter Katoen
PDF of Learning communicating and nondeterministic automata RWTH record for Learning communicating and nondeterministic automata BibTeX for Learning communicating and nondeterministic automata

All records on RWTH Publications