Publications

2021

Conference paper
A Debugger for Probabilistic Programs
Alexander Hoppen, Thomas Noll
Software Engineering and Formal Methods
RWTH record for A Debugger for Probabilistic Programs BibTeX for A Debugger for Probabilistic Programs
Conference paper
A Modular Approach to Non-deterministic Dynamic Fault Trees
Sascha Müller, Adeline Jordon, Andreas Gerndt, Thomas Noll
Computer Safety, Reliability, and Security
RWTH record for A Modular Approach to Non-deterministic Dynamic Fault Trees BibTeX for A Modular Approach to Non-deterministic Dynamic Fault Trees
Conference paper
Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs
Muhammad Hannan Khan, Osman Hassan, Shahid Khan
Theoretical aspects of computing - ICTAC 2021
RWTH record for Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs BibTeX for Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs
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
On Correctness, Precision, and Performance in Quantitative Verification : QComp 2020 Competition Report
Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Křetínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang
Leveraging Applications of Formal Methods, Verification and Validation
RWTH record for On Correctness, Precision, and Performance in Quantitative Verification : QComp 2020 Competition Report BibTeX for On Correctness, Precision, and Performance in Quantitative Verification : QComp 2020 Competition Report
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
Stochastic Games with Disjunctions of Multiple Objectives
Tobias Winkler, Maximilian Weininger
Proceedings of the 12th International Symposium on Games, Automata, Logics, and Formal Verification
PDF of Stochastic Games with Disjunctions of Multiple Objectives RWTH record for Stochastic Games with Disjunctions of Multiple Objectives BibTeX for Stochastic Games with Disjunctions of Multiple Objectives
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
Conference paper
Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars
Ira Justus Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte
Graph Transformation
RWTH record for Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars BibTeX for Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars
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
Preprint
Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata
Mikołaj Bojańczyk, Bartek Klin, Joshua Moerman
PDF of Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata RWTH record for Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata BibTeX for Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata
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
Journal article
Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer
Journal of Logical and Algebraic Methods in Programming
PDF of Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings RWTH record for Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings BibTeX for Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
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
Journal article
Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control
Mingshuai Chen, Martin Fränzle, Yangjia Li, Peter N. Mosaad, Naijun Zhan
Acta informatica
PDF of Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control RWTH record for Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control BibTeX for Indecision and delays are the parents of failure - taming them algorithmically by synthesizing delay-resilient control

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