Publications

2022
DOI fulltext PDF [bibtex]
@book{NWIR2022,
title = {Nachhaltigen Wandel gestalten: Innovationsimpulse der RWTH},
author = {Thorsten Karbach and Agnes Förster and Eva Christine Strobel and Stefan Karl Josef Böschen and Peter Letmathe and Elisabeth Clausen and Rik W. de Doncker and Peter Lürkens and Albert Moser and Aaron Jonathan Praktiknjo and Fabian Roemer and Andreas Ulbig and Rainer Dahlmann and Thomas Fischöder and Stefanie Gottuck and Jürgen Klankermeyer and Felix Kunz and Regina Palkovits and Stefan Sterlepper and Peter Quicker and Matthias Jarke and Max C. Lemme and Saskia K. Nagel and Joost-Pieter Katoen and Rainer Waser and Matthias Brockmann and Melanie Sarah Katharina Buchsbaum and Christian Rüdiger Hinke and Patrick Mattfield and Edgar Dahl and Fabian Kiessling and Holger Jahr and Jonas Gesenhues and Joachim Jankowski and Mare Mechelinck and Heidi Noels and Irene Neuner and Rolf Rossaint and Stefan Uhlig and Tanja Veselinović and Emiel van der Vorst and Maximilian Alfons Voshage and Dirk Abel and Claus Bonerz and Lutz Eckstein and Bastian Lehrheuer and Micha Lesemann and Tobias Ostermann and René Zweigel and Benjamin Daniels and Frank Lehmkuhl and Michael Leuchner and Frank Lohrberg and Henry Riße and Martina Roß-Nickoll and Thomas Josef Wintgens},
publisher = {RWTH Aachen University},
pages = {145 Seiten : Illustrationen},
type = {Book},
year = {2022},
doi = {10.18154/RWTH-2021-11153},
url = { https://publications.rwth-aachen.de/record/836209},
}×
[issue] 		Alena Beatrice Cohrs, Jose Miguel Sanchez-Molero Martinez, Maren Paegert, 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 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. Nachhaltigen Wandel gestalten: Innovationsimpulse der RWTH, 145 Seiten : Illustrationen, RWTH Aachen University, 2022.
DOI [bibtex]
@conference{OCRPMCSE2022,
title = {Out of Control: Reducing Probabilistic Models by Control-State Elimination},
author = {Tobias Winkler and Johannes Lehmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13182, Theoretical Computer Science and General Issues},
pages = {450-472},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-94583-1_22},
url = { https://publications.rwth-aachen.de/record/838775},
}×
[issue] 		Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen. Out of Control: Reducing Probabilistic Models by Control-State Elimination, 23. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), Volume 13182, Theoretical Computer Science and General Issues of LNCS, 450-472, Springer, 2022.
DOI fulltext PDF [bibtex]
@article{RLNNA2022,
title = {Residuality and Learning for Nondeterministic Nominal Automata},
author = {Joshua Moerman and Matteo Sammartino},
publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig},
journal = {Logical methods in computer science},
volume = {18(1)},
pages = {pages 29},
type = {Journal Article},
year = {2022},
doi = {10.46298/lmcs-18(1:29)2022},
url = { https://publications.rwth-aachen.de/record/841706},
}×
[issue] 		Joshua Moerman, Matteo Sammartino. Residuality and Learning for Nondeterministic Nominal Automata, Logical methods in computer science 18 (1), pages 29, Department of Theoretical Computer Science, Technical University of Braunschweig, 2022.
DOI [bibtex]
@conference{GDRCUPO2022,
title = {Gradient-Descent for Randomized Controllers Under Partial Observability},
author = {Linus Heck and Jip Josephine Spel and Sebastian Junges and Joshua Moerman and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13182, Theoretical Computer Science and General Issues},
pages = {127-150},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-94583-1_7},
url = { https://publications.rwth-aachen.de/record/841719},
}×
[issue] 		Linus Heck, Jip Josephine Spel, Sebastian Junges, Joshua Moerman, Joost-Pieter Katoen. Gradient-Descent for Randomized Controllers Under Partial Observability, 23. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), Volume 13182, Theoretical Computer Science and General Issues of LNCS, 127-150, Springer, 2022.
DOI fulltext PDF [bibtex]
@conference{MCTPRPP2022,
title = {Model Checking Temporal Properties of Recursive Probabilistic Programs},
author = {Tobias Winkler and Christina Gehnen and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13242},
pages = {449-469},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-99253-8_23},
url = { https://publications.rwth-aachen.de/record/843600},
}×
[issue] 		Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Foundations of Software Science and Computation Structures, Volume 13242 of LNCS, 449-469, Springer, 2022.
DOI fulltext PDF [bibtex]
@conference{FECQSL2022,
title = {Foundations for Entailment Checking in Quantitative Separation Logic},
author = {Kevin Batz and Ira Justus Fesefeldt and Marvin Jansen and Joost-Pieter Katoen and Florian Keßler and Christoph Matheja and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {13240},
pages = {57-84},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-99336-8_3},
url = { https://publications.rwth-aachen.de/record/843799},
}×
[issue] 		Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll. Foundations for Entailment Checking in Quantitative Separation Logic, 31. European Symposium on Programming (ESOP 2022), Volume 13240 of LNCS, 57-84, Springer, 2022.
DOI fulltext PDF [bibtex]
@article{D2022,
title = {DFT modeling approach for operational risk assessment of railway infrastructure},
author = {Norman Weik and Matthias Volk and Joost-Pieter Katoen and Nils Nießen},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {24(3)},
pages = {pages 331-350},
type = {Journal Article},
year = {2022},
doi = {10.1007/s10009-022-00652-4},
url = { https://publications.rwth-aachen.de/record/844073},
}×
[issue] 		Norman Weik, Matthias Volk, Joost-Pieter Katoen, Nils Nießen. DFT modeling approach for operational risk assessment of railway infrastructure, International journal on software tools for technology transfer 24 (3), pages 331-350, Springer, 2022.
DOI fulltext PDF [bibtex]
@conference{UAETRP2022,
title = {Under-Approximating Expected Total Rewards in POMDPs},
author = {Alexander Nikolai Bork and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
booktitle = {LNCS},
volume = {13244},
pages = {22-40},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-99527-0_2},
url = { https://publications.rwth-aachen.de/record/844526},
}×
[issue] 		Alexander Nikolai Bork, Joost-Pieter Katoen, Tim Quatmann. Under-Approximating Expected Total Rewards in POMDPs, 28. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2022), Volume 13244 of LNCS, 22-40, Springer, 2022.
DOI fulltext PDF [bibtex]
@article{W2022,
title = {Weighted programming: a programming paradigm for specifying mathematical models},
author = {Kevin Batz and Adrian Gallus and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Tobias Winkler},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
pages = {pages 66},
type = {Journal Article},
year = {2022},
doi = {10.1145/3527310},
url = { https://publications.rwth-aachen.de/record/845157},
}×
[issue] 		Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models, Proceedings of the ACM on programming languages, pages 66, ACM, 2022.
fulltext PDF [bibtex]
@article{EDPIK2022,
title = {Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen"},
author = {Simon Schotten and Thorsten Büker and Wiebke Lenze and Bastian Kogel and Thomas Noll and Mario Fietze and Jana Berger},
publisher = {DVV Media Group, Eurailpress},
journal = {Eisenbahntechnische Rundschau},
volume = {71(5)},
pages = {pages 33-37},
type = {Journal Article},
year = {2022},
url = { https://publications.rwth-aachen.de/record/847020},
}×
[issue] 		Simon Schotten, Thorsten Büker, Wiebke Lenze, Bastian Kogel, Thomas Noll, Mario Fietze, Jana Berger. Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen", Eisenbahntechnische Rundschau 71 (5), pages 33-37, DVV Media Group, Eurailpress, 2022.
DOI [bibtex]
@conference{DPYRDVPPGF2022,
title = {Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions},
author = {Mingshuai Chen and Joost-Pieter Katoen and Lutz Klinkenberg and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {13371},
pages = {79-101},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-13185-1_5},
url = { https://publications.rwth-aachen.de/record/848175},
}×
[issue] 		Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions, 34. International Conference on Computer Aided Verification (CAV 2022), Volume 13371 of LNCS, 79-101, Springer, 2022.
DOI [bibtex]
@conference{CBCMC2022,
title = {Configurable Benchmarks for C Model Checkers},
author = {Xaver Fink and Philipp Berger and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13260},
pages = {338-354},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-06773-0_18},
url = { https://publications.rwth-aachen.de/record/848928},
}×
[issue] 		Xaver Fink, Philipp Berger, Joost-Pieter Katoen. Configurable Benchmarks for C Model Checkers, 14. International Symposium NASA Formal Methods (NFM 2022), Volume 13260 of LNCS, 338-354, Springer, 2022.
DOI fulltext PDF [bibtex]
@conference{TCQSL2022,
title = {Towards Concurrent Quantitative Separation Logic},
author = {Ira Justus Fesefeldt and Joost-Pieter Katoen and Thomas Noll},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
booktitle = {LIPIcs - Leibniz International Proceedings in Informatics},
volume = {243},
pages = {25:1-25:24},
type = {Conference Paper},
year = {2022},
doi = {10.4230/LIPICS.CONCUR.2022.25},
url = { https://publications.rwth-aachen.de/record/853299},
}×
[issue] 		Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, 33. International Conference on Concurrency Theory (CONCUR 2022), Volume 243 of LIPIcs - Leibniz International Proceedings in Informatics, 25:1-25:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022.
DOI arXiv:2207.02822 fulltext PDF [bibtex]
@unpublished{TCQSL2022,
title = {Towards Concurrent Quantitative Separation Logic},
author = {Ira Justus Fesefeldt and Joost-Pieter Katoen and Thomas Noll},
pages = {[1]-62},
type = {Preprint},
year = {2022},
doi = {10.18154/RWTH-2022-08799},
url = { https://arxiv.org/abs/2207.02822},
}×
[issue] 		Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll. Towards Concurrent Quantitative Separation Logic, [1]-62, 2022. https://arxiv.org/abs/2207.02822
fulltext PDF [bibtex]
@techreport{JSIRAESTB2022,
title = {50 Jahre Studiengang Informatik an der RWTH Aachen: Ein Streifzug in Text und Bild},
author = {},
publisher = {Fachgruppe Informatik in der Fakultät für Mathematik, Informatik und Naturwissenschaften der RWTH Aachen},
pages = {152 Seiten : Illustrationen, Diagramme},
type = {Tech Report},
year = {2022},
url = { https://publications.rwth-aachen.de/record/853722},
}×
[issue] 		Helene-Maria Bolke-Hermanns, Klaus Indermark, Joost-Pieter Katoen, Stefan Kowalewski, Thomas Noll, Wolfgang Thomas. 50 Jahre Studiengang Informatik an der RWTH Aachen: Ein Streifzug in Text und Bild, 152 Seiten : Illustrationen, Diagramme, Fachgruppe Informatik in der Fakultät für Mathematik, Informatik und Naturwissenschaften der RWTH Aachen, 2022.
DOI [bibtex]
@article{ES2022,
title = {Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Information and computation},
volume = {289(A)},
pages = {pages 104965},
type = {Journal Article},
year = {2022},
doi = {10.1016/j.ic.2022.104965},
url = { https://publications.rwth-aachen.de/record/853946},
}×
[issue] 		Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen. Encoding inductive invariants as barrier certificates: Synthesis via difference-of-convex programming, Information and computation 289 (A), pages 104965, Elsevier, 2022.
DOI [bibtex]
@conference{PCOB2022,
title = {POMDP Controllers with Optimal Budget},
author = {Jip Josephine Spel and Svenja Maria Stein and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13479},
pages = {107-130},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-16336-4_6},
url = { https://publications.rwth-aachen.de/record/854105},
}×
[issue] 		Jip Josephine Spel, Svenja Maria Stein, Joost-Pieter Katoen. POMDP Controllers with Optimal Budget, 19. International Conference on Quantitative Evaluation of SysTems (QEST 2022), Volume 13479 of LNCS, 107-130, Springer, 2022.
DOI [bibtex]
@conference{ACBRIEM2022,
title = {Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining},
author = {Philipp Berger and Wiebke Lenze and Thomas Noll and Simon Schotten and Thorsten Büker and Mario Fietze and Bastian Kogel},
publisher = {Springer},
booktitle = {LNCS},
volume = {13487},
pages = {121-133},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-15008-1_9},
url = { https://publications.rwth-aachen.de/record/854106},
}×
[issue] 		Philipp Berger, Wiebke Lenze, Thomas Noll, Simon Schotten, Thorsten Büker, Mario Fietze, Bastian Kogel. Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining, 27. International Conference Formal Methods for Industrial Critical Systems (FMICS 2022), Volume 13487 of LNCS, 121-133, Springer, 2022.
DOI fulltext PDF [bibtex]
@article{SM2022,
title = {Scenario-based verification of uncertain parametric MDPs},
author = {Thom Badings and Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
type = {Journal Article},
year = {2022},
doi = {10.1007/s10009-022-00673-z},
url = { https://publications.rwth-aachen.de/record/854160},
}×
[issue] 		Thom Badings, Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Scenario-based verification of uncertain parametric MDPs, International journal on software tools for technology transfer, Springer, 2022.
2021
fulltext PDF [bibtex]
@conference{GFPP2021,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
publisher = {Springer},
booktitle = {Theoretical Computer Science and General Issues},
volume = {12561},
pages = {231-248},
type = {Conference Paper},
year = {2021},
url = { https://publications.rwth-aachen.de/record/807881},
}×
[issue] 		Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 30. International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020), Volume 12561 of Theoretical Computer Science and General Issues, 231-248, Springer, 2021.
DOI fulltext PDF [bibtex]
@book{F2021,
title = {Foundations of probabilistic programming},
author = {},
editor = {Gilles Barthe and Joost-Pieter Katoen and Alexandra Silva},
publisher = {Cambridge University Press},
pages = {xiv, 568 Seiten : Illustrationen},
type = {Book},
year = {2021},
doi = {10.1017/9781108770750},
url = { https://publications.rwth-aachen.de/record/814578},
}×
[issue] 		Gilles Barthe (ed), Joost-Pieter Katoen (ed), Alexandra Silva (ed). Foundations of probabilistic programming, xiv, 568 Seiten : Illustrationen, Cambridge University Press, 2021.
DOI fulltext PDF [bibtex]
@article{D2021,
title = {Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
publisher = {Elsevier Science},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {119},
pages = {pages 100633},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jlamp.2020.100633},
url = { https://publications.rwth-aachen.de/record/816049},
}×
[issue] 		Erika Ábrahám, James H. Davenport, Matthew England, Gereon Kremer. Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings, Journal of Logical and Algebraic Methods in Programming 119, pages 100633, Elsevier Science, 2021.
DOI [bibtex]
@article{TM2021,
title = {The complexity of reachability in parametric Markov decision processes},
author = {Sebastian Junges and Joost-Pieter Katoen and Guillermo A. Pérez and Tobias Winkler},
publisher = {Elsevier},
journal = {Journal of computer and system sciences},
volume = {119},
pages = {pages 183-210},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jcss.2021.02.006},
url = { https://publications.rwth-aachen.de/record/816179},
}×
[issue] 		Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, Tobias Winkler. The complexity of reachability in parametric Markov decision processes, Journal of computer and system sciences 119, pages 183-210, Elsevier, 2021.
DOI fulltext PDF [bibtex]
@article{R2021,
title = {Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {5},
pages = {pages 39},
type = {Journal Article},
year = {2021},
doi = {10.1145/3434320},
url = { https://publications.rwth-aachen.de/record/816245},
}×
[issue] 		Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning, Proceedings of the ACM on programming languages 5, pages 39, ACM, 2021.
DOI [bibtex]
@article{M2021,
title = {Markov automata with multiple objectives},
author = {Tim Quatmann and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal methods in system design},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10703-021-00364-6},
url = { https://publications.rwth-aachen.de/record/816671},
}×
[issue] 		Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov automata with multiple objectives, Formal methods in system design, Springer, 2021.
DOI arXiv:2104.02438 fulltext PDF [bibtex]
@unpublished{OFDVSWRA2021,
title = {Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata},
author = {Mikołaj Bojańczyk and Bartek Klin and Joshua Moerman},
pages = {16 Seiten},
type = {Preprint},
year = {2021},
doi = {10.18154/RWTH-2021-03671},
url = { https://arxiv.org/abs/2104.02438},
}×
[issue] 		Mikołaj Bojańczyk, Bartek Klin, Joshua Moerman. Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata, 16 Seiten, 2021. https://arxiv.org/abs/2104.02438
DOI fulltext PDF [bibtex]
@conference{MOLATR2021,
title = {Multi-objective Optimization of Long-run Average and Total Rewards},
author = {Tim Quatmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12651},
pages = {230-249},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-72016-2_13},
url = { https://publications.rwth-aachen.de/record/817768},
}×
[issue] 		Tim Quatmann, Joost-Pieter Katoen. Multi-objective Optimization of Long-run Average and Total Rewards, 27. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Volume 12651 of LNCS, 230-249, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{FPOMC2021,
title = {Finding Provably Optimal Markov Chains},
author = {Jip Josephine Spel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12651},
pages = {173-190},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-72016-2_10},
url = { https://publications.rwth-aachen.de/record/818128},
}×
[issue] 		Jip Josephine Spel, Sebastian Junges, Joost-Pieter Katoen. Finding Provably Optimal Markov Chains, 27. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2021), Volume 12651 of LNCS, 173-190, Springer, 2021.
DOI fulltext PDF [bibtex]
@article{A2021,
title = {A pre-expectation calculus for probabilistic sensitivity},
author = {Alejandro Aguirre and Gilles Barthe and Justin Hsu and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Association for Computing Machinery},
journal = {Proceedings of the ACM on programming languages},
volume = {5(POPL)},
pages = {pages 52},
type = {Journal Article},
year = {2021},
doi = {10.1145/3434333},
url = { https://publications.rwth-aachen.de/record/819375},
}×
[issue] 		Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. A pre-expectation calculus for probabilistic sensitivity, Proceedings of the ACM on programming languages 5 (POPL), pages 52, Association for Computing Machinery, 2021.
DOI [bibtex]
@article{C2021,
title = {Counterexample-guided inductive synthesis for probabilistic systems},
author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal aspects of computing},
volume = {33(4/5)},
pages = {pages 637-667},
type = {Journal Article},
year = {2021},
doi = {10.1007/s00165-021-00547-2},
url = { https://publications.rwth-aachen.de/record/820111},
}×
[issue] 		Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-guided inductive synthesis for probabilistic systems, Formal aspects of computing 33 (4/5), pages 637-667, Springer, 2021.
DOI [bibtex]
@conference{ACCBCHRG2021,
title = {Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars},
author = {Ira Justus Fesefeldt and Christoph Matheja and Thomas Noll and Johannes Schulte},
publisher = {Springer},
booktitle = {LNCS},
volume = {12741},
pages = {283-293},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-78946-6_15},
url = { https://publications.rwth-aachen.de/record/820755},
}×
[issue] 		Ira Justus Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte. Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars, 14. International Conference on Graph Transformation (ICGT21), Volume 12741 of LNCS, 283-293, Springer, 2021.
DOI fulltext PDF [bibtex]
@article{TS2021,
title = {The probabilistic model checker STORM},
author = {Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Matthias Volk},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {24(4)},
pages = {pages 589-610},
type = {Journal Article},
year = {2021},
doi = {10.1007/s10009-021-00633-z},
url = { https://publications.rwth-aachen.de/record/822059},
}×
[issue] 		Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Matthias Volk. The probabilistic model checker STORM, International journal on software tools for technology transfer 24 (4), pages 589-610, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{SIBCDCP2021,
title = {Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming},
author = {Qiuye Wang and Mingshuai Chen and Bai Xue and Naijun Zhan and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12759, Theoretical Computer Science and General Issues},
pages = {443-466},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81685-8_21},
url = { https://publications.rwth-aachen.de/record/822586},
}×
[issue] 		Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, Joost-Pieter Katoen. Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming, 33. International Conference on Computer-Aided Verification (CAV 2021), Volume 12759, Theoretical Computer Science and General Issues of LNCS, 443-466, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{LIAPP2021,
title = {Latticed $k$-Induction with an Application to Probabilistic Programs},
author = {Kevin Batz and Mingshuai Chen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12760},
pages = {524-549},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81688-9_25},
url = { https://publications.rwth-aachen.de/record/822587},
}×
[issue] 		Kevin Batz, Mingshuai Chen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. Latticed $k$-Induction with an Application to Probabilistic Programs, 33. International Conference on Computer-Aided Verification (CAV 2021), Volume 12760 of LNCS, 524-549, Springer, 2021.
DOI arXiv:2109.08317 fulltext PDF [bibtex]
@conference{SGDMO2021,
title = {Stochastic Games with Disjunctions of Multiple Objectives},
author = {Tobias Winkler and Maximilian Weininger},
publisher = {NICTA},
booktitle = {EPTCS},
volume = {346},
pages = {85-100},
type = {Conference Paper},
year = {2021},
doi = {10.4204/EPTCS.346.6},
url = { https://arxiv.org/abs/2109.08317},
}×
[issue] 		Tobias Winkler, Maximilian Weininger. Stochastic Games with Disjunctions of Multiple Objectives, 12. International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Volume 346 of EPTCS, 85-100, NICTA, 2021.
DOI [bibtex]
@conference{TOPTA2021,
title = {Tweaking the Odds in Probabilistic Timed Automata},
author = {Arnd Hartmanns and Joost-Pieter Katoen and Bram Kohlen and Jip Josephine Spel},
publisher = {Springer},
booktitle = {LNCS},
volume = {12846},
pages = {39-58},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-85172-9_3},
url = { https://publications.rwth-aachen.de/record/828609},
}×
[issue] 		Arnd Hartmanns, Joost-Pieter Katoen, Bram Kohlen, Jip Josephine Spel. Tweaking the Odds in Probabilistic Timed Automata, 18. International Conference on Quantitative Evaluation of Systems (QEST 2021), Volume 12846 of LNCS, 39-58, Springer, 2021.
DOI [bibtex]
@conference{FTOBN2021,
title = {Fine-Tuning the Odds in Bayesian Networks},
author = {Bahare Salmani Barzoki and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12897},
pages = {268-283},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-86772-0_20},
url = { https://publications.rwth-aachen.de/record/828686},
}×
[issue] 		Bahare Salmani Barzoki, Joost-Pieter Katoen. Fine-Tuning the Odds in Bayesian Networks, European Conference on Symbolic and Quantitative Approaches with Uncertainty (ECSQARU), Volume 12897 of LNCS, 268-283, Springer, 2021.
DOI fulltext PDF [bibtex]
@conference{PATISPP2021,
title = {PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs},
author = {Roman Andriushchenko and Milan Češka and Sebastian Junges and Joost-Pieter Katoen and Šimon Stupinský},
publisher = {Springer},
booktitle = {LNCS},
volume = {12759, Theoretical Computer Science and General Issues},
pages = {856-869},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-81685-8_40},
url = { https://publications.rwth-aachen.de/record/834351},
}×
[issue] 		Roman Andriushchenko, Milan Češka, Sebastian Junges, Joost-Pieter Katoen, Šimon Stupinský. PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs, 33. International Conference on Computer-Aided Verification (CAV 2021), Volume 12759, Theoretical Computer Science and General Issues of LNCS, 856-869, Springer, 2021.
DOI [bibtex]
@conference{OCPPQVQCR2021,
title = {On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report},
author = {Carlos E. Budde and Arnd Hartmanns and Michaela Klauck and Jan Křetínský and David Parker and Tim Quatmann and Andrea Turrini and Zhen Zhang},
publisher = {Springer},
booktitle = {LNCS},
volume = {12479},
pages = {216-241},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-83723-5_15},
url = { https://publications.rwth-aachen.de/record/834796},
}×
[issue] 		Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Křetínský, David Parker, Tim Quatmann, Andrea Turrini, Zhen Zhang. On Correctness, Precision, and Performance in Quantitative Verification: QComp 2020 Competition Report, 9. International Symposium on Leveraging Applications of Formal Methods (ISoLA 2020), Volume 12479 of LNCS, 216-241, Springer, 2021.
DOI [bibtex]
@conference{MCMFLF2021,
title = {Model Checking the Multi-Formalism Language FIGARO},
author = {Shahid Khan and Matthias Volk and Joost-Pieter Katoen and Alexis Braibant and Marc Bouissou},
publisher = {IEEE},
pages = {463-470},
type = {Conference Paper},
year = {2021},
doi = {10.1109/DSN48987.2021.00056},
url = { https://publications.rwth-aachen.de/record/835145},
}×
[issue] 		Shahid Khan, Matthias Volk, Joost-Pieter Katoen, Alexis Braibant, Marc Bouissou. Model Checking the Multi-Formalism Language FIGARO, 51. Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), 463-470, IEEE, 2021.
DOI [bibtex]
@conference{ASMPMCUG2021,
title = {Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs},
author = {Muhammad Hannan Khan and Osman Hassan and Shahid Khan},
publisher = {Springer},
booktitle = {LNCS},
volume = {12819, Theoretical computer science and general issues},
pages = {86-104},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-85315-0_6},
url = { https://publications.rwth-aachen.de/record/835153},
}×
[issue] 		Muhammad Hannan Khan, Osman Hassan, Shahid Khan. Accelerating SpMV Multiplication in Probabilistic Model Checkers Using GPUs, 18. International Colloquium on Theoretical Aspects of Computing (ICTAC 2021), Volume 12819, Theoretical computer science and general issues of LNCS, 86-104, Springer, 2021.
DOI fulltext PDF [bibtex]
@article{S2021,
title = {Synthesizing optimal bias in randomized self-stabilization},
author = {Matthias Volk and Borzoo Bonakdarpour and Joost-Pieter Katoen and Saba Aflaki},
publisher = {Springer},
journal = {Distributed computing},
volume = {35(1)},
pages = {pages 37-57},
type = {Journal Article},
year = {2021},
doi = {10.1007/s00446-021-00408-4},
url = { https://publications.rwth-aachen.de/record/835189},
}×
[issue] 		Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Saba Aflaki. Synthesizing optimal bias in randomized self-stabilization, Distributed computing 35 (1), pages 37-57, Springer, 2021.
DOI [bibtex]
@conference{AMANDFT2021,
title = {A Modular Approach to Non-deterministic Dynamic Fault Trees},
author = {Sascha Müller and Adeline Jordon and Andreas Gerndt and Thomas Noll},
publisher = {Springer},
booktitle = {Programming and Software Engineering},
volume = {12852},
pages = {243-257},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-83903-1_16},
url = { https://publications.rwth-aachen.de/record/835216},
}×
[issue] 		Sascha Müller, Adeline Jordon, Andreas Gerndt, Thomas Noll. A Modular Approach to Non-deterministic Dynamic Fault Trees, 40. International Conference on Computer Safety, Reliability and Security (SAFECOMP 2021), Volume 12852 of Programming and Software Engineering, 243-257, Springer, 2021.
DOI [bibtex]
@conference{ADPP2021,
title = {A Debugger for Probabilistic Programs},
author = {Alexander Hoppen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {13085},
pages = {282-289},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-92124-8_16},
url = { https://publications.rwth-aachen.de/record/836481},
}×
[issue] 		Alexander Hoppen, Thomas Noll. A Debugger for Probabilistic Programs, 19. International Conference on Software Engineering and Formal Methods (SEFM 2021), Volume 13085 of LNCS, 282-289, Springer, 2021.
DOI [bibtex]
@article{PDCD2021,
title = {Probabilistic Data with Continuous Distributions},
author = {Martin Grohe and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Peter Lindner},
publisher = {Association for Computing Machinery},
journal = {ACM SIGMOD record},
volume = {50(1)},
pages = {pages 69-76},
type = {Journal Article},
year = {2021},
doi = {10.1145/3471485.3471502},
url = { https://publications.rwth-aachen.de/record/840183},
}×
[issue] 		Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner. Probabilistic Data with Continuous Distributions, ACM SIGMOD record 50 (1), pages 69-76, Association for Computing Machinery, 2021.
DOI arXiv:2103.02972 fulltext PDF [bibtex]
@unpublished{WLGSRW2021,
title = {Weisfeiler-Leman, Graph Spectra, and Random Walks},
author = {Gaurav Rattan and Tim Frederik Seppelt},
pages = {19 Seiten},
type = {Preprint},
year = {2021},
doi = {10.18154/RWTH-2022-01183},
url = { https://arxiv.org/abs/2103.02972},
}×
[issue] 		Gaurav Rattan, Tim Frederik Seppelt. Weisfeiler-Leman, Graph Spectra, and Random Walks, 19 Seiten, 2021. https://arxiv.org/abs/2103.02972
DOI [bibtex]
@conference{TPTTA2021,
title = {The Probabilistic Termination Tool Amber},
author = {Marcel Moosbrugger and Ezio Bartocci and Joost-Pieter Katoen and Laura Kovács},
publisher = {Springer},
booktitle = {LNCS},
volume = {13047},
pages = {667-675},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-90870-6_36},
url = { https://publications.rwth-aachen.de/record/840912},
}×
[issue] 		Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács. The Probabilistic Termination Tool Amber, Formal Methods - 24. International Symposium (FM 2021), Volume 13047 of LNCS, 667-675, Springer, 2021.
DOI [bibtex]
@conference{ATAPPP2021,
title = {Automated Termination Analysis of Polynomial Probabilistic Programs},
author = {Marcel Moosbrugger and Ezio Bartocci and Joost-Pieter Katoen and Laura Kovács},
publisher = {Springer},
booktitle = {LNCS},
volume = {12648},
pages = {491-518},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-72019-3_18},
url = { https://publications.rwth-aachen.de/record/840913},
}×
[issue] 		Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, Laura Kovács. Automated Termination Analysis of Polynomial Probabilistic Programs, 30. European Symposium on Programming (ESOP 2021), Volume 12648 of LNCS, 491-518, Springer, 2021.
DOI [bibtex]
@conference{SRMLBRD2021,
title = {Synergising Reliability Modelling Languages: BDMPs and Repairable DFTs},
author = {Shahid Khan and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {113-122},
type = {Conference Paper},
year = {2021},
doi = {10.1109/PRDC53464.2021.00023},
url = { https://publications.rwth-aachen.de/record/841296},
}×
[issue] 		Shahid Khan, Joost-Pieter Katoen. Synergising Reliability Modelling Languages: BDMPs and Repairable DFTs, IEEE 26. Pacific Rim International Symposium on Dependable Computing (PRDC), 113-122, IEEE, 2021.
DOI [bibtex]
@conference{MAFSVDFT2021,
title = {Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees},
author = {Shahid Khan and Joost-Pieter Katoen and Matthias Volk and Ahmad Zafar and Falak Sher},
publisher = {IEEE},
type = {Conference Paper},
year = {2021},
doi = {10.1109/LADC53747.2021.9672579},
url = { https://publications.rwth-aachen.de/record/841297},
}×
[issue] 		Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Ahmad Zafar, Falak Sher. Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees, 10. Latin-American Symposium on Dependable Computing (LADC), IEEE, 2021.
DOI [bibtex]
@conference{SRALV2021,
title = {Scalable Reliability Analysis by Lazy Verification},
author = {Shahid Khan and Joost-Pieter Katoen and Matthias Volk and Marc Bouissou},
publisher = {Springer},
booktitle = {LNCS},
volume = {12673, Programming and Software Engineering},
pages = {180-197},
type = {Conference Paper},
year = {2021},
doi = {10.1007/978-3-030-76384-8_12},
url = { https://publications.rwth-aachen.de/record/841298},
}×
[issue] 		Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Marc Bouissou. Scalable Reliability Analysis by Lazy Verification, 13. NASA Formal Methods Symposium, Volume 12673, Programming and Software Engineering of LNCS, 180-197, Springer, 2021.
DOI arXiv:1910.11666v4 fulltext PDF [bibtex]
@unpublished{RLNNA2021,
title = {Residuality and Learning for Nondeterministic Nominal Automata},
author = {Joshua Moerman and Matteo Sammartino},
pages = {27 Seiten},
type = {Preprint},
year = {2021},
doi = {10.18154/RWTH-2022-01946},
url = { https://arxiv.org/abs/1910.11666v4},
}×
[issue] 		Joshua Moerman, Matteo Sammartino. Residuality and Learning for Nondeterministic Nominal Automata, 27 Seiten, 2021. https://arxiv.org/abs/1910.11666v4
DOI [bibtex]
@conference{OFDVSWRA2021,
title = {Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata},
author = {Mikolaj Bojanczyk and Bartek Klin and Joshua Moerman},
publisher = {Association for Computing Machinery},
booktitle = {ACM Conferences},
type = {Conference Paper},
year = {2021},
doi = {10.1109/LICS52264.2021.9470634},
url = { https://publications.rwth-aachen.de/record/847230},
}×
[issue] 		Mikolaj Bojanczyk, Bartek Klin, Joshua Moerman. Orbit-Finite-Dimensional Vector Spaces and Weighted Register Automata, 36. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), ACM Conferences, Association for Computing Machinery, 2021.
Show all