Publications

2026

Conference paper
Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation
Nikolaus Vertovec, Frederik Baymler Mathiesen, Thom Badings, Luca Laurenti, Alessandro Abate
Annual Learning for Dynamics and Control Conference, 17-19 June 2026, Los Angeles, California, USA
RWTH record for Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation BibTeX for Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation
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
Journal article
Probabilistic programming meets automata theory: Exact inference using weighted automata
Dominik Geißler, Tobias Winkler
Theoretical computer science
PDF of Probabilistic programming meets automata theory: Exact inference using weighted automata RWTH record for Probabilistic programming meets automata theory: Exact inference using weighted automata BibTeX for Probabilistic programming meets automata theory: Exact inference using weighted automata
Conference paper
Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
Milan Češka, Sebastian Junges, Luko van der Maas, Filip Macák, Tim Quatmann
Computer Aided Verification
PDF of Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families RWTH record for Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families BibTeX for Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families
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
Conference paper
Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking
Arnd Hartmanns, Tim Quatmann, Mark van Wijk
Formal Methods
PDF of Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking RWTH record for Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking BibTeX for Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking
Conference paper
Correction to: Weighted Automata for Exact Inference in Discrete Probabilistic Programs
Dominik Geißler, Tobias Winkler
Theoretical Aspects of Computing – ICTAC 2025
RWTH record for Correction to: Weighted Automata for Exact Inference in Discrete Probabilistic Programs BibTeX for Correction to: Weighted Automata for Exact Inference in Discrete Probabilistic Programs
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
Patent
Verfahren zur Herstellung flächiger, poröser Hydrogele mittels Fluss-Lithographie
Matthias Wessling, Sebastian Brosch, Ann-Kathrin Mertens, Lea Maria Steinbeck, Richard Paul
RWTH record for Verfahren zur Herstellung flächiger, poröser Hydrogele mittels Fluss-Lithographie BibTeX for Verfahren zur Herstellung flächiger, poröser Hydrogele mittels Fluss-Lithographie
Journal article
The revised practitioner’s guide to MDP model checking algorithms
Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger
International journal on software tools for technology transfer
PDF of The revised practitioner’s guide to MDP model checking algorithms RWTH record for The revised practitioner’s guide to MDP model checking algorithms BibTeX for The revised practitioner’s guide to MDP model checking algorithms
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
Weighted Automata for Exact Inference in Discrete Probabilistic Programs
Dominik Geißler, Tobias Winkler
Theoretical Aspects of Computing – ICTAC 2025
RWTH record for Weighted Automata for Exact Inference in Discrete Probabilistic Programs BibTeX for Weighted Automata for Exact Inference in Discrete Probabilistic Programs
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

Journal article
Report on the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
Emma Katharina Ahrens, Jan-Christoph Kassing
ACM SIGLOG news
RWTH record for Report on the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)BibTeX for Report on the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)
Journal article
Report on Probability in Computer Science (PICS) 2024
Emma Katharina Ahrens, Christina Gehnen, Lena Franziska Verscht
ACM SIGLOG news
RWTH record for Report on Probability in Computer Science (PICS) 2024 BibTeX for Report on Probability in Computer Science (PICS) 2024
Conference paper
CertPHash: Towards Certified Perceptual Hashing via Robust Training
Yuchen Yang, Qichang Liu, Christopher Jan-Steffen Brix, Huan Zhang, Yinzhi Cao
Proceedings of the 34th USENIX Security Symposium
RWTH record for CertPHash: Towards Certified Perceptual Hashing via Robust Training BibTeX for CertPHash: Towards Certified Perceptual Hashing via Robust Training
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
Preprint
Partial Incorrectness Logic
Lena Verscht, Ānrán Wáng, Benjamin Lucien Kaminski
PDF of Partial Incorrectness Logic RWTH record for Partial Incorrectness Logic BibTeX for Partial Incorrectness Logic