Publications

2024
DOI fulltext PDF [bibtex]
@article{PSSRNPP2024,
title = {Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs},
author = {Kevin Batz and Tom Jannik Biskup and Joost-Pieter Katoen and Tobias Winkler},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {8},
pages = {pages 93},
type = {Journal Article},
year = {2024},
doi = {10.1145/3632935},
url = { https://publications.rwth-aachen.de/record/979194},
}×
[issue]
Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs, Proceedings of the ACM on programming languages 8, pages 93, ACM, 2024.
DOI [bibtex]
@article{PM2024,
title = {Parameter synthesis for Markov models: covering the parameter space},
author = {Sebastian Junges and Erika Ábrahám and Hans Christian Hensel and Nils Jansen and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {62(1/3)},
pages = {pages 181-259},
type = {Journal Article},
year = {2024},
doi = {10.1007/s10703-023-00442-x},
url = { https://publications.rwth-aachen.de/record/985754},
}×
[issue]
Sebastian Junges, Erika Ábrahám, Hans Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. Parameter synthesis for Markov models: covering the parameter space, Formal methods in system design 62 (1/3), pages 181-259, Springer, 2024.
DOI fulltext PDF [bibtex]
@article{EBILPPGF2024,
title = {Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions},
author = {Lutz Klinkenberg and Christian Blumenthal and Mingshuai Chen and Darion Haase and Joost-Pieter Katoen},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {8(OOPSLA1)},
pages = {pages 127},
type = {Journal Article},
year = {2024},
doi = {10.1145/3649844},
url = { https://publications.rwth-aachen.de/record/986464},
}×
[issue]
Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions, Proceedings of the ACM on programming languages 8 (OOPSLA1), pages 127, ACM, 2024.
DOI [bibtex]
@conference{SFTAVPMC2024,
title = {SAFEST: Fault Tree Analysis Via Probabilistic Model Checking},
author = {Matthias Volk and Falak Sher and Joost-Pieter Katoen and Mariëlle Stoelinga},
publisher = {IEEE},
type = {Conference Paper},
year = {2024},
doi = {10.1109/RAMS51492.2024.10457719},
url = { https://publications.rwth-aachen.de/record/988574},
}×
[issue]
Matthias Volk, Falak Sher, Joost-Pieter Katoen, Mariëlle Stoelinga. SAFEST: Fault Tree Analysis Via Probabilistic Model Checking, 2024 Annual Reliability and Maintainability Symposium (RAMS), IEEE, 2024.
DOI fulltext PDF [bibtex]
@conference{ACEVTSDMC2024,
title = {Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains},
author = {Hannah Mertens and Joost-Pieter Katoen and Tim Quatmann and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {14571},
pages = {237-257},
type = {Conference Paper},
year = {2024},
doi = {10.1007/978-3-031-57249-4_12},
url = { https://publications.rwth-aachen.de/record/990356},
}×
[issue]
Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains, 30. International Conference TACAS (TACAS 2024), Volume 14571 of LNCS, 237-257, Springer, 2024.
DOI [bibtex]
@conference{NSASMAS2024,
title = {Natural Strategic Ability in Stochastic Multi-Agent Systems},
author = {Raphael Jean Berthon and Joost-Pieter Katoen and Munyque Mittelmann and Aniello Murano},
publisher = {Association for the Advancement of Artificial Intelligence},
booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence},
volume = {38,16},
pages = {17308-17316},
type = {Conference Paper},
year = {2024},
doi = {10.1609/aaai.v38i16.29678},
url = { https://publications.rwth-aachen.de/record/992292},
}×
[issue]
Raphael Jean Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano. Natural Strategic Ability in Stochastic Multi-Agent Systems, 38. AAAI Conference on Artificial Intelligence (AAAI 2024), Volume 38,16 of Proceedings of the AAAI Conference on Artificial Intelligence, 17308-17316, Association for the Advancement of Artificial Intelligence, 2024.
arXiv:2401.12170 [bibtex]
@unpublished{NSASMAS2024,
title = {Natural Strategic Ability in Stochastic Multi-Agent Systems},
author = {Raphael Jean Berthon and Joost-Pieter Katoen and Munyque Mittelmann and Aniello Murano},
pages = {10 Seiten},
type = {Preprint},
year = {2024},
url = { https://arxiv.org/abs/2401.12170},
}×
[issue]
Raphael Jean Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano. Natural Strategic Ability in Stochastic Multi-Agent Systems, 10 Seiten, 2024. https://arxiv.org/abs/2401.12170
DOI fulltext PDF [bibtex]
@conference{LEBPRPS2024,
title = {Learning Explainable and Better Performing Representations of POMDP Strategies},
author = {Alexander Nikolai Bork and Debraj Chakraborty and Kush Grover and Jan Křetínský and Stefanie Mohr},
publisher = {Springer},
booktitle = {LNCS},
volume = {14571},
pages = {299-319},
type = {Conference Paper},
year = {2024},
doi = {10.1007/978-3-031-57249-4_15},
url = { https://publications.rwth-aachen.de/record/992671},
}×
[issue]
Alexander Nikolai Bork, Debraj Chakraborty, Kush Grover, Jan Křetínský, Stefanie Mohr. Learning Explainable and Better Performing Representations of POMDP Strategies, 30. International Conference TACAS (TACAS 2024), Volume 14571 of LNCS, 299-319, Springer, 2024.
2023
DOI arXiv:2302.00513 fulltext PDF [bibtex]
@unpublished{EPIUGF2023,
title = {Exact Probabilistic Inference Using Generating Functions},
author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen},
pages = {3 Seiten},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2302.00513},
url = { https://arxiv.org/abs/2302.00513},
}×
[issue]
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 3 Seiten, 2023. https://arxiv.org/abs/2302.00513
DOI fulltext PDF [bibtex]
@article{ACAER2023,
title = {A Calculus for Amortized Expected Runtimes},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Lena Verscht},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {7(POPL)},
pages = {pages 67},
type = {Journal Article},
year = {2023},
doi = {10.1145/3571260},
url = { https://publications.rwth-aachen.de/record/889639},
}×
[issue]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Lena Verscht. A Calculus for Amortized Expected Runtimes, Proceedings of the ACM on programming languages 7 (POPL), pages 67, ACM, 2023.
DOI fulltext PDF [bibtex]
@article{S2023,
title = {Stochastic games with lexicographic objectives},
author = {Krishnendu Chatterjee and Joost-Pieter Katoen and Stefanie Mohr and Maximilian Weininger and Tobias Winkler},
publisher = {Springer},
journal = {Formal methods in system design},
pages = {41 Seiten},
type = {Journal Article},
year = {2023},
doi = {10.1007/s10703-023-00411-4},
url = { https://publications.rwth-aachen.de/record/954240},
}×
[issue]
Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler. Stochastic games with lexicographic objectives, Formal methods in system design, 41 Seiten, Springer, 2023.
DOI fulltext PDF [bibtex]
@conference{PPVISII2023,
title = {Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants},
author = {Kevin Batz and Mingshuai Chen and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {13994},
pages = {410-429},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30820-8_25},
url = { https://publications.rwth-aachen.de/record/957952},
}×
[issue]
Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 410-429, Springer, 2023.
DOI fulltext PDF [bibtex]
@article{LBPDPP2023,
title = {Lower Bounds for Possibly Divergent Probabilistic Programs},
author = {Shenghua Feng and Mingshuai Chen and Han Su and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Naijun Zhan},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {7(OOPSLA1)},
pages = {pages 99},
type = {Journal Article},
year = {2023},
doi = {10.1145/3586051},
url = { https://publications.rwth-aachen.de/record/958360},
}×
[issue]
Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan. Lower Bounds for Possibly Divergent Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA1), pages 99, ACM, 2023.
DOI fulltext PDF [bibtex]
@article{T2023,
title = {The probabilistic termination tool amber},
author = {Marcel Moosbrugger and Ezio Bartocci and Joost-Pieter Katoen and Laura Kovács},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {61(1)},
pages = {pages 90-109},
type = {Journal Article},
year = {2023},
doi = {10.1007/s10703-023-00424-z},
url = { https://publications.rwth-aachen.de/record/959110},
}×
[issue]
Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács. The probabilistic termination tool amber, Formal methods in system design 61 (1), pages 90-109, Springer, 2023.
DOI fulltext PDF [bibtex]
@article{FVC2023,
title = {First three years of the international verification of neural networks competition (VNN-COMP)},
author = {Christopher Jan-Steffen Brix and Mark Niklas Müller and Stanley Bak and Taylor T. Johnson and Changliu Liu},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {25},
pages = {pages 329-339},
type = {Journal Article},
year = {2023},
doi = {10.1007/s10009-023-00703-4},
url = { https://publications.rwth-aachen.de/record/960369},
}×
[issue]
Christopher Jan-Steffen Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, Changliu Liu. First three years of the international verification of neural networks competition (VNN-COMP), International journal on software tools for technology transfer 25, pages 329-339, Springer, 2023.
DOI fulltext PDF [bibtex]
@conference{SESPSP2023,
title = {Search and Explore: Symbiotic Policy Synthesis in POMDPs},
author = {Roman Andriushchenko and Alexander Nikolai Bork and Milan Češka and Sebastian Junges and Joost-Pieter Katoen and Filip Macák},
publisher = {Springer},
booktitle = {LNCS},
volume = {13966},
pages = {113-135},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-37709-9_6},
url = { https://publications.rwth-aachen.de/record/968844},
}×
[issue]
Roman Andriushchenko, Alexander Nikolai Bork, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Filip Macák. Search and Explore: Symbiotic Policy Synthesis in POMDPs, 35. International Conference on Computer-Aided Verification (CAV 2023), Volume 13966 of LNCS, 113-135, Springer, 2023.
DOI fulltext PDF [bibtex]
@article{AFRPBN2023,
title = {Automatically Finding the Right Probabilities in Bayesian Networks},
author = {Bahare Salmani Barzoki and Joost-Pieter Katoen},
publisher = {AI Access Found.},
journal = {Journal of artificial intelligence research},
volume = {77},
pages = {pages 1637-1696},
type = {Journal Article},
year = {2023},
doi = {10.1613/jair.1.14044},
url = { https://publications.rwth-aachen.de/record/969130},
}×
[issue]
Bahare Salmani Barzoki, Joost-Pieter Katoen. Automatically Finding the Right Probabilities in Bayesian Networks, Journal of artificial intelligence research 77, pages 1637-1696, AI Access Found., 2023.
DOI [bibtex]
@conference{APGMMCA2023,
title = {A Practitioner’s Guide to MDP Model Checking Algorithms},
author = {Arnd Hartmanns and Sebastian Junges and Tim Quatmann and Maximilian Weininger},
publisher = {Springer},
booktitle = {LNCS},
volume = {13993},
pages = {469-488},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30823-9_24},
url = { https://publications.rwth-aachen.de/record/972074},
}×
[issue]
Arnd Hartmanns, Sebastian Junges, Tim Quatmann, Maximilian Weininger. A Practitioner’s Guide to MDP Model Checking Algorithms, International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13993 of LNCS, 469-488, Springer, 2023.
DOI fulltext PDF [bibtex]
@proceedings{KPGP2023,
title = {22. Kolloquium Programmiersprachen und Grundlagen der Programmierung},
author = {},
editor = {Thomas Noll and Ira Justus Fesefeldt},
publisher = {RWTH Aachen University, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {AIB-2023-03},
pages = {1 Online-Ressource},
type = {Proceeding Article},
year = {2023},
doi = {10.18154/RWTH-2023-10034},
url = { https://publications.rwth-aachen.de/record/972197},
}×
[issue]
Thomas Noll (ed), Ira Justus Fesefeldt (ed). 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung, Volume AIB-2023-03 of Aachener Informatik-Berichte, 1 Online-Ressource, RWTH Aachen University, Department of Computer Science, 2023.
DOI fulltext PDF [bibtex]
@conference{CPPAOVI2023,
title = {Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration},
author = {Tobias Winkler and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13994},
pages = {391-409},
type = {Conference Paper},
year = {2023},
doi = {10.1007/978-3-031-30820-8_24},
url = { https://publications.rwth-aachen.de/record/972636},
}×
[issue]
Tobias Winkler, Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 391-409, Springer, 2023.
DOI [bibtex]
@conference{OCERTPPA2023,
title = {On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata},
author = {Tobias Winkler and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {13 Seiten},
type = {Conference Paper},
year = {2023},
doi = {10.1109/LICS56636.2023.10175714},
url = { https://publications.rwth-aachen.de/record/972664},
}×
[issue]
Tobias Winkler, Joost-Pieter Katoen. On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata, 38. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), 13 Seiten, IEEE, 2023.
DOI fulltext PDF [bibtex]
@article{ADVIPP2023,
title = {A Deductive Verification Infrastructure for Probabilistic Programs},
author = {Philipp Schroer and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {7(OOPSLA2)},
pages = {pages 294},
type = {Journal Article},
year = {2023},
doi = {10.1145/3622870},
url = { https://publications.rwth-aachen.de/record/973293},
}×
[issue]
Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs, Proceedings of the ACM on programming languages 7 (OOPSLA2), pages 294, ACM, 2023.
DOI arXiv:2309.07781 fulltext PDF [bibtex]
@unpublished{ADVIPPEV2023,
title = {A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version)},
author = {Philipp Schroer and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
pages = {[1]-48},
type = {Preprint},
year = {2023},
doi = {10.48550/arXiv.2309.07781},
url = { https://arxiv.org/abs/2309.07781},
}×
[issue]
Philipp Schroer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A Deductive Verification Infrastructure for Probabilistic Programs (Extended Version), [1]-48, 2023. https://arxiv.org/abs/2309.07781
DOI fulltext PDF [bibtex]
@article{MCTPRPP2023,
title = {Model Checking Temporal Properties of Recursive Probabilistic Programs},
author = {Tobias Winkler and Christina Gehnen and Joost-Pieter Katoen},
publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig},
journal = {Logical methods in computer science},
volume = {19(4)},
pages = {pages 24},
type = {Journal Article},
year = {2023},
doi = {10.46298/lmcs-19(4:24)2023},
url = { https://publications.rwth-aachen.de/record/976967},
}×
[issue]
Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Logical methods in computer science 19 (4), pages 24, Department of Theoretical Computer Science, Technical University of Braunschweig, 2023.
arXiv:2307.07314 [bibtex]
@unpublished{EBILPPGF2023,
title = {Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions},
author = {Lutz Klinkenberg and Christian Blumenthal and Mingshuai Chen and Darion Haase and Joost-Pieter Katoen},
pages = {54 Seiten},
type = {Preprint},
year = {2023},
url = { https://arxiv.org/abs/2307.07314},
}×
[issue]
Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions, 54 Seiten, 2023. https://arxiv.org/abs/2307.07314
DOI [bibtex]
@proceedings{FM2023,
title = {Formal Methods},
author = {},
editor = {Marsha Chechik and Joost-Pieter Katoen and Martin Leucker},
publisher = {Springer},
booktitle = {LNCS},
volume = {14000},
pages = {xvi, 659 Seiten : Diagramme},
type = {Proceeding Article},
year = {2023},
doi = {10.1007/978-3-031-27481-7},
url = { https://publications.rwth-aachen.de/record/990325},
}×
[issue]
Marsha Chechik (ed), Joost-Pieter Katoen (ed), Martin Leucker (ed). Formal Methods, Volume 14000 of LNCS, xvi, 659 Seiten : Diagramme, Springer, 2023.
DOI [bibtex]
@conference{FCMVPBN2023,
title = {Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks},
author = {Bahare Salmani Barzoki and Joost-Pieter Katoen},
publisher = {International Joint Conferences on Artificial Intelligence},
type = {Conference Paper},
year = {2023},
doi = {10.24963/ijcai.2023/635},
url = { https://publications.rwth-aachen.de/record/990327},
}×
[issue]
Bahare Salmani Barzoki, Joost-Pieter Katoen. Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks, 32. International Joint Conference on Artificial Intelligence (IJCAI 2023), International Joint Conferences on Artificial Intelligence, 2023.
[bibtex]
@conference{PBNNP2023,
title = {Provably Bounding Neural Network Preimages},
author = {Suhas Kotha and Christopher Jan-Steffen Brix and Zico Kolter and Krishnamurthy (Dj Dvijotham and Huan Zhang},
booktitle = {Advances in Neural Information Processing Systems},
type = {Conference Paper},
year = {2023},
url = { https://publications.rwth-aachen.de/record/993058},
}×
[issue]
Suhas Kotha, Christopher Jan-Steffen Brix, Zico Kolter, Krishnamurthy (Dj Dvijotham, Huan Zhang. Provably Bounding Neural Network Preimages, 37. Conference on Neural Information Processing Systems (NeurIPS), Advances in Neural Information Processing Systems, 2023.
Show all