Joost-Pieter Katoen

katoen-2
Email
katoen at 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

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.
DOI 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},
doi = {10.48550/ARXIV.2401.12170},
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
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},
volume = {63(1/3)},
pages = {pages 40-80},
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 63 (1/3), pages 40-80, 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]
@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 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.
DOI 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},
doi = {10.48550/ARXIV.2307.07314},
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.
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 Petrus Carla 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 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. 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 [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 : 25. International Conference (FOSSACS 2022), 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.
DOI fulltext PDF [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.48550/ARXIV.2207.02822},
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
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 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},
volume = {24(5)},
pages = {pages 803-8019},
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 24 (5), pages 803-8019, Springer, 2022.
DOI [bibtex]
@article{GDCD2022,
title = {Generative Datalog with Continuous Distributions},
author = {Martin Grohe and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Peter Lindner},
publisher = {ACM},
journal = {Journal of the ACM},
volume = {69(6)},
pages = {pages 46},
type = {Journal Article},
year = {2022},
doi = {10.1145/3559102},
url = { https://publications.rwth-aachen.de/record/861295},
}×
[issue]
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner. Generative Datalog with Continuous Distributions, Journal of the ACM 69 (6), pages 46, ACM, 2022.
DOI [bibtex]
@article{COPSM2022,
title = {Convex Optimization for Parameter Synthesis in MDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Institute of Electrical and Electronics Engineers},
journal = {IEEE transactions on automatic control},
volume = {67(12)},
pages = {pages 6333-6348},
type = {Journal Article},
year = {2022},
doi = {10.1109/TAC.2021.3133265},
url = { https://publications.rwth-aachen.de/record/888868},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Convex Optimization for Parameter Synthesis in MDPs, IEEE transactions on automatic control 67 (12), pages 6333-6348, Institute of Electrical and Electronics Engineers, 2022.
DOI [bibtex]
@conference{BSBEASDFT2022,
title = {BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees},
author = {Daniel Basgöze and Matthias Volk and Joost-Pieter Katoen and Shahid Khan and Marielle Stoelinga},
publisher = {Springer},
booktitle = {LNCS},
volume = {13260},
pages = {713-732},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-06773-0_38},
url = { https://publications.rwth-aachen.de/record/951563},
}×
[issue]
Daniel Basgöze, Matthias Volk, Joost-Pieter Katoen, Shahid Khan, Marielle Stoelinga. BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees, 14. International Symposium NASA Formal Methods (NFM 2022), Volume 13260 of LNCS, 713-732, Springer, 2022.
DOI [bibtex]
@article{R2022,
title = {Reasoning about distributed reconfigurable systems},
author = {Emma Ahrens and Marius Bozga and Radu Iosif and Joost-Pieter Katoen},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {6(OOPSLA2)},
pages = {pages 145-174},
type = {Journal Article},
year = {2022},
doi = {10.1145/3563293},
url = { https://publications.rwth-aachen.de/record/951603},
}×
[issue]
Emma Ahrens, Marius Bozga, Radu Iosif, Joost-Pieter Katoen. Reasoning about distributed reconfigurable systems, Proceedings of the ACM on programming languages 6 (OOPSLA2), pages 145-174, ACM, 2022.
DOI [bibtex]
@inbook{PSMMAGS2022,
title = {Parameter Synthesis in Markov Models: A Gentle Survey},
author = {Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13660},
pages = {407-437},
type = {Book Chapter},
year = {2022},
doi = {10.1007/978-3-031-22337-2_20},
url = { https://publications.rwth-aachen.de/record/951604},
}×
[issue]
Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis in Markov Models: A Gentle Survey, Volume 13660 of LNCS, 407-437, Springer, 2022.
2021
DOI [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},
doi = {10.1007/978-3-030-68446-4_12},
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 [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},
volume = {60(1)},
pages = {pages 33-86},
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 60 (1), pages 33-86, Springer, 2021.
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 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 [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 fulltext PDF [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{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 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]
@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 [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 (NFM 2021), Volume 12673, Programming and software engineering of LNCS, 180-197, Springer, 2021.
2020
DOI [bibtex]
@article{A2020,
title = {Aiming low is harder: induction for lower bounds in probabilistic program verification},
author = {Marcel Tobias Hark and Benjamin Lucien Kaminski and Jürgen Giesl and Joost-Pieter Katoen},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {4(POPL)},
pages = {pages 1-28},
type = {Journal Article},
year = {2020},
doi = {10.1145/3371105},
url = { https://publications.rwth-aachen.de/record/784743},
}×
[issue]
Marcel Tobias Hark, Benjamin Lucien Kaminski, Jürgen Giesl, Joost-Pieter Katoen. Aiming low is harder: induction for lower bounds in probabilistic program verification, Proceedings of the ACM on programming languages 4 (POPL), pages 1-28, ACM, 2020.
DOI arXiv:2004.14835 [bibtex]
@unpublished{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schroer},
type = {Preprint},
year = {2020},
doi = {10.48550/ARXIV.2004.14835},
url = { https://arxiv.org/abs/2004.14835},
}×
[issue]
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schroer. PrIC3: Property Directed Reachability for MDPs, 2020. https://arxiv.org/abs/2004.14835
DOI fulltext PDF [bibtex]
@conference{SSMOM2020,
title = {Simple Strategies in Multi-Objective MDPs},
author = {Florent Delgrange and Joost-Pieter Katoen and Tim Quatmann and Mickael Randour},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078, Theoretical Computer Science and General Issues},
pages = {346-364},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_19},
url = { https://publications.rwth-aachen.de/record/792348},
}×
[issue]
Florent Delgrange, Joost-Pieter Katoen, Tim Quatmann, Mickael Randour. Simple Strategies in Multi-Objective MDPs, 26. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078, Theoretical Computer Science and General Issues of LNCS, 346-364, Springer, 2020.
DOI [bibtex]
@article{PMPG2020,
title = {Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination},
author = {Christel Baier and Hans Christian Hensel and Lisa Hutschenreiter and Sebastian Junges and Joost-Pieter Katoen and Joachim Klein},
publisher = {Elsevier},
journal = {Information and computation},
volume = {272},
pages = {pages 104504},
type = {Journal Article},
year = {2020},
doi = {10.1016/j.ic.2019.104504},
url = { https://publications.rwth-aachen.de/record/793292},
}×
[issue]
Christel Baier, Hans Christian Hensel, Lisa Hutschenreiter, Sebastian Junges, Joost-Pieter Katoen, Joachim Klein. Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination, Information and computation 272, pages 104504, Elsevier, 2020.
DOI [bibtex]
@conference{SBVUM2020,
title = {Scenario-Based Verification of Uncertain MDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078, Theoretical Computer Science and General Issues},
pages = {287-305},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_16},
url = { https://publications.rwth-aachen.de/record/794207},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Scenario-Based Verification of Uncertain MDPs, 26. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078, Theoretical Computer Science and General Issues of LNCS, 287-305, Springer, 2020.
DOI [bibtex]
@article{SSPRPGBA2020,
title = {Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions},
author = {Leonore Winterer and Sebastian Junges and Ralf Wimmer and Nils Jansen and Ufuk Topcu and Joost-Pieter Katoen and Bernd Becker},
publisher = {Institute of Electrical and Electronics Engineers},
journal = {IEEE transactions on automatic control},
volume = {66(3)},
pages = {pages 1040-1054},
type = {Journal Article},
year = {2020},
doi = {10.1109/TAC.2020.2990140},
url = { https://publications.rwth-aachen.de/record/794210},
}×
[issue]
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Strategy Synthesis for POMDPs in Robot Planning via Game-Based Abstractions, IEEE transactions on automatic control 66 (3), pages 1040-1054, Institute of Electrical and Electronics Engineers, 2020.
DOI [bibtex]
@conference{GDCD2020,
title = {Generative Datalog with Continuous Distributions},
author = {Martin Grohe and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Peter Lindner},
publisher = {ACM},
pages = {347-360},
type = {Conference Paper},
year = {2020},
doi = {10.1145/3375395.3387659},
url = { https://publications.rwth-aachen.de/record/794402},
}×
[issue]
Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Peter Lindner. Generative Datalog with Continuous Distributions, 39. ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems (PODS 2020), 347-360, ACM, 2020.
DOI fulltext PDF [bibtex]
@article{MBTAM2020,
title = {Multi-cost Bounded Tradeoff Analysis in MDP},
author = {Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
journal = {Journal of automated reasoning},
volume = {64(7)},
pages = {pages 1483-1522},
type = {Journal Article},
year = {2020},
doi = {10.1007/s10817-020-09574-9},
url = { https://publications.rwth-aachen.de/record/794977},
}×
[issue]
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Tradeoff Analysis in MDP, Journal of automated reasoning 64 (7), pages 1483-1522, Springer, 2020.
DOI fulltext PDF [bibtex]
@conference{SGLRSO2020,
title = {Stochastic Games with Lexicographic Reachability-Safety Objectives},
author = {Krishnendu Chatterjee and Joost-Pieter Katoen and Maximilian Weininger and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {398-420},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_21},
url = { https://publications.rwth-aachen.de/record/795010},
}×
[issue]
Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler. Stochastic Games with Lexicographic Reachability-Safety Objectives, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 398-420, Springer, 2020.
DOI fulltext PDF [bibtex]
@conference{VWQB2020,
title = {Various Ways to Quantify BDMPs},
author = {Marc Bouissou and Shahid Khan and Joost-Pieter Katoen and Pavel Krcal},
publisher = {NICTA},
booktitle = {EPTCS},
volume = {316},
pages = {1-14},
type = {Conference Paper},
year = {2020},
doi = {10.4204/EPTCS.316.1},
url = { https://publications.rwth-aachen.de/record/795086},
}×
[issue]
Marc Bouissou, Shahid Khan, Joost-Pieter Katoen, Pavel Krcal. Various Ways to Quantify BDMPs, 4. Workshop on Models for Formal Analysis of Real Systems (MARS 2020), Volume 316 of EPTCS, 1-14, NICTA, 2020.
DOI arXiv:2007.06327 [bibtex]
@unpublished{GFPP2020,
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},
type = {Preprint},
year = {2020},
doi = {10.48550/ARXIV.2007.06327},
url = { https://arxiv.org/abs/2007.06327},
}×
[issue]
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 2020. https://arxiv.org/abs/2007.06327
DOI arXiv:2010.14548 [bibtex]
@unpublished{RCVPP2020,
title = {Relatively Complete Verification of Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
pages = {49 Seiten},
type = {Preprint},
year = {2020},
doi = {10.48550/ARXIV.2010.14548},
url = { https://arxiv.org/abs/2010.14548},
}×
[issue]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Relatively Complete Verification of Probabilistic Programs, 49 Seiten, 2020. https://arxiv.org/abs/2010.14548
fulltext PDF [bibtex]
@techreport{URTGURAVL2020,
title = {UnRAVeL Research Training Group: Uncertainty and Randomness in Algorithms, Verification, and Logic},
author = {Joost-Pieter Katoen and Martin Ritzert and Richard Marlon Wilke and Katrin M. Dannert and Peter Lindner and Dennis Fischer and Janosch Fuchs and Björn Frederik Tauer and Vipin Ravindran Vijayalakshmi and Laura Vargas Koch and Nadine Friesen and Andreas Gabriel Klinger and Marcel Tobias Hark and Benjamin Lucien Kaminski and Sebastian Junges and Jip Josephine Spel and Anton Pirogov and Stefan Schupp and Till Hofmann and Daxin Liu and Martin Comis and Tabea Claudia Krabs and Stephan Zieger and Rebecca Haehn and Matthias Volk and Norman Weik and Helene-Maria Bolke-Hermanns},
pages = {85 Seiten},
type = {Tech Report},
year = {2020},
url = { https://publications.rwth-aachen.de/record/807487},
}×
[issue]
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. UnRAVeL Research Training Group: Uncertainty and Randomness in Algorithms, Verification, and Logic, 85 Seiten, 2020.
DOI [bibtex]
@conference{WPSBICCDD2020,
title = {Weakest Preexpectation Semantics for Bayesian Inference: Conditioning, Continuous Distributions and Divergence},
author = {Marcin Szymczak and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12154},
pages = {44-121},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-55089-9_3},
url = { https://publications.rwth-aachen.de/record/814579},
}×
[issue]
Marcin Szymczak, Joost-Pieter Katoen. Weakest Preexpectation Semantics for Bayesian Inference: Conditioning, Continuous Distributions and Divergence, 5. School on Engineering Trustworthy Software Systems (SETSS 2019), Volume 12154 of LNCS, 44-121, Springer, 2020.
DOI [bibtex]
@conference{PMCA2020,
title = {Probabilistic Model Checking of AODV},
author = {Mojgan Kamali and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12289},
pages = {54-73},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-59854-9_6},
url = { https://publications.rwth-aachen.de/record/814584},
}×
[issue]
Mojgan Kamali, Joost-Pieter Katoen. Probabilistic Model Checking of AODV, 17. International Conference on Quantitative Evaluation of SysTems (QEST 2020), Volume 12289 of LNCS, 54-73, Springer, 2020.
DOI fulltext PDF [bibtex]
@conference{BISMC2020,
title = {Bayesian Inference by Symbolic Model Checking},
author = {Bahare Salmani Barzoki and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12289},
pages = {115-133},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-59854-9_9},
url = { https://publications.rwth-aachen.de/record/814595},
}×
[issue]
Bahare Salmani Barzoki, Joost-Pieter Katoen. Bayesian Inference by Symbolic Model Checking, 17. International Conference on Quantitative Evaluation of SysTems (QEST 2020), Volume 12289 of LNCS, 115-133, Springer, 2020.
DOI fulltext PDF [bibtex]
@conference{IBVWVCN2020,
title = {Interpretation-Based Violation Witness Validation for C: NITWIT},
author = {Jan Švejda and Philipp Berger and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12078, Theoretical Computer Science and General Issues},
pages = {40-57},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-45190-5_3},
url = { https://publications.rwth-aachen.de/record/814598},
}×
[issue]
Jan Švejda, Philipp Berger, Joost-Pieter Katoen. Interpretation-Based Violation Witness Validation for C: NITWIT, 26. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2020), Volume 12078, Theoretical Computer Science and General Issues of LNCS, 40-57, Springer, 2020.
DOI [bibtex]
@conference{BSMCAC2020,
title = {Benchmarking Software Model Checkers on Automotive Code},
author = {Lukas Westhofen and Philipp Berger and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {12229},
pages = {133-150},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-55754-6_8},
url = { https://publications.rwth-aachen.de/record/814599},
}×
[issue]
Lukas Westhofen, Philipp Berger, Joost-Pieter Katoen. Benchmarking Software Model Checkers on Automotive Code, 12. NASA Formal Methods Symposium (NFM 2020), Volume 12229 of LNCS, 133-150, Springer, 2020.
DOI [bibtex]
@conference{EBLDMPG2020,
title = {Explaining Boolean-Logic Driven Markov Processes using GSPNs},
author = {Shahid Khan and Joost-Pieter Katoen and Marc Bouissou},
publisher = {IEEE},
pages = {119-126},
type = {Conference Paper},
year = {2020},
doi = {10.1109/EDCC51268.2020.00028},
url = { https://publications.rwth-aachen.de/record/814600},
}×
[issue]
Shahid Khan, Joost-Pieter Katoen, Marc Bouissou. Explaining Boolean-Logic Driven Markov Processes using GSPNs, 16. European Dependable Computing Conference (EDCC), 119-126, IEEE, 2020.
DOI [bibtex]
@conference{ACSRB2020,
title = {A Compositional Semantics for Repairable BDMPs},
author = {Shahid Khan and Joost-Pieter Katoen and Marc Bouissou},
publisher = {Springer},
booktitle = {LNCS},
volume = {12234},
pages = {82-98},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-54549-9_6},
url = { https://publications.rwth-aachen.de/record/814601},
}×
[issue]
Shahid Khan, Joost-Pieter Katoen, Marc Bouissou. A Compositional Semantics for Repairable BDMPs, 39. International Conference on Computer Safety, Reliability and Security (SAFECOMP 2020), Volume 12234 of LNCS, 82-98, Springer, 2020.
DOI [bibtex]
@conference{VIHP2020,
title = {Verification of Indefinite-Horizon POMDPs},
author = {Alexander Nikolai Bork and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
booktitle = {LNCS},
volume = {12302},
pages = {288-304},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-59152-6_16},
url = { https://publications.rwth-aachen.de/record/814779},
}×
[issue]
Alexander Nikolai Bork, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Verification of Indefinite-Horizon POMDPs, International Symposium on Automated Technology for Verification and Analysis (ATVA 2020), Volume 12302 of LNCS, 288-304, Springer, 2020.
DOI fulltext PDF [bibtex]
@conference{PPDRM2020,
title = {PrIC3: Property Directed Reachability for MDPs},
author = {Kevin Batz and Sebastian Junges and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Philipp Schröer},
publisher = {Springer},
booktitle = {LNCS},
volume = {12225},
pages = {512-538},
type = {Conference Paper},
year = {2020},
doi = {10.1007/978-3-030-53291-8_27},
url = { https://publications.rwth-aachen.de/record/816242},
}×
[issue]
Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Philipp Schröer. PrIC3: Property Directed Reachability for MDPs, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 512-538, Springer, 2020.
DOI arXiv:2004.13283 [bibtex]
@unpublished{VWQB2020,
title = {Various Ways to Quantify BDMPs},
author = {Marc Bouissou and Shahid Khan and Joost-Pieter Katoen and Pavel Krcal},
type = {Preprint},
year = {2020},
doi = {10.48550/ARXIV.2004.13283},
url = { https://arxiv.org/abs/2004.13283},
}×
[issue]
Marc Bouissou, Shahid Khan, Joost-Pieter Katoen, Pavel Krcal. Various Ways to Quantify BDMPs, 2020. https://arxiv.org/abs/2004.13283
fulltext PDF [bibtex]
@conference{VPP2020,
title = {Verifying Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {12289},
pages = {298-298},
type = {Conference Paper},
year = {2020},
url = { https://publications.rwth-aachen.de/record/834060},
}×
[issue]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Verifying Probabilistic Programs, 17. International Conference on Quantitative Evaluation of SysTems (QEST 2020), Volume 12289 of LNCS, 298-298, Springer, 2020.
2019
DOI [bibtex]
@article{O2019,
title = {On the hardness of analyzing probabilistic programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
journal = {Acta informatica},
volume = {56(3)},
pages = {pages 255-285},
type = {Journal Article},
year = {2019},
doi = {10.1007/s00236-018-0321-1},
url = { https://publications.rwth-aachen.de/record/753077},
}×
[issue]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. On the hardness of analyzing probabilistic programs, Acta informatica 56 (3), pages 255-285, Springer, 2019.
DOI fulltext PDF [bibtex]
@article{Q2019,
title = {Quantitative separation logic: a logic for reasoning about probabilistic pointer programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
volume = {3(POPL)},
pages = {pages 34},
type = {Journal Article},
year = {2019},
doi = {10.1145/3290347},
url = { https://publications.rwth-aachen.de/record/753722},
}×
[issue]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative separation logic: a logic for reasoning about probabilistic pointer programs, Proceedings of the ACM on programming languages 3 (POPL), pages 34, ACM, 2019.
DOI [bibtex]
@article{S2019,
title = {Safety analysis for vehicle guidance systems with dynamic fault trees},
author = {Majdi Ghadhab and Sebastian Junges and Joost-Pieter Katoen and Matthias Kuntz and Matthias Volk},
publisher = {Elsevier Science},
journal = {Reliability engineering & system safety},
volume = {186},
pages = {pages 37-50},
type = {Journal Article},
year = {2019},
doi = {10.1016/j.ress.2019.02.005},
url = { https://publications.rwth-aachen.de/record/755407},
}×
[issue]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Safety analysis for vehicle guidance systems with dynamic fault trees, Reliability engineering & system safety 186, pages 37-50, Elsevier Science, 2019.
DOI [bibtex]
@conference{CP2019,
title = {Correct-by-construction policies for POMDPs},
author = {Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann and Bernd Becker and Ralf Wimmer and Leonore Winterer},
publisher = {ACM Press},
booktitle = {ACM Digital Library},
pages = {6-8},
type = {Conference Paper},
year = {2019},
doi = {10.1145/3313149.3313366},
url = { https://publications.rwth-aachen.de/record/764541},
}×
[issue]
Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann, Bernd Becker, Ralf Wimmer, Leonore Winterer. Correct-by-construction policies for POMDPs, 5. International Workshop on Symbolic-Numeric Methods for Reasoning about CPS and IoT (SNR) held as part of the 12th Cyber-Physical Systems and Internet-of-Things Week (CPS-IoT Week) (SNR '19), ACM Digital Library, 6-8, ACM Press, 2019.
DOI [bibtex]
@conference{ADMAIRARSA2019,
title = {A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas},
author = {Matthias Volk and Norman Weik and Joost-Pieter Katoen and Nils Nießen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11687},
pages = {40-58},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-27008-7_3},
url = { https://publications.rwth-aachen.de/record/766655},
}×
[issue]
Matthias Volk, Norman Weik, Joost-Pieter Katoen, Nils Nießen. A DFT Modeling Approach for Infrastructure Reliability Analysis of Railway Station Areas, 24. International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, 40-58, Springer, 2019.
DOI [bibtex]
@conference{FVRRDFT2019,
title = {Formal Verification of Rewriting Rules for Dynamic Fault Trees},
author = {Yassmeen Elderhalli and Matthias Volk and Osman Hasan and Joost-Pieter Katoen and Sofiène Tahar},
publisher = {Springer},
booktitle = {LNCS},
volume = {11724, Theoretical computer science and general issues},
pages = {513-531},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-30446-1_27},
url = { https://publications.rwth-aachen.de/record/766660},
}×
[issue]
Yassmeen Elderhalli, Matthias Volk, Osman Hasan, Joost-Pieter Katoen, Sofiène Tahar. Formal Verification of Rewriting Rules for Dynamic Fault Trees, 17. edition of the International Conference on Software Engineering and Formal Methods (SEFM 2019), Volume 11724, Theoretical computer science and general issues of LNCS, 513-531, Springer, 2019.
DOI [bibtex]
@conference{MAROSTVAMBD2019,
title = {Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development},
author = {Philipp Berger and Johanna Nellen and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow},
publisher = {Springer},
booktitle = {LNCS},
volume = {11687},
pages = {59-75},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-27008-7_4},
url = { https://publications.rwth-aachen.de/record/767285},
}×
[issue]
Philipp Berger, Johanna Nellen, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Multiple Analyses, Requirements Once: Simplifying Testing and Verification in Automotive Model-Based Development, 24. International Conference on Formal Methods for Industrial Critical Systems (FMICS 2019), Volume 11687 of LNCS, 59-75, Springer, 2019.
DOI fulltext PDF [bibtex]
@proceedings{ISMFCS2019,
title = {44th International Symposium on Mathematical Foundations of Computer Science},
author = {},
editor = {Peter Rossmanith and Pinar Heggernes and Joost-Pieter Katoen},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing},
booktitle = {Leibniz international proceedings in informatics},
volume = {138},
pages = {1 Online-Ressource : Illustrationen},
type = {Proceeding Article},
year = {2019},
doi = {10.4230/LIPICS.MFCS.2019.0},
url = { https://publications.rwth-aachen.de/record/767443},
}×
[issue]
Peter Rossmanith (ed), Pinar Heggernes (ed), Joost-Pieter Katoen (ed). 44th International Symposium on Mathematical Foundations of Computer Science, Volume 138 of Leibniz international proceedings in informatics, 1 Online-Ressource : Illustrationen, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, 2019.
DOI [bibtex]
@inbook{TFMMC2019,
title = {The 10,000 Facets of MDP Model Checking},
author = {Christel Baier and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10000},
pages = {420-451},
type = {Book Chapter},
year = {2019},
doi = {10.1007/978-3-319-91908-9_21},
url = { https://publications.rwth-aachen.de/record/768053},
}×
[issue]
Christel Baier, Holger Hermanns, Joost-Pieter Katoen. The 10,000 Facets of MDP Model Checking, Volume 10000 of LNCS, 420-451, Springer, 2019.
DOI [bibtex]
@inbook{MRR2019,
title = {Model Repair Revamped},
author = {Milan Češka and Hans Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11500},
pages = {107-125},
type = {Book Chapter},
year = {2019},
doi = {10.1007/978-3-030-31514-6_7},
url = { https://publications.rwth-aachen.de/record/768054},
}×
[issue]
Milan Češka, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Model Repair Revamped, Volume 11500 of LNCS, 107-125, Springer, 2019.
DOI [bibtex]
@article{D2019,
title = {Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems},
author = {Mingzhang Huang and Hongfei Fu and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Information and computation},
volume = {268},
pages = {pages 104431},
type = {Journal Article},
year = {2019},
doi = {10.1016/j.ic.2019.05.004},
url = { https://publications.rwth-aachen.de/record/768514},
}×
[issue]
Mingzhang Huang, Hongfei Fu, Joost-Pieter Katoen. Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems, Information and computation 268, pages 104431, Elsevier, 2019.
DOI [bibtex]
@article{I2019,
title = {IC3 software model checking},
author = {Tim Felix Lange and Martin R. Neuhäußer and Thomas Noll and Joost-Pieter Katoen},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {22(2)},
pages = {pages 135-161},
type = {Journal Article},
year = {2019},
doi = {10.1007/s10009-019-00547-x},
url = { https://publications.rwth-aachen.de/record/772976},
}×
[issue]
Tim Felix Lange, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. IC3 software model checking, International journal on software tools for technology transfer 22 (2), pages 135-161, Springer, 2019.
DOI fulltext PDF [bibtex]
@conference{OCRPMDP2019,
title = {On the Complexity of Reachability in Parametric Markov Decision Processes},
author = {Tobias Winkler and Sebastian Junges and Guillermo A. Pérez and Joost-Pieter Katoen},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August},
booktitle = {Leibniz international proceedings in informatics : LIPIcs},
volume = {140},
type = {Conference Paper},
year = {2019},
doi = {10.4230/LIPICS.CONCUR.2019.14},
url = { https://publications.rwth-aachen.de/record/780394},
}×
[issue]
Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes, 30. International Conference on Concurrency Theory (CONCUR), Volume 140 of Leibniz international proceedings in informatics : LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019.
DOI [bibtex]
@conference{APMCM2019,
title = {Are Parametric Markov Chains Monotonic?},
author = {Jip Josephine Spel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11781},
pages = {479-496},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-31784-3_28},
url = { https://publications.rwth-aachen.de/record/786826},
}×
[issue]
Jip Josephine Spel, Sebastian Junges, Joost-Pieter Katoen. Are Parametric Markov Chains Monotonic?, 17. International Symposium on Automated Technology for Verification and Analysis (ATVA 2019), Volume 11781 of LNCS, 479-496, Springer, 2019.
DOI fulltext PDF [bibtex]
@conference{SHMC2019,
title = {Shepherding Hordes of Markov Chains},
author = {Milan Češka and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11428},
pages = {172-190},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-17465-1_10},
url = { https://publications.rwth-aachen.de/record/786829},
}×
[issue]
Milan Češka, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Shepherding Hordes of Markov Chains, 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Volume 11428 of LNCS, 172-190, Springer, 2019.
DOI [bibtex]
@proceedings{D2019,
title = {Dependable software engineering: theories, tools, and applications},
author = {},
editor = {Nan Guan and Joost-Pieter Katoen and Jun Sun},
publisher = {Springer},
booktitle = {LNCS},
volume = {11951},
pages = {viii, 138 Seiten : Illustrationen},
type = {Proceeding Article},
year = {2019},
doi = {10.1007/978-3-030-35540-1},
url = { https://publications.rwth-aachen.de/record/786830},
}×
[issue]
Nan Guan (ed), Joost-Pieter Katoen (ed), Jun Sun (ed). Dependable software engineering: theories, tools, and applications, Volume 11951 of LNCS, viii, 138 Seiten : Illustrationen, Springer, 2019.
DOI [bibtex]
@conference{CDSPPS2019,
title = {Counterexample-Driven Synthesis for Probabilistic Program Sketches},
author = {Milan Češka and Hans Christian Hensel and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {11800},
pages = {101-120},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-30942-8_8},
url = { https://publications.rwth-aachen.de/record/786831},
}×
[issue]
Milan Češka, Hans Christian Hensel, Sebastian Junges, Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches, 3. World Congress on Formal Methods (FM 2019), Volume 11800 of LNCS, 101-120, Springer, 2019.
DOI [bibtex]
@conference{SRMLBRD2019,
title = {Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs},
author = {Shahid Khan and Joost-Pieter Katoen and Matthias Volk and Marc Bouissou},
publisher = {IEEE},
pages = {266-275},
type = {Conference Paper},
year = {2019},
doi = {10.1109/PRDC47002.2019.00057},
url = { https://publications.rwth-aachen.de/record/786900},
}×
[issue]
Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Marc Bouissou. Synergizing Reliability Modeling Languages: BDMPs without Repairs and DFTs, 24. Pacific Rim International Symposium on Dependable Computing (PRDC), 266-275, IEEE, 2019.
DOI fulltext PDF [bibtex]
@conference{C2019,
title = {COMPASS 3.0},
author = {Marco Bozzano and Harold Yorick Bruintjes and Alessandro Cimatti and Joost-Pieter Katoen and Thomas Noll and Stefano Tonetta},
publisher = {Springer},
booktitle = {LNCS},
volume = {11427},
pages = {379-385},
type = {Conference Paper},
year = {2019},
doi = {10.1007/978-3-030-17462-0_25},
url = { https://publications.rwth-aachen.de/record/860910},
}×
[issue]
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. COMPASS 3.0, 25. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Volume 11427 of LNCS, 379-385, Springer, 2019.
2018
DOI [bibtex]
@article{CPP2018,
title = {Conditioning in Probabilistic Programming},
author = {Federico Olmedo and Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Annabelle Mciver},
publisher = {Association for Computing Machinery},
journal = {ACM transactions on programming languages and systems},
volume = {40(1)},
pages = {pages 4},
type = {Journal Article},
year = {2018},
doi = {10.1145/3156018},
url = { https://publications.rwth-aachen.de/record/713137},
}×
[issue]
Federico Olmedo, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Annabelle Mciver. Conditioning in Probabilistic Programming, ACM transactions on programming languages and systems 40 (1), pages 4, Association for Computing Machinery, 2018.
DOI [bibtex]
@article{FDFTAMCT2018,
title = {Fast Dynamic Fault Tree Analysis by Model Checking Techniques},
author = {Matthias Volk and Sebastian Junges and Joost-Pieter Katoen},
publisher = {IEEE},
journal = {IEEE transactions on industrial informatics},
volume = {14(1)},
pages = {pages 370-379},
type = {Journal Article},
year = {2018},
doi = {10.1109/TII.2017.2710316},
url = { https://publications.rwth-aachen.de/record/713138},
}×
[issue]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Fast Dynamic Fault Tree Analysis by Model Checking Techniques, IEEE transactions on industrial informatics 14 (1), pages 370-379, IEEE, 2018.
DOI fulltext PDF [bibtex]
@conference{MBRM2018,
title = {Multi-cost Bounded Reachability in MDP},
author = {Arnd Hartmanns and Sebastian Junges and Joost-Pieter Katoen and Tim Quatmann},
publisher = {Springer},
booktitle = {LNCS},
volume = {10806, Part 2},
pages = {320-339},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89963-3_19},
url = { https://publications.rwth-aachen.de/record/745801},
}×
[issue]
Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen, Tim Quatmann. Multi-cost Bounded Reachability in MDP, 24. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), Volume 10806, Part 2 of LNCS, 320-339, Springer, 2018.
DOI [bibtex]
@article{A2018,
title = {A new proof rule for almost-sure termination},
author = {Annabelle McIver and Carroll Morgan and Benjamin Lucien Kaminski and Joost-Pieter Katoen},
publisher = {ACM},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
pages = {pages 33:1-33:28},
type = {Journal Article},
year = {2018},
doi = {10.1145/3158121},
url = { https://publications.rwth-aachen.de/record/753060},
}×
[issue]
Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, Joost-Pieter Katoen. A new proof rule for almost-sure termination, Proceedings of the ACM on Programming Languages 2, pages 33:1-33:28, ACM, 2018.
DOI fulltext PDF [bibtex]
@conference{HOBIA2018,
title = {How long, O Bayesian network, will I sample thee?: A program analysis perspective on expected sampling times},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {10801},
pages = {186-213},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-89884-1_7},
url = { https://publications.rwth-aachen.de/record/753062},
}×
[issue]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. How long, O Bayesian network, will I sample thee?: A program analysis perspective on expected sampling times, 27. European Symposium on Programming (ESOP 2018), Volume 10801 of LNCS, 186-213, Springer, 2018.
DOI [bibtex]
@conference{ONFAAUSDFTUG2018,
title = {One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs},
author = {Sebastian Junges and Joost-Pieter Katoen and Marielle Stoelinga and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10877},
pages = {272-293},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-91268-4_14},
url = { https://publications.rwth-aachen.de/record/753065},
}×
[issue]
Sebastian Junges, Joost-Pieter Katoen, Marielle Stoelinga, Matthias Volk. One Net Fits All: A Unifying Semantics of Dynamic Fault Trees Using GSPNs, 39. International Conference on Applications and Theory of Petri Nets and Concurrency (PETRI NETS 2018), Volume 10877 of LNCS, 272-293, Springer, 2018.
DOI arXiv:1802.10467 [bibtex]
@unpublished{QSLALRPP2018,
title = {Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
pages = {159 Seiten},
type = {Preprint},
year = {2018},
doi = {10.48550/ARXIV.1802.10467},
url = { https://arxiv.org/abs/1802.10467},
}×
[issue]
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Quantitative Separation Logic: A Logic for Reasoning about Probabilistic Programs, 159 Seiten, 2018. https://arxiv.org/abs/1802.10467
DOI [bibtex]
@conference{BBCOV2018,
title = {Branching Bisimulation and Concurrent Object Verification},
author = {Xiaoxiao Yang and Joost-Pieter Katoen and Huimin Lin and Gaoang Liu and Hao Wu},
publisher = {IEEE},
pages = {267-278},
type = {Conference Paper},
year = {2018},
doi = {10.1109/DSN.2018.00037},
url = { https://publications.rwth-aachen.de/record/753067},
}×
[issue]
Xiaoxiao Yang, Joost-Pieter Katoen, Huimin Lin, Gaoang Liu, Hao Wu. Branching Bisimulation and Concurrent Object Verification, 48. Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2018), 267-278, IEEE, 2018.
DOI [bibtex]
@conference{LGBYWAAVJPP2018,
title = {Let this Graph Be Your Witness!: An Attestor for Verifying Java Pointer Programs},
author = {Hannah Arndt and Christina Jansen and Joost-Pieter Katoen and Christoph Matheja and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {10982},
pages = {3-11},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-96142-2_1},
url = { https://publications.rwth-aachen.de/record/753069},
}×
[issue]
Hannah Arndt, Christina Jansen, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll. Let this Graph Be Your Witness!: An Attestor for Verifying Java Pointer Programs, 30. International Conference on Computer Aided Verification (CAV 2018), Volume 10982 of LNCS, 3-11, Springer, 2018.
DOI [bibtex]
@article{WPRERRA2018,
title = {Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo},
journal = {Journal of the ACM},
volume = {65(5)},
pages = {pages 30:1-30:68},
type = {Journal Article},
year = {2018},
doi = {10.1145/3208102},
url = { https://publications.rwth-aachen.de/record/753072},
}×
[issue]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms, Journal of the ACM 65 (5), pages 30:1-30:68, 2018.
DOI fulltext PDF [bibtex]
@conference{MCMTA2018,
title = {Monitoring CTMCs by Multi-clock Timed Automata},
author = {Yijun Feng and Joost-Pieter Katoen and Haokun Li and Bican Xia and Naijun Zhan},
publisher = {Springer},
booktitle = {LNCS},
volume = {10981},
pages = {507-526},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-96145-3_27},
url = { https://publications.rwth-aachen.de/record/753073},
}×
[issue]
Yijun Feng, Joost-Pieter Katoen, Haokun Li, Bican Xia, Naijun Zhan. Monitoring CTMCs by Multi-clock Timed Automata, 30. International Conference on Computer Aided Verification (CAV 2018), Volume 10981 of LNCS, 507-526, Springer, 2018.
DOI fulltext PDF [bibtex]
@conference{SVI2018,
title = {Sound Value Iteration},
author = {Tim Quatmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10981},
pages = {643-661},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-96145-3_37},
url = { https://publications.rwth-aachen.de/record/753074},
}×
[issue]
Tim Quatmann, Joost-Pieter Katoen. Sound Value Iteration, 30. International Conference on Computer Aided Verification (CAV 2018), Volume 10981 of LNCS, 643-661, Springer, 2018.
DOI [bibtex]
@conference{VACCSAERAD2018,
title = {Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain},
author = {Philipp Berger and Joost-Pieter Katoen and Erika Ábrahám and Md Tawhid Bin Waez and Thomas Rambow},
publisher = {Springer},
booktitle = {LNCS},
volume = {10951},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-95582-7_18},
url = { https://publications.rwth-aachen.de/record/753075},
}×
[issue]
Philipp Berger, Joost-Pieter Katoen, Erika Ábrahám, Md Tawhid Bin Waez, Thomas Rambow. Verifying Auto-generated C Code from Simulink: An Experience Report in the Automotive Domain, 22. International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
DOI [bibtex]
@conference{FVASCMETCER2018,
title = {Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations},
author = {Johanna Nellen and Thomas Rambow and Md Tawhid Bin Waez and Erika Ábrahám and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10951},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-95582-7_23},
url = { https://publications.rwth-aachen.de/record/753076},
}×
[issue]
Johanna Nellen, Thomas Rambow, Md Tawhid Bin Waez, Erika Ábrahám, Joost-Pieter Katoen. Formal Verification of Automotive Simulink Controller Models: Empirical Technical Challenges, Evaluation and Recommendations, 22. International Symposium on Formal Methods (FM 2018), Volume 10951 of LNCS, Springer, 2018.
DOI [bibtex]
@conference{IGSI2018,
title = {Improving Generalization in Software IC3},
author = {Tim Lange and Frederick Prinz and Martin R. Neuhäußer and Thomas Noll and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
pages = {85-102},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-94111-0_5},
url = { https://publications.rwth-aachen.de/record/753079},
}×
[issue]
Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen. Improving Generalization in Software IC3, 23. International Symposium on Model Checking Software (Spin 2018), LNCS, 85-102, Springer, 2018.
DOI [bibtex]
@conference{RBCPD2018,
title = {Rule-Based Conditioning of Probabilistic Data},
author = {Maurice van Keulen and Benjamin Lucien Kaminski and Christoph Matheja and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {Lecture Notes in Artificial Intelligence},
volume = {11142},
pages = {290-305},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-030-00461-3_20},
url = { https://publications.rwth-aachen.de/record/753086},
}×
[issue]
Maurice van Keulen, Benjamin Lucien Kaminski, Christoph Matheja, Joost-Pieter Katoen. Rule-Based Conditioning of Probabilistic Data, 12. International Conference on Scalable Uncertainty Management (SUM 2018), Volume 11142 of Lecture Notes in Artificial Intelligence, 290-305, Springer, 2018.
DOI [bibtex]
@conference{SATP2018,
title = {Synthesis in pMDPs: A Tale of 1001 Parameters},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {Springer},
booktitle = {LNCS},
volume = {11138},
pages = {160-176},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-030-01090-4},
url = { https://publications.rwth-aachen.de/record/753087},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ufuk Topcu. Synthesis in pMDPs: A Tale of 1001 Parameters, 16. International Symposium on Automated Technology for Verification and Analysis (ATVA 2018), Volume 11138 of LNCS, 160-176, Springer, 2018.
DOI [bibtex]
@conference{MCSNAH2018,
title = {Model Checking for Safe Navigation Among Humans},
author = {Sebastian Junges and Nils Jansen and Joost-Pieter Katoen and Ufuk Topcu and Ruohan Zhang and Mary Hayhoe},
publisher = {Springer},
booktitle = {LNCS},
volume = {11024, Theoretical Computer Science and General Issues},
pages = {207-222},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-99154-2_13},
url = { https://publications.rwth-aachen.de/record/754533},
}×
[issue]
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu, Ruohan Zhang, Mary Hayhoe. Model Checking for Safe Navigation Among Humans, 15. International Conference on Quantitative Evaluation of Systems (QEST 2018), Volume 11024, Theoretical Computer Science and General Issues of LNCS, 207-222, Springer, 2018.
fulltext PDF [bibtex]
@conference{FSCPPS2018,
title = {Finite-State Controllers of POMDPs using Parameter Synthesis},
author = {Sebastian Junges and Nils Jansen and Ralf Wimmer and Tim Quatmann and Leonore Winterer and Joost-Pieter Katoen and Bernd Becker},
publisher = {AUAI Press},
pages = {519-529},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/754534},
}×
[issue]
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34. Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, AUAI Press, 2018.
DOI [bibtex]
@conference{PISP2018,
title = {Parameter-Independent Strategies for pMDPs via POMDPs},
author = {Sebastian Arming and Ezio Bartocci and Krishnendu Chatterjee and Joost-Pieter Katoen and Ana Sokolova},
publisher = {Springer},
booktitle = {LNCS},
volume = {11024, Theoretical Computer Science and General Issues},
pages = {53-70},
type = {Conference Paper},
year = {2018},
doi = {10.1007/978-3-319-99154-2_4},
url = { https://publications.rwth-aachen.de/record/759181},
}×
[issue]
Sebastian Arming, Ezio Bartocci, Krishnendu Chatterjee, Joost-Pieter Katoen, Ana Sokolova. Parameter-Independent Strategies for pMDPs via POMDPs, 15. International Conference on Quantitative Evaluation of Systems (QEST 2018), Volume 11024, Theoretical Computer Science and General Issues of LNCS, 53-70, Springer, 2018.
[bibtex]
@conference{FSCPPS2018,
title = {Finite-State Controllers of POMDPs using Parameter Synthesis},
author = {Sebastian Junges and Nils Jansen and Ralf Wimmer and Tim Quatmann and Leonore Winterer and Joost-Pieter Katoen and Bernd Becker},
publisher = {Curran Associates, Inc.},
pages = {519-529},
type = {Conference Paper},
year = {2018},
url = { https://publications.rwth-aachen.de/record/794908},
}×
[issue]
Sebastian Junges, Nils Jansen, Ralf Wimmer, Tim Quatmann, Leonore Winterer, Joost-Pieter Katoen, Bernd Becker. Finite-State Controllers of POMDPs using Parameter Synthesis, 34. Conference on Uncertainty in Artificial Intelligence (UAI 34), 519-529, Curran Associates, Inc., 2018.
2017
DOI [bibtex]
@article{QM2017,
title = {Quantitative model-checking of controlled discrete-time Markov processes},
author = {Ilya Tkachev and Alexandru Mereacre and Joost-Pieter Katoen and Alessandro Abate},
publisher = {Elsevier},
journal = {Information and Computation},
volume = {253(Part 1)},
pages = {pages 1-35},
type = {Journal Article},
year = {2017},
doi = {10.1016/j.ic.2016.11.006},
url = { https://publications.rwth-aachen.de/record/684632},
}×
[issue]
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate. Quantitative model-checking of controlled discrete-time Markov processes, Information and Computation 253 (Part 1), pages 1-35, Elsevier, 2017.
DOI [bibtex]
@article{F2017,
title = {Fault trees on a diet: automated reduction by graph rewriting},
author = {Sebastian Junges and Dennis Guck and Joost-Pieter Katoen and Arend Rensink and Mariëlle Stoelinga},
publisher = {Springer},
journal = {Formal aspects of computing},
volume = {29(4)},
pages = {pages 651-703},
type = {Journal Article},
year = {2017},
doi = {10.1007/s00165-016-0412-0},
url = { https://publications.rwth-aachen.de/record/696190},
}×
[issue]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga. Fault trees on a diet: automated reduction by graph rewriting, Formal aspects of computing 29 (4), pages 651-703, Springer, 2017.
DOI [bibtex]
@conference{AWPESMSE2017,
title = {A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {1-12},
type = {Conference Paper},
year = {2017},
doi = {10.1109/LICS.2017.8005153},
url = { https://publications.rwth-aachen.de/record/713562},
}×
[issue]
Benjamin Lucien Kaminski, Joost-Pieter Katoen. A Weakest Pre-Expectation Semantics for Mixed-Sign Expectations, 32. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), 1-12, IEEE, 2017.
DOI arXiv:1702.04311 [bibtex]
@unpublished{ACAMPMC2017,
title = {A storm is Coming: A Modern Probabilistic Model Checker},
author = {Hans Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk},
pages = {14 Seiten : Tabellen, Diagramme},
type = {Preprint},
year = {2017},
doi = {10.48550/ARXIV.1702.04311},
url = { https://arxiv.org/abs/1702.04311},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A storm is Coming: A Modern Probabilistic Model Checker, 14 Seiten : Tabellen, Diagramme, 2017. https://arxiv.org/abs/1702.04311
fulltext PDF [bibtex]
@article{M2017,
title = {Missie: foutvrije software in de ruimte},
author = {Harold Yorick Bruintjes and Joost-Pieter Katoen},
publisher = {Techwatch bv},
journal = {Bits en Chips},
volume = {1},
pages = {pages 38-39},
type = {Journal Article},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713564},
}×
[issue]
Harold Yorick Bruintjes, Joost-Pieter Katoen. Missie: foutvrije software in de ruimte, Bits en Chips 1, pages 38-39, Techwatch bv, 2017.
DOI [bibtex]
@conference{ASCAMPMC2017,
title = {A Storm is Coming: A Modern Probabilistic Model Checker},
author = {Hans Christian Dehnert and Sebastian Junges and Joost-Pieter Katoen and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10427},
pages = {592-600},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-63390-9_31},
url = { https://publications.rwth-aachen.de/record/713569},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker, 29. International Conference on Computer-Aided Verification (CAV 2017), Volume 10427 of LNCS, 592-600, Springer, 2017.
DOI [bibtex]
@conference{SCPEVPM2017,
title = {Sequential Convex Programming for the Efficient Verification of Parametric MDPs},
author = {Murat Cubuktepe and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen and Ivan Papusha and Hasan A. Poonawala and Ufuk Topcu},
publisher = {Springer},
booktitle = {LNCS},
volume = {10206},
pages = {133-150},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-662-54580-5_8},
url = { https://publications.rwth-aachen.de/record/713572},
}×
[issue]
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs, 23. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2017), Volume 10206 of LNCS, 133-150, Springer, 2017.
DOI [bibtex]
@conference{MAMO2017,
title = {Markov Automata with Multiple Objectives},
author = {Tim Quatmann and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10426},
pages = {140-159},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-63387-9_7},
url = { https://publications.rwth-aachen.de/record/713574},
}×
[issue]
Tim Quatmann, Sebastian Junges, Joost-Pieter Katoen. Markov Automata with Multiple Objectives, 29. International Conference on Computer-Aided Verification (CAV 2017), Volume 10426 of LNCS, 140-159, Springer, 2017.
fulltext PDF [bibtex]
@conference{TCT2017,
title = {The COMPASS 3.0 Toolset},
author = {Marco Bozzano and Harold Yorick Bruintjes and Alessandro Cimatti and Joost-Pieter Katoen and Thomas Noll and Stefano Tonetta},
pages = {2 Seiten},
type = {Conference Talk},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713576},
}×
[issue]
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. The COMPASS 3.0 Toolset, 5. International Symposium on Model Based Safety Assessment (IMBSA 2017), 2 Seiten, 2017.
DOI [bibtex]
@conference{MSAVGS2017,
title = {Model-based Safety Analysis for Vehicle Guidance Systems},
author = {Majdi Ghadhab and Sebastian Junges and Joost-Pieter Katoen and Matthias Kuntz and Matthias Volk},
publisher = {Springer},
booktitle = {LNCS},
volume = {10488},
pages = {3-19},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-66266-4_1},
url = { https://publications.rwth-aachen.de/record/713577},
}×
[issue]
Majdi Ghadhab, Sebastian Junges, Joost-Pieter Katoen, Matthias Kuntz, Matthias Volk. Model-based Safety Analysis for Vehicle Guidance Systems, 36. International Conference on Computer Safety, Reliability, and Security (SAFECOMP 2017), Volume 10488 of LNCS, 3-19, Springer, 2017.
DOI [bibtex]
@conference{AFTPSSA2017,
title = {Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms},
author = {Saba Aflaki and Matthias Volk and Borzoo Bonakdarpour and Joost-Pieter Katoen and Arne Storjohann},
publisher = {IEEE},
pages = {94-103},
type = {Conference Paper},
year = {2017},
doi = {10.1109/SRDS.2017.22},
url = { https://publications.rwth-aachen.de/record/713578},
}×
[issue]
Saba Aflaki, Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen, Arne Storjohann. Automated Fine Tuning of Probabilistic Self-Stabilizing Algorithms, 36. International Symposium on Reliable Distributed Systems (SRDS 2017), 94-103, IEEE, 2017.
DOI [bibtex]
@conference{M2017,
title = {Motion planning under partial observability using game-based abstraction},
author = {Leonore Winterer and Sebastian Junges and Ralf Wimmer and Nils Jansen and Ufuk Topcu and Joost-Pieter Katoen and Bernd Becker},
publisher = {IEEE},
pages = {2201-2208},
type = {Conference Paper},
year = {2017},
doi = {10.1109/CDC.2017.8263971},
url = { https://publications.rwth-aachen.de/record/713579},
}×
[issue]
Leonore Winterer, Sebastian Junges, Ralf Wimmer, Nils Jansen, Ufuk Topcu, Joost-Pieter Katoen, Bernd Becker. Motion planning under partial observability using game-based abstraction, IEEE 56. Annual Conference on Decision and Control (CDC), 2201-2208, IEEE, 2017.
DOI [bibtex]
@conference{MSGARPA2017,
title = {Modal Stochastic Games: Abstraction-Refinement of Probabilistic Automata},
author = {Joost-Pieter Katoen and Falak Sher},
publisher = {Springer},
booktitle = {LNCS},
volume = {10460},
pages = {426-448},
type = {Conference Paper},
year = {2017},
doi = {10.1007/978-3-319-63121-9_21},
url = { https://publications.rwth-aachen.de/record/713580},
}×
[issue]
Joost-Pieter Katoen, Falak Sher. Modal Stochastic Games: Abstraction-Refinement of Probabilistic Automata, KiMfest, Volume 10460 of LNCS, 426-448, Springer, 2017.
DOI [bibtex]
@inbook{BFTAFM2017,
title = {Boosting Fault Tree Analysis by Formal Methods},
author = {Joost-Pieter Katoen and Marielle Stoelinga},
publisher = {Springer},
booktitle = {LNCS},
volume = {10500},
pages = {368-389},
type = {Book Chapter},
year = {2017},
doi = {10.1007/978-3-319-68270-9_19},
url = { https://publications.rwth-aachen.de/record/713581},
}×
[issue]
Joost-Pieter Katoen, Marielle Stoelinga. Boosting Fault Tree Analysis by Formal Methods, Volume 10500 of LNCS, 368-389, Springer, 2017.
fulltext PDF [bibtex]
@misc{TTOPSMMA2017,
title = {Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract)},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {10580},
pages = {[XVI]-XVII},
type = {Invited Abstract},
year = {2017},
url = { https://publications.rwth-aachen.de/record/713582},
}×
[issue]
Joost-Pieter Katoen. Tweaking The Odds: Parameter Synthesis in Markov Models (Abstract), Volume 10580 of LNCS, [XVI]-XVII, Springer, 2017.
DOI [bibtex]
@book{MTTEB2017,
title = {ModelEd, TestEd, TrustEd: essays dedicated to Ed Brinksma on the occassion of his 60th birthday},
author = {Joost-Pieter Katoen and Rom Langerak and Arend Rensink},
publisher = {Springer},
booktitle = {LNCS},
volume = {10500},
pages = {XII, 389 Seiten : Illustrationen, Diagramme},
type = {Book},
year = {2017},
doi = {10.1007/978-3-319-68270-9},
url = { https://publications.rwth-aachen.de/record/713625},
}×
[issue]
Joost-Pieter Katoen, Rom Langerak, Arend Rensink. ModelEd, TestEd, TrustEd: essays dedicated to Ed Brinksma on the occassion of his 60th birthday, Volume 10500 of LNCS, XII, 389 Seiten : Illustrationen, Diagramme, Springer, 2017.
DOI [bibtex]
@inbook{FMASAC2017,
title = {Formal Methods for Aerospace Systems: Achievements and Challenges},
author = {Marco Bozzano and Harold Yorick Bruintjes and Alessandro Cimatti and Joost-Pieter Katoen and Thomas Noll and Stefano Tonetta},
publisher = {Springer},
booktitle = {Springer eBook Collection : Computer Science},
pages = {133-159},
type = {Book Chapter},
year = {2017},
doi = {10.1007/978-981-10-4436-6_6},
url = { https://publications.rwth-aachen.de/record/713628},
}×
[issue]
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta. Formal Methods for Aerospace Systems: Achievements and Challenges, Springer eBook Collection : Computer Science, 133-159, Springer, 2017.
DOI [bibtex]
@inbook{SVSCS2017,
title = {Synthesis and Verification of Self-aware Computing Systems},
author = {Radu Calinescu and Marco Autili and Javier Ciamara and Antinisca Di Marco and Simos Gerasimou and Paola Inverardi and Alexander Perucci and Nils Jansen and Joost-Pieter Katoen and Marta Kwiatkowska and Ole J. Mengshoel and Romina Spalazzese and Massimo Tivoli},
publisher = {Springer},
booktitle = {Springer eBook Collection : Computer Science},
pages = {337-373},
type = {Book Chapter},
year = {2017},
doi = {10.1007/978-3-319-47474-8_11},
url = { https://publications.rwth-aachen.de/record/713629},
}×
[issue]
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. Synthesis and Verification of Self-aware Computing Systems, Springer eBook Collection : Computer Science, 337-373, Springer, 2017.
2016
DOI fulltext PDF [bibtex]
@article{EG2016,
title = {Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components},
author = {Anton Wijs and Joost-Pieter Katoen and Dragan Bošnački},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {48(3)},
pages = {pages 274-300},
type = {Journal Article},
year = {2016},
doi = {10.1007/s10703-016-0246-7},
url = { https://publications.rwth-aachen.de/record/674301},
}×
[issue]
Anton Wijs, Joost-Pieter Katoen, Dragan Bošnački. Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components, Formal methods in system design 48 (3), pages 274-300, Springer, 2016.
DOI [bibtex]
@conference{TPMCL2016,
title = {The Probabilistic Model Checking Landscape},
author = {Joost-Pieter Katoen},
publisher = {ACM Press},
pages = {31-45},
type = {Conference Paper},
year = {2016},
doi = {10.1145/2933575.2934574},
url = { https://publications.rwth-aachen.de/record/679763},
}×
[issue]
Joost-Pieter Katoen. The Probabilistic Model Checking Landscape, 31. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16), 31-45, ACM Press, 2016.
DOI [bibtex]
@conference{OSSSPL2016,
title = {On the Satisfiability of Some Simple Probabilistic Logics},
author = {Souymodip Chakraborty and Joost-Pieter Katoen},
publisher = {ACM Press},
pages = {56-65},
type = {Conference Paper},
year = {2016},
doi = {10.1145/2933575.2934526},
url = { https://publications.rwth-aachen.de/record/679769},
}×
[issue]
Souymodip Chakraborty, Joost-Pieter Katoen. On the Satisfiability of Some Simple Probabilistic Logics, 31. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '16), 56-65, ACM Press, 2016.
DOI [bibtex]
@conference{RRPP2016,
title = {Reasoning about Recursive Probabilistic Programs},
author = {Federico Olmedo Beron and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {ACM Press},
pages = {672-681},
type = {Conference Paper},
year = {2016},
doi = {10.1145/2933575.2935317},
url = { https://publications.rwth-aachen.de/record/680115},
}×
[issue]
Federico Olmedo Beron, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Reasoning about Recursive Probabilistic Programs, 31. Annual ACM/IEEE Symposium, 672-681, ACM Press, 2016.
DOI [bibtex]
@conference{ICPP2016,
title = {Inferring Covariances for Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
publisher = {Springer},
booktitle = {LNCS},
volume = {9826},
pages = {191-206},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-43425-4_14},
url = { https://publications.rwth-aachen.de/record/680858},
}×
[issue]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja. Inferring Covariances for Probabilistic Programs, 13. International Conference on Quantitative Evaluation of Systems (QEST 2016), Volume 9826 of LNCS, 191-206, Springer, 2016.
DOI [bibtex]
@conference{PECDS2016,
title = {Performance Evaluation of Concurrent Data Structures},
author = {Hao Wu and Xiaoxiao Yang and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9984},
pages = {38-49},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-47677-3_3},
url = { https://publications.rwth-aachen.de/record/681476},
}×
[issue]
Hao Wu, Xiaoxiao Yang, Joost-Pieter Katoen. Performance Evaluation of Concurrent Data Structures, International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA 2016), Volume 9984 of LNCS, 38-49, Springer, 2016.
DOI [bibtex]
@conference{PSMMFTE2016,
title = {Parameter Synthesis for Markov Models: Faster Than Ever},
author = {Tim Quatmann and Hans Christian Dehnert and Nils Jansen and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9938},
pages = {50-67},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-46520-3_4},
url = { https://publications.rwth-aachen.de/record/681503},
}×
[issue]
Tim Quatmann, Hans Christian Dehnert, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever, 14. International Symposium on Automated Technology for Verification and Analysis (ATVA 2016), Volume 9938 of LNCS, 50-67, Springer, 2016.
DOI [bibtex]
@conference{BMCPP2016,
title = {Bounded Model Checking for Probabilistic Programs},
author = {Nils Jansen and Hans Christian Dehnert and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Lukas Westhofen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9938},
pages = {68-85},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-46520-3_5},
url = { https://publications.rwth-aachen.de/record/681511},
}×
[issue]
Nils Jansen, Hans Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lukas Westhofen. Bounded Model Checking for Probabilistic Programs, 14. International Symposium on Automated Technology for Verification and Analysis (ATVA), Volume 9938 of LNCS, 68-85, Springer, 2016.
DOI fulltext PDF [bibtex]
@conference{P2016,
title = {Parameter synthesis for probabilistic systems},
author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Albert-Ludwigs-Universität},
pages = {72-74},
type = {Conference Paper},
year = {2016},
doi = {10.6094/UNIFR/10639},
url = { https://publications.rwth-aachen.de/record/683021},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. Parameter synthesis for probabilistic systems, 19. GI/ITG/GMM-Workshop "Methoden und Beschreibungsprachen zur Modellierung und Verifikation von Schaltungen und Systemen" (MBMV 2016), 72-74, Albert-Ludwigs-Universität, 2016.
DOI [bibtex]
@article{CM2016,
title = {Confluence reduction for Markov automata},
author = {Mark Timmer and Joost-Pieter Katoen and Jaco van de Pol and Mariëlle Stoelinga},
publisher = {Elsevier},
journal = {Theoretical computer science},
volume = {655},
pages = {pages 193-219},
type = {Journal Article},
year = {2016},
doi = {10.1016/j.tcs.2016.01.017},
url = { https://publications.rwth-aachen.de/record/683022},
}×
[issue]
Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Mariëlle Stoelinga. Confluence reduction for Markov automata, Theoretical computer science 655, pages 193-219, Elsevier, 2016.
DOI [bibtex]
@conference{MCAPDULLWN2016,
title = {Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks},
author = {Christian Dombrowski and Sebastian Junges and Joost-Pieter Katoen and James Gross},
publisher = {IEEE},
pages = {307-316},
type = {Conference Paper},
year = {2016},
doi = {10.1109/SRDS.2016.048},
url = { https://publications.rwth-aachen.de/record/683784},
}×
[issue]
Christian Dombrowski, Sebastian Junges, Joost-Pieter Katoen, James Gross. Model-Checking Assisted Protocol Design for Ultra-reliable Low-Latency Wireless Networks, IEEE 35. Symposium on Reliable Distributed Systems (SRDS 2016), 307-316, IEEE, 2016.
DOI [bibtex]
@article{PMCUSADF2016,
title = {Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow},
author = {Joost-Pieter Katoen and Hao Wu},
publisher = {ACM Press},
journal = {ACM Transactions on Embedded Computing Systems},
volume = {22(1)},
pages = {pages 15},
type = {Journal Article},
year = {2016},
doi = {10.1145/2914788},
url = { https://publications.rwth-aachen.de/record/684630},
}×
[issue]
Joost-Pieter Katoen, Hao Wu. Probabilistic Model Checking for Uncertain Scenario-Aware Data Flow, ACM Transactions on Embedded Computing Systems 22 (1), pages 15, ACM Press, 2016.
fulltext PDF [bibtex]
@misc{OSIC2016,
title = {On the Semantic Intricacies of Conditioning},
author = {Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Federico Olmedo Beron},
pages = {2 Seiten},
type = {Invited Abstract},
year = {2016},
url = { https://publications.rwth-aachen.de/record/684633},
}×
[issue]
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo Beron. On the Semantic Intricacies of Conditioning, 2 Seiten, 2016.
DOI [bibtex]
@conference{SRLM2016,
title = {Safety-constrained Reinforcement Learning for MDPs},
author = {Sebastian Junges and Nils Jansen and Hans Christian Dehnert and Ufuk Topcu and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9636},
pages = {130-146},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-662-49674-9_8},
url = { https://publications.rwth-aachen.de/record/684642},
}×
[issue]
Sebastian Junges, Nils Jansen, Hans Christian Dehnert, Ufuk Topcu, Joost-Pieter Katoen. Safety-constrained Reinforcement Learning for MDPs, 22. international conference, held as part of the European Joint Conferences on Theory and Practice of Software (TACAS 2016), Volume 9636 of LNCS, 130-146, Springer, 2016.
DOI [bibtex]
@conference{WPRERTPP2016,
title = {Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo Beron},
publisher = {Springer},
booktitle = {LNCS},
volume = {9632},
pages = {364-389},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-662-49498-1_15},
url = { https://publications.rwth-aachen.de/record/684643},
}×
[issue]
Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo Beron. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs, 25. European Symposium on Programming (ESOP 2016), Volume 9632 of LNCS, 364-389, Springer, 2016.
DOI [bibtex]
@conference{UDFT2016,
title = {Uncovering Dynamic Fault Trees},
author = {Sebastian Junges and Dennis Guck and Joost-Pieter Katoen and Marielle Stoelinga},
publisher = {IEEE},
pages = {299-310},
type = {Conference Paper},
year = {2016},
doi = {10.1109/DSN.2016.35},
url = { https://publications.rwth-aachen.de/record/684644},
}×
[issue]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga. Uncovering Dynamic Fault Trees, 46. Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2016), 299-310, IEEE, 2016.
DOI [bibtex]
@conference{ADFTAGSSSFSFR2016,
title = {Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates},
author = {Matthias Volk and Sebastian Junges and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9922},
pages = {253-265},
type = {Conference Paper},
year = {2016},
doi = {10.1007/978-3-319-45477-1_20},
url = { https://publications.rwth-aachen.de/record/684646},
}×
[issue]
Matthias Volk, Sebastian Junges, Joost-Pieter Katoen. Advancing Dynamic Fault Tree Analysis - Get Succinct State Spaces Fast and Synthesise Failure Rates, 35. International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Volume 9922 of LNCS, 253-265, Springer, 2016.
fulltext PDF [bibtex]
@conference{PVCM2016,
title = {Probabilistic Verification for Cognitive Models},
author = {Sebastian Junges and Nils Jansen and Joost-Pieter Katoen and Ufuk Topcu},
publisher = {AAAI Press},
booktitle = {AAAI Technical Reports},
volume = {FS-16-03},
pages = {185-188},
type = {Conference Paper},
year = {2016},
url = { https://publications.rwth-aachen.de/record/684648},
}×
[issue]
Sebastian Junges, Nils Jansen, Joost-Pieter Katoen, Ufuk Topcu. Probabilistic Verification for Cognitive Models, AAAI 2016 Fall Symposium, Volume FS-16-03 of AAAI Technical Reports, 185-188, AAAI Press, 2016.
2015
DOI [bibtex]
@article{V2015,
title = {Verifying pointer programs using graph grammars},
author = {Jonathan Heinen and Christina Jansen and Joost-Pieter Katoen and Thomas Noll},
publisher = {Elsevier},
journal = {Science of computer programming},
volume = {97(1)},
pages = {pages 157-162},
type = {Journal Article},
year = {2015},
doi = {10.1016/j.scico.2013.11.012},
url = { https://publications.rwth-aachen.de/record/459638},
}×
[issue]
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Verifying pointer programs using graph grammars, Science of computer programming 97 (1), pages 157-162, Elsevier, 2015.
DOI [bibtex]
@article{M2015,
title = {Modelling and statistical model checking of a microgrid},
author = {Souymodip Chakraborty and Joost-Pieter Katoen and Falak Sher and Martin Strelec},
publisher = {Springer},
journal = {International journal on software tools for technology transfer},
volume = {17(4)},
pages = {pages 537-554},
type = {Journal Article},
year = {2015},
doi = {10.1007/s10009-014-0345-y},
url = { https://publications.rwth-aachen.de/record/465767},
}×
[issue]
Souymodip Chakraborty, Joost-Pieter Katoen, Falak Sher, Martin Strelec. Modelling and statistical model checking of a microgrid, International journal on software tools for technology transfer 17 (4), pages 537-554, Springer, 2015.
DOI fulltext PDF [bibtex]
@article{HCPA2015,
title = {High-level Counterexamples for Probabilistic Automata},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen},
publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig},
journal = {Logical methods in computer science},
volume = {11(1)},
pages = {pages 15},
type = {Journal Article},
year = {2015},
doi = {10.2168/LMCS-11(1:15)2015},
url = { https://publications.rwth-aachen.de/record/540624},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen. High-level Counterexamples for Probabilistic Automata, Logical methods in computer science 11 (1), pages 15, Department of Theoretical Computer Science, Technical University of Braunschweig, 2015.
DOI [bibtex]
@conference{CER2015,
title = {Counterexamples for Expected Rewards},
author = {Tim Quatmann and Nils Jansen and Hans Christian Dehnert and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {9109},
pages = {435-452},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-19249-9_27},
url = { https://publications.rwth-aachen.de/record/541095},
}×
[issue]
Tim Quatmann, Nils Jansen, Hans Christian Dehnert, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Counterexamples for Expected Rewards, 20. international symposium Formal Methods (FM 2015), Volume 9109 of LNCS, 435-452, Springer, 2015.
DOI [bibtex]
@conference{MCOIMC2015,
title = {Model Checking of Open Interval Markov Chains},
author = {Souymodip Chakraborty and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9081},
pages = {30-42},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-18579-8_3},
url = { https://publications.rwth-aachen.de/record/541099},
}×
[issue]
Souymodip Chakraborty, Joost-Pieter Katoen. Model Checking of Open Interval Markov Chains, 22. International Conference on Analytical Stochastic Modelling Techniques Applications (ASMTA 2015), Volume 9081 of LNCS, 30-42, Springer, 2015.
DOI [bibtex]
@conference{MPSPHS2015,
title = {Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems},
author = {Martin Fränzle and Sebastian Gerwinn and Paul Kröger and Alessandro Abate and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9268},
pages = {93-107},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-22975-1_7},
url = { https://publications.rwth-aachen.de/record/561520},
}×
[issue]
Martin Fränzle, Sebastian Gerwinn, Paul Kröger, Alessandro Abate, Joost-Pieter Katoen. Multi-objective Parameter Synthesis in Probabilistic Hybrid Systems, 13. International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2015), Volume 9268 of LNCS, 93-107, Springer, 2015.
DOI [bibtex]
@conference{AGAERSM2015,
title = {A Greedy Approach for the Efficient Repair of Stochastic Models},
author = {Shashank Pathak and Erika Ábrahám and Nils Jansen and Armando Tacchella and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9058},
pages = {295-309},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-17524-9_21},
url = { https://publications.rwth-aachen.de/record/561930},
}×
[issue]
Shashank Pathak, Erika Ábrahám, Nils Jansen, Armando Tacchella, Joost-Pieter Katoen. A Greedy Approach for the Efficient Repair of Stochastic Models, 7. NASA Formal Methods Symposium (NFM'15), Volume 9058 of LNCS, 295-309, Springer, 2015.
DOI [bibtex]
@conference{PAPPST2015,
title = {PROPhESY: A PRObabilistic ParamEter SYnthesis Tool},
author = {Hans Christian Dehnert and Sebastian Junges and Nils Jansen and Florian Corzilius and Matthias Volk and Harold Yorick Bruintjes and Joost-Pieter Katoen and Erika Ábrahám},
publisher = {Springer},
booktitle = {LNCS},
volume = {9206},
pages = {214-231},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-21690-4_13},
url = { https://publications.rwth-aachen.de/record/564236},
}×
[issue]
Hans Christian Dehnert, Sebastian Junges, Nils Jansen, Florian Corzilius, Matthias Volk, Harold Yorick Bruintjes, Joost-Pieter Katoen, Erika Ábrahám. PROPhESY: A PRObabilistic ParamEter SYnthesis Tool, International Conference on Computer Aided Verification (CAV'15), Volume 9206 of LNCS, 214-231, Springer, 2015.
DOI [bibtex]
@conference{ASATRAM2015,
title = {A Statistical Approach for Timed Reachability in AADL Models},
author = {Harold Yorick Bruintjes and Joost-Pieter Katoen and David Lesens},
publisher = {IEEE},
pages = {81-88},
type = {Conference Paper},
year = {2015},
doi = {10.1109/DSN.2015.32},
url = { https://publications.rwth-aachen.de/record/571609},
}×
[issue]
Harold Yorick Bruintjes, Joost-Pieter Katoen, David Lesens. A Statistical Approach for Timed Reachability in AADL Models, 45. Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN 2015), 81-88, IEEE, 2015.
DOI fulltext PDF [bibtex]
@article{CPP2015,
title = {Conditioning in Probabilistic Programming},
author = {Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Federico Olmedo and Friedrich Gretz and Annabelle McIver},
publisher = {Elsevier Science},
journal = {Electronic notes in theoretical computer science},
volume = {319},
pages = {pages 199-216},
type = {Journal Article},
year = {2015},
doi = {10.1016/j.entcs.2015.12.013},
url = { https://publications.rwth-aachen.de/record/571612},
}×
[issue]
Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver. Conditioning in Probabilistic Programming, Electronic notes in theoretical computer science 319, pages 199-216, Elsevier Science, 2015.
DOI [bibtex]
@conference{PPATVC2015,
title = {Probabilistic Programming: A True Verification Challenge},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9364},
pages = {1-3},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-24953-7_1},
url = { https://publications.rwth-aachen.de/record/571613},
}×
[issue]
Joost-Pieter Katoen. Probabilistic Programming: A True Verification Challenge, 13. International Symposium on Automated Technology for Verification and Analysis (ATVA 2015), Volume 9364 of LNCS, 1-3, Springer, 2015.
DOI [bibtex]
@conference{OHAST2015,
title = {On the Hardness of Almost–Sure Termination},
author = {Benjamin Lucien Kaminski and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {9234},
pages = {308-318},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-662-48057-1_24},
url = { https://publications.rwth-aachen.de/record/571614},
}×
[issue]
Benjamin Lucien Kaminski, Joost-Pieter Katoen. On the Hardness of Almost–Sure Termination, 40. International Symposium on Mathematical Foundations of Computer Science (MFCS 2015), Volume 9234 of LNCS, 308-318, Springer, 2015.
DOI [bibtex]
@conference{FTD2015,
title = {Fault Trees on a Diet},
author = {Sebastian Junges and Dennis Guck and Joost-Pieter Katoen and Arend Rensink and Mariëlle Stoelinga},
publisher = {Springer},
booktitle = {LNCS},
volume = {9409},
pages = {3-18},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-25942-0_1},
url = { https://publications.rwth-aachen.de/record/571615},
}×
[issue]
Sebastian Junges, Dennis Guck, Joost-Pieter Katoen, Arend Rensink, Mariëlle Stoelinga. Fault Trees on a Diet, 1. International Symposium on Dependable Software Engineering (SETTA 2015), Volume 9409 of LNCS, 3-18, Springer, 2015.
DOI [bibtex]
@article{J2015,
title = {Juggrnaut: using graph grammars for abstracting unbounded heap structures},
author = {Jonathan Heinen and Christina Jansen and Joost-Pieter Katoen and Thomas Noll},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {47(2)},
pages = {pages 159-203},
type = {Journal Article},
year = {2015},
doi = {10.1007/s10703-015-0236-1},
url = { https://publications.rwth-aachen.de/record/571616},
}×
[issue]
Jonathan Heinen, Christina Jansen, Joost-Pieter Katoen, Thomas Noll. Juggrnaut: using graph grammars for abstracting unbounded heap structures, Formal methods in system design 47 (2), pages 159-203, Springer, 2015.
DOI [bibtex]
@conference{UPP2015,
title = {Understanding Probabilistic Programs},
author = {Joost-Pieter Katoen and Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Federico Olmedo Beron},
publisher = {Springer},
booktitle = {LNCS},
volume = {9360},
pages = {15-32},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-23506-6_4},
url = { https://publications.rwth-aachen.de/record/571617},
}×
[issue]
Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Federico Olmedo Beron. Understanding Probabilistic Programs, Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60. Birthday, Volume 9360 of LNCS, 15-32, Springer, 2015.
DOI [bibtex]
@conference{CAUCOI2015,
title = {Compositional Analysis Using Component-Oriented Interpolation},
author = {Viet Yen Nguyen and Benjamin Bittner and Joost-Pieter Katoen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {8997},
pages = {69-85},
type = {Conference Paper},
year = {2015},
doi = {10.1007/978-3-319-15317-9_5},
url = { https://publications.rwth-aachen.de/record/571619},
}×
[issue]
Viet Yen Nguyen, Benjamin Bittner, Joost-Pieter Katoen, Thomas Noll. Compositional Analysis Using Component-Oriented Interpolation, International Symposium on Formal Aspects of Component Software (FACS 2014), Volume 8997 of LNCS, 69-85, Springer, 2015.
fulltext PDF [bibtex]
@conference{PAMDP2015,
title = {P-Automata for Markov Decision Processes},
author = {Souymodip Chakraborty and Joost-Pieter Katoen},
pages = {2-18},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571632},
}×
[issue]
Souymodip Chakraborty, Joost-Pieter Katoen. P-Automata for Markov Decision Processes, 3. International Workshop on Strategic Reasoning (SR 2015), 2-18, 2015.
[bibtex]
@conference{PPANMAC2015,
title = {Probabilistic Programs - A Natural Model for Approximate Computations},
author = {Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja and Federico Olmedo},
type = {Conference Paper},
year = {2015},
url = { https://publications.rwth-aachen.de/record/571634},
}×
[issue]
Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Federico Olmedo. Probabilistic Programs - A Natural Model for Approximate Computations, Workshop on Approximate Computing (AC15), 2015.
2014
DOI [bibtex]
@article{O2014,
title = {Operational versus weakest pre-expectation semantics for the probabilistic guarded command language},
author = {Friedrich Gretz and Joost-Pieter Katoen and Annabelle McIver},
publisher = {Elsevier},
journal = {Performance evaluation},
volume = {73 Special(SI)},
pages = {pages 110-132},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.peva.2013.11.004},
url = { https://publications.rwth-aachen.de/record/232583},
}×
[issue]
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language, Performance evaluation 73 Special (SI), pages 110-132, Elsevier, 2014.
DOI [bibtex]
@conference{CGDTMMAIS2014,
title = {Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey},
author = {Erika Ábrahám and Bernd Becker and Hans Christian Dehnert and Nils Jansen and Joost-Pieter Katoen and Ralf Wimmer},
publisher = {Springer},
booktitle = {LNCS},
volume = {8483},
pages = {65-121},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-07317-0_3},
url = { https://publications.rwth-aachen.de/record/443312},
}×
[issue]
Erika Ábrahám, Bernd Becker, Hans Christian Dehnert, Nils Jansen, Joost-Pieter Katoen, Ralf Wimmer. Counterexample Generation for Discrete-Time Markov Models: An Introductory Survey, Formal methods for executable software models (SFM 2014), Volume 8483 of LNCS, 65-121, Springer, 2014.
DOI [bibtex]
@article{SM2014,
title = {Symbolic counterexample generation for large discrete-time Markov chains},
author = {Nils Jansen and Ralf Wimmer and Erika Ábrahám and Barna Zajzon and Joost-Pieter Katoen and Bernd Becker and Johann Schuster},
publisher = {Elsevier},
journal = {Science of computer programming},
volume = {91(Part A)},
pages = {pages 90-114},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.scico.2014.02.001},
url = { https://publications.rwth-aachen.de/record/445537},
}×
[issue]
Nils Jansen, Ralf Wimmer, Erika Ábrahám, Barna Zajzon, Joost-Pieter Katoen, Bernd Becker, Johann Schuster. Symbolic counterexample generation for large discrete-time Markov chains, Science of computer programming 91 (Part A), pages 90-114, Elsevier, 2014.
DOI [bibtex]
@article{S2014,
title = {Spacecraft early design validation using formal methods},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Panagiotis Katsaros and Konstantinos Mokos and Viet Yen Nguyen and Thomas Noll and Bart Postma and Marco Roveri},
publisher = {Elsevier},
journal = {Reliability engineering & system safety},
volume = {132},
pages = {pages 20-35},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.ress.2014.07.003},
url = { https://publications.rwth-aachen.de/record/445610},
}×
[issue]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Panagiotis Katsaros, Konstantinos Mokos, Viet Yen Nguyen, Thomas Noll, Bart Postma, Marco Roveri. Spacecraft early design validation using formal methods, Reliability engineering & system safety 132, pages 20-35, Elsevier, 2014.
DOI [bibtex]
@article{M2014,
title = {Minimal counterexamples for linear-time probabilistic verification},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Elsevier},
journal = {Theoretical computer science},
volume = {549},
pages = {pages 61-100},
type = {Journal Article},
year = {2014},
doi = {10.1016/j.tcs.2014.06.020},
url = { https://publications.rwth-aachen.de/record/447343},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal counterexamples for linear-time probabilistic verification, Theoretical computer science 549, pages 61-100, Elsevier, 2014.
DOI [bibtex]
@conference{FDPM2014,
title = {Fast Debugging of PRISM Models},
author = {Hans Christian Dehnert and Nils Jansen and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8837},
pages = {146-162},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-11936-6_11},
url = { https://publications.rwth-aachen.de/record/460136},
}×
[issue]
Hans Christian Dehnert, Nils Jansen, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen. Fast Debugging of PRISM Models, Automated technology for verification and analysis : 12th international symposium (ATVA 2014), Volume 8837 of LNCS, 146-162, Springer, 2014.
DOI [bibtex]
@conference{ZRPMCA2014,
title = {Zero-Reachability in Probabilistic Multi-Counter Automata},
author = {Tomáš Brázdil and Stefan Kiefer and Antonín Kucera and Petr Novotný and Joost-Pieter Katoen},
publisher = {ACM},
pages = {Article No. 22, 10 S.},
type = {Conference Paper},
year = {2014},
doi = {10.1145/2603088.2603161},
url = { https://publications.rwth-aachen.de/record/465750},
}×
[issue]
Tomáš Brázdil, Stefan Kiefer, Antonín Kucera, Petr Novotný, Joost-Pieter Katoen. Zero-Reachability in Probabilistic Multi-Counter Automata, 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), Article No. 22, 10 S., ACM, 2014.
DOI [bibtex]
@conference{PLMC2014,
title = {Parametric LTL on Markov Chains},
author = {Souymodip Chakraborty and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8705},
pages = {207-222},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-662-44602-7_17},
url = { https://publications.rwth-aachen.de/record/465751},
}×
[issue]
Souymodip Chakraborty, Joost-Pieter Katoen. Parametric LTL on Markov Chains, 8. IFIP TC 1/WG 2.2 international conference (TCS 2014), Volume 8705 of LNCS, 207-222, Springer, 2014.
DOI [bibtex]
@conference{SRMESMC2014,
title = {Smart Railroad Maintenance Engineering with Stochastic Model Checking},
author = {Dennis Guck and Joost-Pieter Katoen and Marielle Stoelinga and Ted Luiten and Judi Romijn},
publisher = {Civil-Comp Press},
booktitle = {Civil-Comp Proceedings : CCP},
volume = {104},
pages = {Paper 299, 16 S.},
type = {Conference Paper},
year = {2014},
doi = {10.4203/ccp.104.299},
url = { https://publications.rwth-aachen.de/record/465754},
}×
[issue]
Dennis Guck, Joost-Pieter Katoen, Marielle Stoelinga, Ted Luiten, Judi Romijn. Smart Railroad Maintenance Engineering with Stochastic Model Checking, 2. International Conference on Railway Technology: Research, Development and Maintenance, Volume 104 of Civil-Comp Proceedings : CCP, Paper 299, 16 S., Civil-Comp Press, 2014.
DOI [bibtex]
@conference{ESCSRA2014,
title = {Exponentially timed SADF: Compositional Semantics, Reduction, and Analysis},
author = {Joost-Pieter Katoen and Hao Wu},
publisher = {ACM},
pages = {Article No. 1, 10 S.},
type = {Conference Paper},
year = {2014},
doi = {10.1145/2656045.2656058},
url = { https://publications.rwth-aachen.de/record/465756},
}×
[issue]
Joost-Pieter Katoen, Hao Wu. Exponentially timed SADF: Compositional Semantics, Reduction, and Analysis, International Conference on Embedded Software (EMSOFT), Article No. 1, 10 S., ACM, 2014.
fulltext PDF [bibtex]
@conference{MCGMM2014,
title = {Model Checking Gigantic Markov Models},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8702},
pages = {XV-XVII},
type = {Conference Paper},
year = {2014},
url = { https://publications.rwth-aachen.de/record/465757},
}×
[issue]
Joost-Pieter Katoen. Model Checking Gigantic Markov Models, Software engineering and formal methods (SEFM 2014), Volume 8702 of LNCS, XV-XVII, Springer, 2014.
DOI [bibtex]
@conference{PACSG2014,
title = {Performance Analysis of Computing Servers: a case study exploiting a new GSPN semantics},
author = {Joost-Pieter Katoen and Thomas Noll and Thomas Santen and Dirk Seifert and Hao Wu},
publisher = {Springer},
booktitle = {LNCS},
volume = {8376},
pages = {57-72},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-05359-2_5},
url = { https://publications.rwth-aachen.de/record/465758},
}×
[issue]
Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Performance Analysis of Computing Servers: a case study exploiting a new GSPN semantics, Measurement, modelling, and evaluation of computing systems and dependability and fault-tolerance (MMB DFT 2014), Volume 8376 of LNCS, 57-72, Springer, 2014.
DOI [bibtex]
@conference{PSL2014,
title = {Probably Safe or Live},
author = {Joost-Pieter Katoen and Lei Song and Lijun Zhang},
publisher = {ACM},
pages = {Article No. 55, 10 S.},
type = {Conference Paper},
year = {2014},
doi = {10.1145/2603088.2603147},
url = { https://publications.rwth-aachen.de/record/465759},
}×
[issue]
Joost-Pieter Katoen, Lei Song, Lijun Zhang. Probably Safe or Live, 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) (CSL-LICS '14), Article No. 55, 10 S., ACM, 2014.
DOI [bibtex]
@conference{LRAPA2014,
title = {Layered Reduction for Abstract Probabilistic Automata},
author = {Arpit Sharma and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {21-31},
type = {Conference Paper},
year = {2014},
doi = {10.1109/ACSD.2014.10},
url = { https://publications.rwth-aachen.de/record/465762},
}×
[issue]
Arpit Sharma, Joost-Pieter Katoen. Layered Reduction for Abstract Probabilistic Automata, 14. International Conference on Application of Concurrency to System Design (ACSD 2014), 21-31, IEEE, 2014.
DOI [bibtex]
@conference{TGAPA2014,
title = {Tight Game Abstractions of Probabilistic Automata},
author = {Falak Sher Vira and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8704},
pages = {576-592},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-662-44584-6_39},
url = { https://publications.rwth-aachen.de/record/465763},
}×
[issue]
Falak Sher Vira, Joost-Pieter Katoen. Tight Game Abstractions of Probabilistic Automata, CONCUR 2014 - concurrency theory (CONCUR 2014), Volume 8704 of LNCS, 576-592, Springer, 2014.
DOI [bibtex]
@conference{LRMST2014,
title = {Layered Reduction for Modal Specification Theories},
author = {Arpit Sharma and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8348},
pages = {1-19},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-07602-7_20},
url = { https://publications.rwth-aachen.de/record/465764},
}×
[issue]
Arpit Sharma, Joost-Pieter Katoen. Layered Reduction for Modal Specification Theories, Formal aspects of component software : 10. international symposium (FACS 2013), Volume 8348 of LNCS, 1-19, Springer, 2014.
DOI [bibtex]
@conference{GBGDSCMEC2014,
title = {GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components},
author = {Anton J. Wijs and Joost-Pieter Katoen and Dragan Bosnacki},
publisher = {Springer},
booktitle = {LNCS},
volume = {8559},
pages = {309-325},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-08867-9_20},
url = { https://publications.rwth-aachen.de/record/465765},
}×
[issue]
Anton J. Wijs, Joost-Pieter Katoen, Dragan Bosnacki. GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components, Computer aided verification : 26. international conference (CAV 2014), Volume 8559 of LNCS, 309-325, Springer, 2014.
DOI [bibtex]
@article{ATLROMA2014,
title = {Analysis of Timed and Long-Run Objectives in Markov Automata},
author = {Dennis Guck and Hassan Hatefi and Holger Hermanns and Joost-Pieter Katoen and Mark Timmer},
publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig},
journal = {Logical methods in computer science},
volume = {10(3)},
pages = {pages Paper 17},
type = {Journal Article},
year = {2014},
doi = {10.2168/LMCS-10(3:17)2014},
url = { https://publications.rwth-aachen.de/record/465769},
}×
[issue]
Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer. Analysis of Timed and Long-Run Objectives in Markov Automata, Logical methods in computer science 10 (3), pages Paper 17, Department of Theoretical Computer Science, Technical University of Braunschweig, 2014.
fulltext PDF [bibtex]
@inbook{FVMMBSSE2014,
title = {Formal Validation Methods in Model-Based Spacecraft Systems Engineering},
author = {Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll},
publisher = {Taylor and Francis},
pages = {340-375},
type = {Book Chapter},
year = {2014},
url = { https://publications.rwth-aachen.de/record/465771},
}×
[issue]
Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Formal Validation Methods in Model-Based Spacecraft Systems Engineering, 340-375, Taylor and Francis, 2014.
DOI [bibtex]
@conference{APPV2014,
title = {Accelerating Parametric Probabilistic Verification},
author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {8657},
pages = {404-420},
type = {Conference Paper},
year = {2014},
doi = {10.1007/978-3-319-10696-0_31},
url = { https://publications.rwth-aachen.de/record/540007},
}×
[issue]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 11. International Conference on Quantitative Evaluation of Systems (QEST 2014), Volume 8657 of LNCS, 404-420, Springer, 2014.
2013
DOI arXiv:1305.5055 [bibtex]
@unpublished{HCPA2013,
title = {High-level Counterexamples for Probabilistic Automata},
author = {Ralf Wimmer and Nils Jansen and Andreas Vorpahl and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Cornell University},
type = {Preprint},
year = {2013},
doi = {10.48550/ARXIV.1305.5055},
url = { https://arxiv.org/abs/1305.5055},
}×
[issue]
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Cornell University, 2013. https://arxiv.org/abs/1305.5055
DOI [bibtex]
@conference{MRAMA2013,
title = {Modelling, Reduction and Analysis of Markov Automata},
author = {Dennis Guck and Hassan Hatefi and Holger Hermanns and Joost-Pieter Katoen and Mark Timmer},
publisher = {Springer},
booktitle = {LNCS},
volume = {8054},
pages = {34-50},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-40196-1_5},
url = { https://publications.rwth-aachen.de/record/224793},
}×
[issue]
Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, Mark Timmer. Modelling, Reduction and Analysis of Markov Automata, Quantitative Bewertung von Systemen (QEST 3013), Volume 8054 of LNCS, 34-50, Springer, 2013.
DOI [bibtex]
@conference{ASEG2013,
title = {A Semantics for Every GSPN},
author = {Christian Eisentraut and Holger Hermanns and Joost-Pieter Katoen and Lijun Zhang},
booktitle = {LNCS},
volume = {7927},
pages = {90-109},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-38697-8_6},
url = { https://publications.rwth-aachen.de/record/225412},
}×
[issue]
Christian Eisentraut, Holger Hermanns, Joost-Pieter Katoen, Lijun Zhang. A Semantics for Every GSPN, Application and Theory of Petri Nets and Concurrency : 34. International Conference (PETRI NETS 2013), Volume 7927 of LNCS, 90-109, 2013.
DOI [bibtex]
@conference{SBMMM2013,
title = {SMT-based Bisimulation Minimisation of Markov Models},
author = {Hans Christian Dehnert and David Parker and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {7737},
pages = {28-47},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-35873-9_5},
url = { https://publications.rwth-aachen.de/record/225435},
}×
[issue]
Hans Christian Dehnert, David Parker, Joost-Pieter Katoen. SMT-based Bisimulation Minimisation of Markov Models, Verification, Model Checking, and Abstract Interpretation [Elektronische Ressource] : 14. International Conference (VMCAI), Volume 7737 of LNCS, 28-47, Springer, 2013.
DOI [bibtex]
@conference{MBEOACS2013,
title = {Model-Based Energy Optimization of Automotive Control Systems},
author = {Joost-Pieter Katoen and Thomas Noll and Thomas Santen and Dirk Seifert and Hao Wu},
publisher = {IEEE},
pages = {761-766},
type = {Conference Paper},
year = {2013},
doi = {10.7873/date.2013.162},
url = { https://publications.rwth-aachen.de/record/225824},
}×
[issue]
Joost-Pieter Katoen, Thomas Noll, Thomas Santen, Dirk Seifert, Hao Wu. Model-Based Energy Optimization of Automotive Control Systems, 16. Design, Automation & Test in Europe Conference & Exhibition (DATE 2013), 761-766, IEEE, 2013.
DOI [bibtex]
@conference{TCMIPCS2013,
title = {Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems},
author = {Joost-Pieter Katoen and Doron Peled},
publisher = {Springer},
booktitle = {LNCS},
volume = {7792},
pages = {411-430},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-37036-6_23},
url = { https://publications.rwth-aachen.de/record/225915},
}×
[issue]
Joost-Pieter Katoen, Doron Peled. Taming Confusion for Modeling and Implementing Probabilistic Concurrent Systems, 22. European Symposium on Programming (ESOP 2013), Volume 7792 of LNCS, 411-430, Springer, 2013.
DOI [bibtex]
@inbook{CPTP2013,
title = {Concurrency meets Probability: Theory and Practice},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {8052},
pages = {44-45},
type = {Book Chapter},
year = {2013},
doi = {10.1007/978-3-642-40184-8_4},
url = { https://publications.rwth-aachen.de/record/226184},
}×
[issue]
Joost-Pieter Katoen. Concurrency meets Probability: Theory and Practice, Volume 8052 of LNCS, 44-45, Springer, 2013.
DOI [bibtex]
@conference{HCPA2013,
title = {High-level Counterexamples for Probabilistic Automata},
author = {Ralf Wimmer and Nils Jansen and Andreas Vorpahl and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {8054},
pages = {39-54},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-40196-1_4},
url = { https://publications.rwth-aachen.de/record/226401},
}×
[issue]
Ralf Wimmer, Nils Jansen, Andreas Vorpahl, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. High-level Counterexamples for Probabilistic Automata, Quantitative evaluation of systems : 10. international conference (QEST 2013), Volume 8054 of LNCS, 39-54, Springer, 2013.
DOI [bibtex]
@conference{PQPLI2013,
title = {PRINSYS: - on a Quest for Probabilistic Loop Invariants},
author = {Friedrich Gretz and Joost-Pieter Katoen and Annabelle McIver},
publisher = {Springer},
booktitle = {LNCS},
volume = {8054},
pages = {172-187},
type = {Conference Paper},
year = {2013},
doi = {10.1007/978-3-642-40196-1_17},
url = { https://publications.rwth-aachen.de/record/227648},
}×
[issue]
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. PRINSYS: - on a Quest for Probabilistic Loop Invariants, Quantitative evaluation of systems : 10. international conference (QEST 2013), Volume 8054 of LNCS, 172-187, Springer, 2013.
DOI [bibtex]
@conference{QACSNASHS2013,
title = {Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems},
author = {Ilya Tkachev and Alexandru Mereacre and Joost-Pieter Katoen and Alessandro Abate},
publisher = {ACM},
pages = {293-303},
type = {Conference Paper},
year = {2013},
doi = {10.1145/2461328.2461373},
url = { https://publications.rwth-aachen.de/record/227960},
}×
[issue]
Ilya Tkachev, Alexandru Mereacre, Joost-Pieter Katoen, Alessandro Abate. Quantitative Automata-based Controller Synthesis for Non-Autonomous Stochastic Hybrid Systems, 16. International Conference on Hybrid Systems, 293-303, ACM, 2013.
DOI [bibtex]
@inbook{MCMPAGI2013,
title = {Model Checking Meets Probability: A Gentle Introduction},
author = {Joost-Pieter Katoen},
publisher = {IOS Press},
booktitle = {NATO Science for Peace and Security Series - D: Information and Communication Security},
pages = {177-205},
type = {Book Chapter},
year = {2013},
doi = {10.3233/978-1-61499-207-3-177},
url = { https://publications.rwth-aachen.de/record/228249},
}×
[issue]
Joost-Pieter Katoen. Model Checking Meets Probability: A Gentle Introduction, NATO Science for Peace and Security Series - D: Information and Communication Security, 177-205, IOS Press, 2013.
DOI arXiv:1312.3979 [bibtex]
@unpublished{APPV2013,
title = {Accelerating Parametric Probabilistic Verification},
author = {Nils Jansen and Florian Corzilius and Matthias Volk and Ralf Wimmer and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
pages = {21 Seiten},
type = {Preprint},
year = {2013},
doi = {10.48550/ARXIV.1312.3979},
url = { https://arxiv.org/abs/1312.3979},
}×
[issue]
Nils Jansen, Florian Corzilius, Matthias Volk, Ralf Wimmer, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Accelerating Parametric Probabilistic Verification, 21 Seiten, 2013. https://arxiv.org/abs/1312.3979
DOI [bibtex]
@article{A2013,
title = {A compositional modelling and analysis framework for stochastic hybrid systems},
author = {Ernst Moritz Hahn and Arnd Hartmanns and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {43(2)},
pages = {pages 191-232},
type = {Journal Article},
year = {2013},
doi = {10.1007/s10703-012-0167-z},
url = { https://publications.rwth-aachen.de/record/234080},
}×
[issue]
Ernst Moritz Hahn, Arnd Hartmanns, Holger Hermanns, Joost-Pieter Katoen. A compositional modelling and analysis framework for stochastic hybrid systems, Formal methods in system design 43 (2), pages 191-232, Springer, 2013.
DOI [bibtex]
@article{M2013,
title = {Model checking for performability},
author = {Christel Baier and E. Moritz Hahn and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Cambridge Univ. Press},
journal = {Mathematical structures in computer science},
volume = {23(Special Issue 04)},
pages = {pages 751-795},
type = {Journal Article},
year = {2013},
doi = {10.1017/S0960129512000254},
url = { https://publications.rwth-aachen.de/record/234812},
}×
[issue]
Christel Baier, E. Moritz Hahn, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Model checking for performability, Mathematical structures in computer science 23 (Special Issue 04), pages 751-795, Cambridge Univ. Press, 2013.
DOI [bibtex]
@article{APA2013,
title = {Abstract Probabilistic Automata},
author = {Benoit Delahaye and Joost-Pieter Katoen and Kim G. Larsen and Axel Legay and Mikkel Pedersen and Falak Sher and Andrzej Wasowski},
publisher = {Academic Press [u.a.]},
journal = {Information and computation},
volume = {232},
pages = {pages 66-116},
type = {Journal Article},
year = {2013},
doi = {10.1016/j.ic.2013.10.002},
url = { https://publications.rwth-aachen.de/record/237094},
}×
[issue]
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski. Abstract Probabilistic Automata, Information and computation 232, pages 66-116, Academic Press [u.a.], 2013.
2012
fulltext PDF [bibtex]
@conference{M2012,
title = {Model checking of scenario-aware dataflow with cadp},
author = {Bart Theelen and Joost-Pieter Katoen and Hao Wu},
publisher = {IEEE},
pages = {653-658},
type = {Conference Paper},
year = {2012},
url = { https://publications.rwth-aachen.de/record/127054},
}×
[issue]
Bart Theelen, Joost-Pieter Katoen, Hao Wu. Model checking of scenario-aware dataflow with cadp, Design, Automation & Test in Europe Conference & Exhibition (DATE 2012), 653-658, IEEE, 2012.
DOI [bibtex]
@conference{MCSDTMM2012,
title = {Minimal Critical Subsystems for Discrete-Time Markov Models},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Bernd Becker and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {7214},
pages = {299-314},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-28756-5_21},
url = { https://publications.rwth-aachen.de/record/128454},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen. Minimal Critical Subsystems for Discrete-Time Markov Models, Tools and algorithms for the construction and analysis of systems : 18. international conference (TACAS 2012), Volume 7214 of LNCS, 299-314, Springer, 2012.
DOI [bibtex]
@conference{MCOCDMMTYT2012,
title = {Model Checking: One Can Do Much More Than You Think!},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {7141},
pages = {1-14},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-29320-7_1},
url = { https://publications.rwth-aachen.de/record/128834},
}×
[issue]
Joost-Pieter Katoen. Model Checking: One Can Do Much More Than You Think!, Fundamentals of software engineering : 4. IPM International conference (FSEN 2011), Volume 7141 of LNCS, 1-14, Springer, 2012.
DOI [bibtex]
@conference{QTAIMC2012,
title = {Quantitative Timed Analysis of Interactive Markov Chains},
author = {Dennis Guck and Tingting Han and Joost-Pieter Katoen and Martin R. Neuhäußer},
publisher = {Springer},
booktitle = {LNCS},
volume = {7226},
pages = {8-23},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-28891-3_4},
url = { https://publications.rwth-aachen.de/record/128848},
}×
[issue]
Dennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer. Quantitative Timed Analysis of Interactive Markov Chains, NASA formal methods : 4. international symposium (NFM 2012), Volume 7226 of LNCS, 8-23, Springer, 2012.
DOI [bibtex]
@article{TVAPS2012,
title = {Three-Valued Abstraction for Probabilistic Systems},
author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf},
publisher = {North-Holland},
journal = {The journal of logic and algebraic programming},
volume = {2012},
pages = {pages 1-55},
type = {Journal Article},
year = {2012},
doi = {10.1016/j.jlap.2012.03.007},
url = { https://publications.rwth-aachen.de/record/195992},
}×
[issue]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Three-Valued Abstraction for Probabilistic Systems, The journal of logic and algebraic programming 2012, pages 1-55, North-Holland, 2012.
DOI [bibtex]
@article{LRRDA2012,
title = {Layered Reasoning for Randomized Distributed Algorithms},
author = {Mani Swaminathan and Joost-Pieter Katoen and Ernst-Rüdiger Olderog},
journal = {Formal aspects of computing},
volume = {24(4/6)},
pages = {pages 477-496},
type = {Journal Article},
year = {2012},
doi = {10.1007/s00165-012-0231-x},
url = { https://publications.rwth-aachen.de/record/196292},
}×
[issue]
Mani Swaminathan, Joost-Pieter Katoen, Ernst-Rüdiger Olderog. Layered Reasoning for Randomized Distributed Algorithms, Formal aspects of computing 24 (4/6), pages 477-496, 2012.
fulltext PDF [bibtex]
@techreport{MCRRPMDP2012,
title = {Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
booktitle = {Reports of SFB/TR 14 AVACS},
volume = {88},
type = {Tech Report},
year = {2012},
url = { https://publications.rwth-aachen.de/record/197366},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal Counterexamples for Refuting omega-Regular Properties of Markov Decision Processes, Volume 88 of Reports of SFB/TR 14 AVACS, 2012.
DOI [bibtex]
@conference{EMGMA2012,
title = {Efficient Modelling and Generation of Markov Automata},
author = {Mark Timmer and Joost-Pieter Katoen and Jaco van de Pol and Marielle Stoelinga},
publisher = {Springer},
booktitle = {LNCS},
volume = {7454},
pages = {364-379},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-32940-1_26},
url = { https://publications.rwth-aachen.de/record/197708},
}×
[issue]
Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga. Efficient Modelling and Generation of Markov Automata, 23. international conference (CONCUR 2012), Volume 7454 of LNCS, 364-379, Springer, 2012.
DOI [bibtex]
@conference{RPMC2012,
title = {Robust PCTL Model Checking},
author = {Alessandro D'Innocenzo and Alessandro Abate and Joost-Pieter Katoen},
publisher = {ACM},
pages = {275-286},
type = {Conference Paper},
year = {2012},
doi = {10.1145/2185632.2185673},
url = { https://publications.rwth-aachen.de/record/197747},
}×
[issue]
Alessandro D'Innocenzo, Alessandro Abate, Joost-Pieter Katoen. Robust PCTL Model Checking, 15. International Conference on Hybrid Systems, 275-286, ACM, 2012.
DOI [bibtex]
@conference{FCSDPAS2012,
title = {Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite},
author = {Marie-Aude Esteve and Joost-Pieter Katoen and Viet Yen Nguyen and Bart Postma and Yuri Yushtein},
publisher = {IEEE},
booktitle = {ICSE 2012},
pages = {1022-1031},
type = {Conference Paper},
year = {2012},
doi = {10.1109/ICSE.2012.6227118},
url = { https://publications.rwth-aachen.de/record/197902},
}×
[issue]
Marie-Aude Esteve, Joost-Pieter Katoen, Viet Yen Nguyen, Bart Postma, Yuri Yushtein. Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite, 34. International Conference on Software Engineering (ICSE 2012), ICSE 2012, 1022-1031, IEEE, 2012.
DOI [bibtex]
@conference{CATPA2012,
title = {Compositional Abstraction Techniques for Probabilistic Automata},
author = {Falak Sher and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {7604},
pages = {325-341},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-33475-7_23},
url = { https://publications.rwth-aachen.de/record/197943},
}×
[issue]
Falak Sher, Joost-Pieter Katoen. Compositional Abstraction Techniques for Probabilistic Automata, 7. IFIP TC1/WG 2.2 international conference (TCS 2012), Volume 7604 of LNCS, 325-341, Springer, 2012.
DOI [bibtex]
@conference{GRSSNAA2012,
title = {GSPNs Revisited: Simple Semantics and New Analysis Algorithms},
author = {Joost-Pieter Katoen},
publisher = {IEEE},
pages = {6-12},
type = {Conference Paper},
year = {2012},
doi = {10.1109/ACSD.2012.30},
url = { https://publications.rwth-aachen.de/record/197944},
}×
[issue]
Joost-Pieter Katoen. GSPNs Revisited: Simple Semantics and New Analysis Algorithms, 12. International Conference on Application of Concurrency to System Design (ACSD 2012), 6-12, IEEE, 2012.
DOI [bibtex]
@conference{OWPSPGCL2012,
title = {Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language},
author = {Friedrich Gretz and Joost-Pieter Katoen and Annabelle McIver},
publisher = {IEEE CS Press},
pages = {168-177},
type = {Conference Paper},
year = {2012},
doi = {10.1109/QEST.2012.21},
url = { https://publications.rwth-aachen.de/record/197949},
}×
[issue]
Friedrich Gretz, Joost-Pieter Katoen, Annabelle McIver. Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language, 9. International Conference on Quantitative Evaluation of Systems (QEST), 168-177, IEEE CS Press, 2012.
[bibtex]
@conference{MCSCRDP2012,
title = {Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties},
author = {Ralf Wimmer and Nils Jansen and Erika Ábrahám and Joost-Pieter Katoen and Bernd Becker},
publisher = {Kovač},
booktitle = {Schriftenreihe Forschungsergebnisse zur Informatik},
volume = {68},
pages = {169-180},
type = {Conference Paper},
year = {2012},
url = { https://publications.rwth-aachen.de/record/198077},
}×
[issue]
Ralf Wimmer, Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen, Bernd Becker. Minimal Critical Subsystems as Counterexamples for ω-Regular DTMC Properties, 15. Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV 2012), Volume 68 of Schriftenreihe Forschungsergebnisse zur Informatik, 169-180, Kovač, 2012.
DOI [bibtex]
@conference{WLMC2012,
title = {Weighted Lumpability on Markov Chains},
author = {Arpit Sharma and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {7162},
pages = {322-339},
type = {Conference Paper},
year = {2012},
doi = {10.1007/978-3-642-29709-0_28},
url = { https://publications.rwth-aachen.de/record/228241},
}×
[issue]
Arpit Sharma, Joost-Pieter Katoen. Weighted Lumpability on Markov Chains, Perspectives of system informatics : 8. International Ershov Informatics Conference, Volume 7162 of LNCS, 322-339, Springer, 2012.
2011
DOI [bibtex]
@proceedings{C2011,
title = {CONCUR 2011 - concurrency theory},
author = {},
editor = {Joost-Pieter Katoen and B. Koenig},
publisher = {Springer},
booktitle = {LNCS},
volume = {6901},
pages = {XIV, 560 S. : graph. Darst.},
type = {Proceeding Article},
year = {2011},
doi = {10.1007/978-3-642-23217-6},
url = { https://publications.rwth-aachen.de/record/47744},
}×
[issue]
Joost-Pieter Katoen (ed), B. Koenig (ed). CONCUR 2011 - concurrency theory, Volume 6901 of LNCS, XIV, 560 S. : graph. Darst., Springer, 2011.
DOI [bibtex]
@conference{T2011,
title = {Towards trustworthy aerospace systems: an experience report},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {6959},
pages = {1-4},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-24431-5_1},
url = { https://publications.rwth-aachen.de/record/93682},
}×
[issue]
Joost-Pieter Katoen. Towards trustworthy aerospace systems: an experience report, 16. International Workshop: Formal Methods for Industrial Critical Systems (FMICS 2011), Volume 6959 of LNCS, 1-4, Springer, 2011.
DOI [bibtex]
@conference{OCTMCTA2011,
title = {Observing Continuous-Time MDPs by 1-Clock Timed Automata},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {Springer},
booktitle = {LNCS},
volume = {6945},
pages = {2-25},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-24288-5},
url = { https://publications.rwth-aachen.de/record/100789},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Observing Continuous-Time MDPs by 1-Clock Timed Automata, 5. international workshop: Reachability problems (RP 2011), Volume 6945 of LNCS, 2-25, Springer, 2011.
DOI [bibtex]
@conference{QAMCASHS2011,
title = {Quantitative Automata Model Checking of Autonomous Stochastic Hybrid Systems},
author = {Alessandro Abate and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {ACM Press},
pages = {83-92},
type = {Conference Paper},
year = {2011},
doi = {10.1145/1967701.1967715},
url = { https://publications.rwth-aachen.de/record/124907},
}×
[issue]
Alessandro Abate, Joost-Pieter Katoen, Alexandru Mereacre. Quantitative Automata Model Checking of Autonomous Stochastic Hybrid Systems, 14. ACM International Conference on Hybrid Systems:Computation and Control (HSCC'11), 83-92, ACM Press, 2011.
DOI [bibtex]
@conference{ECMCLRTO2011,
title = {Efficient CTMC Model Checking of Linear Real-Time Objectives},
author = {Benoit Barbot and Taolue Chen and Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {Springer},
booktitle = {LNCS},
volume = {6605},
pages = {128-142},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-19835-9_12},
url = { https://publications.rwth-aachen.de/record/124908},
}×
[issue]
Benoit Barbot, Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Efficient CTMC Model Checking of Linear Real-Time Objectives, Tools and algorithms for the construction and analysis of systems : 17. international conference, TACAS 2011, held as part of the Joint European Conference on Theory and Practice of Software, ETAPS 2011, Volume 6605 of LNCS, 128-142, Springer, 2011.
DOI [bibtex]
@conference{APA2011,
title = {Abstract Probabilistic Automata},
author = {Benoit Delahaye and Joost-Pieter Katoen and Kim G. Larsen and Axel Legay and Mikkel Pedersen and Falak Sher and Andrzej Wasowski},
publisher = {Springer},
booktitle = {LNCS},
volume = {6538},
pages = {324-339},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-18275-4_23},
url = { https://publications.rwth-aachen.de/record/124909},
}×
[issue]
Benoit Delahaye, Joost-Pieter Katoen, Kim G. Larsen, Axel Legay, Mikkel Pedersen, Falak Sher, Andrzej Wasowski. Abstract Probabilistic Automata, Verification, model checking, and abstract interpretation : 12th international conference (VMCAI 2011), Volume 6538 of LNCS, 324-339, Springer, 2011.
DOI [bibtex]
@conference{ALGNFHRG2011,
title = {A Local Greibach Normal Form for Hyperedge Replacement Grammars},
author = {Christina Jansen and Jonathan Heinen and Joost-Pieter Katoen and Thomas Noll},
publisher = {Springer},
booktitle = {LNCS},
volume = {6638},
pages = {323-335},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-21254-3},
url = { https://publications.rwth-aachen.de/record/124910},
}×
[issue]
Christina Jansen, Jonathan Heinen, Joost-Pieter Katoen, Thomas Noll. A Local Greibach Normal Form for Hyperedge Replacement Grammars, Language and automata theory and applications : 5. international conference (LATA 2011), Volume 6638 of LNCS, 323-335, Springer, 2011.
DOI [bibtex]
@conference{R2011,
title = {Reachability probabilities in markovian timed automata},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen and A. Mereacre},
publisher = {IEEE},
pages = {7075-7080},
type = {Conference Paper},
year = {2011},
doi = {10.1109/CDC.2011.6160992},
url = { https://publications.rwth-aachen.de/record/124969},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, A. Mereacre. Reachability probabilities in markovian timed automata, 50. IEEE Conference on Decision and Control and European Control Conference (CDC-ECC 2011), 7075-7080, IEEE, 2011.
DOI [bibtex]
@conference{H2011,
title = {Hierarchical counterexamples for discrete-time markov chains},
author = {Nils Jansen and Erika Ábrahám and Jens Katelaan and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker},
publisher = {Springer},
booktitle = {LNCS},
volume = {6996},
pages = {443-452},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-24372-1_33},
url = { https://publications.rwth-aachen.de/record/128557},
}×
[issue]
Nils Jansen, Erika Ábrahám, Jens Katelaan, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. Hierarchical counterexamples for discrete-time markov chains, Automated technolgoy for verification and analysis : 9. international symposium (ATVA 2011), Volume 6996 of LNCS, 443-452, Springer, 2011.
DOI [bibtex]
@article{A2011,
title = {A linear process-algebraic format with data for probabilistic automata},
author = {Joost-Pieter Katoen and Jaco van de Pol and Mariëlle Stoelinga and Mark Timmer},
publisher = {Elsevier},
journal = {Theoretical computer science},
volume = {413(1)},
pages = {pages 36-57},
type = {Journal Article},
year = {2011},
doi = {10.1016/j.tcs.2011.07.021},
url = { https://publications.rwth-aachen.de/record/131713},
}×
[issue]
Joost-Pieter Katoen, Jaco van de Pol, Mariëlle Stoelinga, Mark Timmer. A linear process-algebraic format with data for probabilistic automata, Theoretical computer science 413 (1), pages 36-57, Elsevier, 2011.
[bibtex]
@article{TAS2011,
title = {Trustworthy Aerospace Systems},
author = {Joost-Pieter Katoen and Thomas Noll},
publisher = {PS, PublicService.co.uk Ltd},
journal = {Public service review},
volume = {11},
pages = {pages 204-205},
type = {Journal Article},
year = {2011},
url = { https://publications.rwth-aachen.de/record/169201},
}×
[issue]
Joost-Pieter Katoen, Thomas Noll. Trustworthy Aerospace Systems, Public service review 11, pages 204-205, PS, PublicService.co.uk Ltd, 2011.
DOI fulltext PDF [bibtex]
@article{MCCTMCATAS2011,
title = {Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig},
journal = {Logical methods in computer science},
volume = {7(1/2)},
pages = {pages 12},
type = {Journal Article},
year = {2011},
doi = {10.2168/LMCS-7(1:12)2011},
url = { https://publications.rwth-aachen.de/record/184368},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications, Logical methods in computer science 7 (1/2), pages 12, Department of Theoretical Computer Science, Technical University of Braunschweig, 2011.
DOI [bibtex]
@article{TIOPMCM2011,
title = {The Ins and Outs of the Probabilistic Model Checker MRMC},
author = {Joost-Pieter Katoen and Ivan S. Zapreev and Ernst Moritz Hahn and Holger Hermanns and David N. Jansen},
publisher = {Elsevier},
journal = {Performance evaluation},
volume = {68(2)},
pages = {pages 90-104},
type = {Journal Article},
year = {2011},
doi = {10.1016/j.peva.2010.04.001},
url = { https://publications.rwth-aachen.de/record/184369},
}×
[issue]
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen. The Ins and Outs of the Probabilistic Model Checker MRMC, Performance evaluation 68 (2), pages 90-104, Elsevier, 2011.
DOI [bibtex]
@article{TQ2011,
title = {Time-bounded reachability in tree-structured QBDs by abstraction},
author = {Daniel Klink and Anne Remke and Boudewijn R. Haverkort and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Performance evaluation},
volume = {68(2)},
pages = {pages 105-125},
type = {Journal Article},
year = {2011},
doi = {10.1016/j.peva.2010.04.002},
url = { https://publications.rwth-aachen.de/record/195576},
}×
[issue]
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen. Time-bounded reachability in tree-structured QBDs by abstraction, Performance evaluation 68 (2), pages 105-125, Elsevier, 2011.
DOI [bibtex]
@conference{DPSPPAFSS2011,
title = {Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems},
author = {Hongfei Fu and Joost-Pieter Katoen},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH},
booktitle = {Leibniz International Proceedings in Informatics},
volume = {13},
pages = {445-456},
type = {Conference Paper},
year = {2011},
doi = {10.4230/LIPIcs.FSTTCS.2011.445},
url = { https://publications.rwth-aachen.de/record/225365},
}×
[issue]
Hongfei Fu, Joost-Pieter Katoen. Deciding Probabilistic Simulation between Probabilistic Pushdown Automata and Finite-State Systems, Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), Volume 13 of Leibniz International Proceedings in Informatics, 445-456, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, 2011.
DOI [bibtex]
@conference{A2011,
title = {A two-step scheme for approximate model checking of stochastic hybrid systems},
author = {Alessandro Abate and Joost-Pieter Katoen and John Lygeros and Maria Prandini},
pages = {4519-4524},
type = {Conference Paper},
year = {2011},
doi = {10.3182/20110828-6-IT-1002.02905},
url = { https://publications.rwth-aachen.de/record/225372},
}×
[issue]
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, Maria Prandini. A two-step scheme for approximate model checking of stochastic hybrid systems, 18. IFAC World Congress 2011, 4519-4524, 2011.
DOI [bibtex]
@conference{SSCEDSP2011,
title = {System-Software Co-Engineering: Dependability and Safety Perspective},
author = {Yuri Yushtein and Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Xavier Olive and Marco Roveri},
publisher = {IEEE CS Press},
pages = {18-25},
type = {Conference Paper},
year = {2011},
doi = {10.1109/SMC-IT.2011.16},
url = { https://publications.rwth-aachen.de/record/227417},
}×
[issue]
Yuri Yushtein, Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Xavier Olive, Marco Roveri. System-Software Co-Engineering: Dependability and Safety Perspective, 4. IEEE International Conference on Space Mission Challenges for Information Technology (SMC-IT 2011), 18-25, IEEE CS Press, 2011.
DOI [bibtex]
@conference{AIEEDSA2011,
title = {Analysing and Improving Energy Efficiency of Distributed Slotted Aloha},
author = {Haidi Yue and Henrik Bohnenkamp and Malte Kampschulte and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {6869},
pages = {197-208},
type = {Conference Paper},
year = {2011},
doi = {10.1007/978-3-642-22875-9_18},
url = { https://publications.rwth-aachen.de/record/227423},
}×
[issue]
Haidi Yue, Henrik Bohnenkamp, Malte Kampschulte, Joost-Pieter Katoen. Analysing and Improving Energy Efficiency of Distributed Slotted Aloha, Smart spaces and next generation wired/wireless networking : 11th international conference (NEW2AN 2011), Volume 6869 of LNCS, 197-208, Springer, 2011.
2010
fulltext PDF [bibtex]
@techreport{CMRPMTA2010,
title = {Computing Maximum Reachability Probabilities in Markovian Timed Automata},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {RWTH Aachen, Department of Computer Science},
booktitle = {Aachener Informatik Berichte},
volume = {2010.06},
pages = {40 S.},
type = {Tech Report},
year = {2010},
url = { https://publications.rwth-aachen.de/record/47988},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Computing Maximum Reachability Probabilities in Markovian Timed Automata, Volume 2010.06 of Aachener Informatik Berichte, 40 S., RWTH Aachen, Department of Computer Science, 2010.
DOI [bibtex]
@conference{TALF2010,
title = {libalf: The Automata Learning Framework},
author = {Benedikt Bollig and Carsten Kern and Joost-Pieter Katoen and Daniel Neider and David R. Piegdon},
publisher = {Springer},
booktitle = {LNCS},
volume = {6174},
pages = {360-364},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-14295-6_32},
url = { https://publications.rwth-aachen.de/record/83828},
}×
[issue]
Benedikt Bollig, Carsten Kern, Joost-Pieter Katoen, Daniel Neider, David R. Piegdon. libalf: The Automata Learning Framework, 22. international conference: Computer aided verification (CAV 2010), Volume 6174 of LNCS, 360-364, Springer, 2010.
DOI [bibtex]
@conference{DMCSR2010,
title = {DTMC Model Checking by SCC Reduction},
author = {Erika Ábrahám and Nils Jansen and Ralf Wimmer and Joost-Pieter Katoen and Bernd Becker},
publisher = {IEEE Computer Society},
pages = {37-46},
type = {Conference Paper},
year = {2010},
doi = {10.1109/QEST.2010.13},
url = { https://publications.rwth-aachen.de/record/119427},
}×
[issue]
Erika Ábrahám, Nils Jansen, Ralf Wimmer, Joost-Pieter Katoen, Bernd Becker. DTMC Model Checking by SCC Reduction, 7. International Conference on the Quantitative Evaluation of Systems (QEST 2010), 37-46, IEEE Computer Society, 2010.
DOI [bibtex]
@conference{MCMCKSMAER2010,
title = {Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report},
author = {Falko Dulat and Joost-Pieter Katoen and Viet Yen Nguyen},
publisher = {Springer},
booktitle = {LNCS},
volume = {6342},
pages = {115-130},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-15784-4_8},
url = { https://publications.rwth-aachen.de/record/120049},
}×
[issue]
Falko Dulat, Joost-Pieter Katoen, Viet Yen Nguyen. Model Checking Markov Chains using Krylov Subspace Methods: An Experience Report, 7. European Performance Engineering Workshop: Computer performance engineering (EPEW 2010), Volume 6342 of LNCS, 115-130, Springer, 2010.
DOI [bibtex]
@conference{LEARNMCEC2010,
title = {Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption},
author = {Haidi Yue and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {6148},
pages = {247-261},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-13568-2_18},
url = { https://publications.rwth-aachen.de/record/120052},
}×
[issue]
Haidi Yue, Joost-Pieter Katoen. Leader Election in Anonymous Radio Networks: Model Checking Energy Consumption, 17. international conference: Analytical and stochastic modeling techniques and applications (ASMTA 2010), Volume 6148 of LNCS, 247-261, Springer, 2010.
DOI [bibtex]
@conference{AECGMP2010,
title = {Analyzing Energy Consumption in a Gossiping MAC Protocol},
author = {Haidi Yue and Henrik Bohnenkamp and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {5987},
pages = {107-119},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-12104-3_10},
url = { https://publications.rwth-aachen.de/record/120053},
}×
[issue]
Haidi Yue, Henrik Bohnenkamp, Joost-Pieter Katoen. Analyzing Energy Consumption in a Gossiping MAC Protocol, 15. international GI/ITG conference: Measurement, modelling and evaluation of computing systems and dependability in fault tolerance (MMB&DFT 2010), Volume 5987 of LNCS, 107-119, Springer, 2010.
DOI [bibtex]
@conference{LIGPPASPBM2010,
title = {Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods},
author = {Joost-Pieter Katoen and Annabelle McIver and Larissa Meinicke and Carroll Morgan},
publisher = {Springer},
booktitle = {LNCS},
volume = {6337 : Advanced Research in Computing and Software Science},
pages = {390-406},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-15769-1_24},
url = { https://publications.rwth-aachen.de/record/120056},
}×
[issue]
Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, Carroll Morgan. Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods, 17. international symposium: Static analysis (SAS 2010), Volume 6337 : Advanced Research in Computing and Software Science of LNCS, 390-406, Springer, 2010.
DOI [bibtex]
@conference{APMC2010,
title = {Advances in Probabilistic Model Checking},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {5944},
pages = {25},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-11319-2_5},
url = { https://publications.rwth-aachen.de/record/120057},
}×
[issue]
Joost-Pieter Katoen. Advances in Probabilistic Model Checking, 11. international conference: Verification, model checking, and abstract interpretation (VMCAI 2010), Volume 5944 of LNCS, 25, Springer, 2010.
DOI [bibtex]
@conference{ALPAFPSD2010,
title = {A Linear Process Algebraic Format for Probabilistic Systems with Data},
author = {Joost-Pieter Katoen and Jaco van de Pol and Marielle Stoelinga and Mark Timmer},
publisher = {IEEE Computer Soc.},
pages = {213-222},
type = {Conference Paper},
year = {2010},
doi = {10.1109/ACSD.2010.18},
url = { https://publications.rwth-aachen.de/record/120058},
}×
[issue]
Joost-Pieter Katoen, Jaco van de Pol, Marielle Stoelinga, Mark Timmer. A Linear Process Algebraic Format for Probabilistic Systems with Data, 10. International Conference on Application of Concurrency to System Design (ACSD 2010), 213-222, IEEE Computer Soc., 2010.
DOI [bibtex]
@conference{THWIMC2010,
title = {The How and Why of Interactive Markov Chains},
author = {Holger Hermanns and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {6286},
pages = {311-337},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-17071-3_16},
url = { https://publications.rwth-aachen.de/record/120059},
}×
[issue]
Holger Hermanns, Joost-Pieter Katoen. The How and Why of Interactive Markov Chains, 8. international symposium: Formal methods for components and objects (FMCO 2009), Volume 6286 of LNCS, 311-337, Springer, 2010.
DOI [bibtex]
@conference{AMCA2010,
title = {A Model Checker for AADL},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri and Ralf Wimmer},
publisher = {Springer},
booktitle = {LNCS},
volume = {6174},
pages = {562-565},
type = {Conference Paper},
year = {2010},
doi = {10.1007/978-3-642-14295-6_48},
url = { https://publications.rwth-aachen.de/record/120064},
}×
[issue]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri, Ralf Wimmer. A Model Checker for AADL, 22. international conference: Computer aided verification (CAV 2010), Volume 6174 of LNCS, 562-565, Springer, 2010.
DOI [bibtex]
@article{COSBUES2010,
title = {Computing Optimal Schedules for Battery Usage in Embedded Systems},
author = {Marijn R. Jongerden and Alexandru Mereacre and Henrik Bohnenkamp and Boudewijn R. Haverkort and Joost-Pieter Katoen},
publisher = {IEEE},
journal = {IEEE transactions on industrial informatics},
volume = {6(3)},
pages = {pages 276-286},
type = {Journal Article},
year = {2010},
doi = {10.1109/TII.2010.2051813},
url = { https://publications.rwth-aachen.de/record/171681},
}×
[issue]
Marijn R. Jongerden, Alexandru Mereacre, Henrik Bohnenkamp, Boudewijn R. Haverkort, Joost-Pieter Katoen. Computing Optimal Schedules for Battery Usage in Embedded Systems, IEEE transactions on industrial informatics 6 (3), pages 276-286, IEEE, 2010.
DOI [bibtex]
@article{SDPAEAM2010,
title = {Safety, Dependability, and Performance Analysis of Extended AADL Models},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {Univ. Press},
journal = {Computer journal},
volume = {51},
type = {Journal Article},
year = {2010},
doi = {10.1093/comjnl/bxq024},
url = { https://publications.rwth-aachen.de/record/171721},
}×
[issue]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Safety, Dependability, and Performance Analysis of Extended AADL Models, Computer journal 51, Univ. Press, 2010.
fulltext PDF [bibtex]
@article{STSMA2010,
title = {SMA: The Smyle Modeling Approach},
author = {Benedikt Bollig and Joost-Pieter Katoen and Carsten Kern and Martin Leucker},
publisher = {VEDA, Slov. Akad. Vied},
journal = {Computing and informatics},
volume = {29},
pages = {pages 45-72},
type = {Journal Article},
year = {2010},
url = { https://publications.rwth-aachen.de/record/171722},
}×
[issue]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. SMA: The Smyle Modeling Approach, Computing and informatics 29, pages 45-72, VEDA, Slov. Akad. Vied, 2010.
DOI [bibtex]
@article{LCAM2010,
title = {Learning Communicating Automata from MSCs},
author = {Benedikt Bollig and Joost-Pieter Katoen and Carsten Kern and Martin Leucker},
publisher = {IEEE},
journal = {IEEE transactions on software engineering},
volume = {36(3)},
pages = {pages 390-408},
type = {Journal Article},
year = {2010},
doi = {10.1109/TSE.2009.89},
url = { https://publications.rwth-aachen.de/record/171723},
}×
[issue]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. Learning Communicating Automata from MSCs, IEEE transactions on software engineering 36 (3), pages 390-408, IEEE, 2010.
DOI [bibtex]
@article{PEMCJF2010,
title = {Performance Evaluation and Model Checking Join Forces},
author = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Association for Computing Machinery},
journal = {Communications of the ACM},
volume = {53(9)},
pages = {pages 76-85},
type = {Journal Article},
year = {2010},
doi = {10.1145/1810891.1810912},
url = { https://publications.rwth-aachen.de/record/171724},
}×
[issue]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Performance Evaluation and Model Checking Join Forces, Communications of the ACM 53 (9), pages 76-85, Association for Computing Machinery, 2010.
DOI [bibtex]
@article{PAMCMRM2010,
title = {Performability Assessment by Model Checking of Markov Reward Models},
author = {Christel Baier and Lucia Cloth and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Springer},
journal = {Formal methods in system design},
volume = {36(1)},
pages = {pages 1-36},
type = {Journal Article},
year = {2010},
doi = {10.1007/s10703-009-0088-7},
url = { https://publications.rwth-aachen.de/record/171725},
}×
[issue]
Christel Baier, Lucia Cloth, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Performability Assessment by Model Checking of Markov Reward Models, Formal methods in system design 36 (1), pages 1-36, Springer, 2010.
DOI [bibtex]
@article{A2010,
title = {Approximate model checking of stochastic hybrid systems},
author = {Alessandro Abate and Joost-Pieter Katoen and John Lygeros and Maria Prandini},
publisher = {Hermes [u.a.]},
journal = {European journal of control},
volume = {16(6)},
pages = {pages 624-641},
type = {Journal Article},
year = {2010},
doi = {10.3166/ejc.16.624-641},
url = { https://publications.rwth-aachen.de/record/171727},
}×
[issue]
Alessandro Abate, Joost-Pieter Katoen, John Lygeros, Maria Prandini. Approximate model checking of stochastic hybrid systems, European journal of control 16 (6), pages 624-641, Hermes [u.a.], 2010.
2009
fulltext PDF [bibtex]
@techreport{QM2009,
title = {Quantitative model checking of continuous-time Markov chains against timed automata specifications},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {RWTH Aachen, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2009,2},
pages = {50 S.},
type = {Tech Report},
year = {2009},
url = { https://publications.rwth-aachen.de/record/47815},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Quantitative model checking of continuous-time Markov chains against timed automata specifications, Volume 2009,2 of Aachener Informatik-Berichte, 50 S., RWTH Aachen, Department of Computer Science, 2009.
fulltext PDF [bibtex]
@techreport{CASS2009,
title = {Compositional Abstraction for Stochastic Systems},
author = {Joost-Pieter Katoen and Daniel Klink and Martin R. Neuhäußer},
publisher = {RWTH Aachen, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2009,15},
pages = {32 S.},
type = {Tech Report},
year = {2009},
url = { https://publications.rwth-aachen.de/record/47816},
}×
[issue]
Joost-Pieter Katoen, Daniel Klink, Martin R. Neuhäußer. Compositional Abstraction for Stochastic Systems, Volume 2009,15 of Aachener Informatik-Berichte, 32 S., RWTH Aachen, Department of Computer Science, 2009.
DOI [bibtex]
@inbook{TCACMPAS2009,
title = {The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {Springer},
booktitle = {LNCS},
volume = {5775},
pages = {173-186},
type = {Book Chapter},
year = {2009},
doi = {10.1007/978-3-642-04468-7_15},
url = { https://publications.rwth-aachen.de/record/83788},
}×
[issue]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. The COMPASS Approach: Correctness, Modelling and Performability of Aerospace Systems, Volume 5775 of LNCS, 173-186, Springer, 2009.
DOI [bibtex]
@inbook{LM2009,
title = {LTL model checking of time-inhomogeneous Markov chains},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {Springer},
booktitle = {LNCS},
volume = {5799},
pages = {104-119},
type = {Book Chapter},
year = {2009},
doi = {10.1007/978-3-642-04761-9_10},
url = { https://publications.rwth-aachen.de/record/83789},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. LTL model checking of time-inhomogeneous Markov chains, Volume 5799 of LNCS, 104-119, Springer, 2009.
DOI [bibtex]
@inbook{CASS2009,
title = {Compositional Abstraction for Stochastic Systems},
author = {Joost-Pieter Katoen and Daniel Klink and Martin R. Neuhäußer},
publisher = {Springer},
booktitle = {LNCS},
volume = {5813},
pages = {195-211},
type = {Book Chapter},
year = {2009},
doi = {10.1007/978-3-642-04368-0_16},
url = { https://publications.rwth-aachen.de/record/83790},
}×
[issue]
Joost-Pieter Katoen, Daniel Klink, Martin R. Neuhäußer. Compositional Abstraction for Stochastic Systems, Volume 5813 of LNCS, 195-211, Springer, 2009.
DOI [bibtex]
@inbook{DNCTMDP2009,
title = {Delayed Nondeterminism in Continuous-Time Markov Decision Processes},
author = {Martin R. Neuhäußer and Marielle Stoelinga and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {5504},
pages = {364-379},
type = {Book Chapter},
year = {2009},
doi = {10.1007/978-3-642-00596-1_26},
url = { https://publications.rwth-aachen.de/record/83791},
}×
[issue]
Martin R. Neuhäußer, Marielle Stoelinga, Joost-Pieter Katoen. Delayed Nondeterminism in Continuous-Time Markov Decision Processes, Volume 5504 of LNCS, 364-379, Springer, 2009.
DOI [bibtex]
@conference{CDSACBML2009,
title = {Codesign of Dependable Systems: A Component-Based Modeling Language},
author = {Marco Bozzano and Alessandro Cimatti and Marco Roveri and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll},
publisher = {IEEE},
pages = {121-130},
type = {Conference Paper},
year = {2009},
doi = {10.1109/MEMCOD.2009.5185388},
url = { https://publications.rwth-aachen.de/record/100524},
}×
[issue]
Marco Bozzano, Alessandro Cimatti, Marco Roveri, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll. Codesign of Dependable Systems: A Component-Based Modeling Language, 7. ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 121-130, IEEE, 2009.
fulltext PDF [bibtex]
@conference{MBCCES2009,
title = {Model-Based Codesign of Critical Embedded Systems},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {RWTH Aachen},
booktitle = {CEUR Workshop Proceedings},
volume = {507},
pages = {87-91},
type = {Conference Paper},
year = {2009},
url = { https://publications.rwth-aachen.de/record/100526},
}×
[issue]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Model-Based Codesign of Critical Embedded Systems, 2. International Workshop on Model Based Architecting and Construction of Embedded Systems (ACES-MB 2009), Volume 507 of CEUR Workshop Proceedings, 87-91, RWTH Aachen, 2009.
[bibtex]
@conference{VPEAMTD2009,
title = {Verification and Performance Evaluation of AADL Models (Tool Demonstration)},
author = {Marco Bozzano and Alessandro Cimatti and Joost-Pieter Katoen and Viet Yen Nguyen and Thomas Noll and Marco Roveri},
publisher = {ACM},
pages = {285-286},
type = {Conference Paper},
year = {2009},
url = { https://publications.rwth-aachen.de/record/100527},
}×
[issue]
Marco Bozzano, Alessandro Cimatti, Joost-Pieter Katoen, Viet Yen Nguyen, Thomas Noll, Marco Roveri. Verification and Performance Evaluation of AADL Models (Tool Demonstration), Joint 12. European Software Engineering Conference and 17. ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC-FSE’09), 285-286, ACM, 2009.
DOI [bibtex]
@conference{QMCCTMCATAS2009,
title = {Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {IEEE},
pages = {309-318},
type = {Conference Paper},
year = {2009},
doi = {10.1109/LICS.2009.21},
url = { https://publications.rwth-aachen.de/record/100528},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Quantitative Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications, 24. Annual IEEE Symposium on Logic in Computer Science (LICS 2009), 309-318, IEEE, 2009.
DOI [bibtex]
@conference{MSLBS2009,
title = {Maximizing System Lifetime by Battery Scheduling},
author = {Marijn R. Jongerden and Boudewijn R. Haverkort and Henrik Bohnenkamp and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {63-72},
type = {Conference Paper},
year = {2009},
doi = {10.1109/DSN.2009.5270351},
url = { https://publications.rwth-aachen.de/record/100530},
}×
[issue]
Marijn R. Jongerden, Boudewijn R. Haverkort, Henrik Bohnenkamp, Joost-Pieter Katoen. Maximizing System Lifetime by Battery Scheduling, 2009 IEEE/IFIP International Conference on Dependable Systems & Networks (DSN 2009), 63-72, IEEE, 2009.
DOI [bibtex]
@conference{SCMCAEE2009,
title = {Simulation-based CTMC Model Checking: An Empirical Evaluation},
author = {Joost-Pieter Katoen and Ivan S. Zapreev},
publisher = {IEEE},
pages = {31-40},
type = {Conference Paper},
year = {2009},
doi = {10.1109/QEST.2009.25},
url = { https://publications.rwth-aachen.de/record/100531},
}×
[issue]
Joost-Pieter Katoen, Ivan S. Zapreev. Simulation-based CTMC Model Checking: An Empirical Evaluation, 6. International Conference on the Quantitative Evaluation of Systems (QUEST 2009), 31-40, IEEE, 2009.
DOI [bibtex]
@conference{TBRTSQA2009,
title = {Time-Bounded Reachability in Tree-Structured QBDs by Abstraction},
author = {Daniel Klink and Anne Remke and Boudewijn R. Haverkort and Joost-Pieter Katoen},
publisher = {IEEE},
booktitle = {International Conference on Quantitative Evaluation of Systems-QEST},
pages = {133-142},
type = {Conference Paper},
year = {2009},
doi = {10.1109/QEST.2009.9},
url = { https://publications.rwth-aachen.de/record/124913},
}×
[issue]
Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen. Time-Bounded Reachability in Tree-Structured QBDs by Abstraction, 6. International Conference on the Quantitative Evaluation of Systems (QEST'09), International Conference on Quantitative Evaluation of Systems-QEST, 133-142, IEEE, 2009.
DOI [bibtex]
@conference{TIOTPMCM2009,
title = {The Ins and Outs of The Probabilistic Model Checker MRMC},
author = {Joost-Pieter Katoen and Ivan S. Zapreev and Ernst Moritz Hahn and Holger Hermanns and David N. Jansen},
publisher = {IEEE},
booktitle = {International Conference on Quantitative Evaluation of Systems-QEST},
pages = {167-176},
type = {Conference Paper},
year = {2009},
doi = {10.1109/QEST.2009.11},
url = { https://publications.rwth-aachen.de/record/127000},
}×
[issue]
Joost-Pieter Katoen, Ivan S. Zapreev, Ernst Moritz Hahn, Holger Hermanns, David N. Jansen. The Ins and Outs of The Probabilistic Model Checker MRMC, 6. International Conference on the Quantitative Evaluation of Systems (QEST '09), International Conference on Quantitative Evaluation of Systems-QEST, 167-176, IEEE, 2009.
DOI [bibtex]
@article{CGPMC2009,
title = {Counterexample Generation in Probabilistic Model Checking},
author = {Tingting Han and Joost-Pieter Katoen and Berteun Damman},
publisher = {IEEE},
journal = {IEEE transactions on software engineering},
volume = {35(2)},
pages = {pages 241-257},
type = {Journal Article},
year = {2009},
doi = {10.1109/TSE.2009.5},
url = { https://publications.rwth-aachen.de/record/134125},
}×
[issue]
Tingting Han, Joost-Pieter Katoen, Berteun Damman. Counterexample Generation in Probabilistic Model Checking, IEEE transactions on software engineering 35 (2), pages 241-257, IEEE, 2009.
2008
[bibtex]
@techreport{SS2008,
title = {SMA - the Smyle modeling approach},
author = {Benedikt Bollig and Joost-Pieter Katoen and Carsten Kern and Martin Leucker},
publisher = {TU},
pages = {26 S.},
type = {Tech Report},
year = {2008},
url = { https://publications.rwth-aachen.de/record/47820},
}×
[issue]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. SMA - the Smyle modeling approach, 26 S., TU, 2008.
fulltext PDF [bibtex]
@techreport{AE2008,
title = {Abstraction for stochastic systems by Erlangs method of stages},
author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf},
publisher = {RWTH Aachen, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2008,12},
pages = {27 S.},
type = {Tech Report},
year = {2008},
url = { https://publications.rwth-aachen.de/record/47821},
}×
[issue]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Abstraction for stochastic systems by Erlangs method of stages, Volume 2008,12 of Aachener Informatik-Berichte, 27 S., RWTH Aachen, Department of Computer Science, 2008.
fulltext PDF [bibtex]
@inbook{RM2008,
title = {Reachability in continuous-time Markov reward decision processes},
author = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Amsterdam Univ. Pr.},
booktitle = {Texts in logic and games},
volume = {2},
pages = {53-72},
type = {Book Chapter},
year = {2008},
url = { https://publications.rwth-aachen.de/record/83793},
}×
[issue]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Reachability in continuous-time Markov reward decision processes, Volume 2 of Texts in logic and games, 53-72, Amsterdam Univ. Pr., 2008.
DOI [bibtex]
@conference{STSDMSL2008,
title = {Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning},
author = {Benedikt Bollig and Carsten Kern and Joost-Pieter Katoen and Martin Leucker},
publisher = {Springer},
booktitle = {LNCS},
volume = {5201},
pages = {162-166},
type = {Conference Paper},
year = {2008},
doi = {10.1007/978-3-540-85361-9_15},
url = { https://publications.rwth-aachen.de/record/83794},
}×
[issue]
Benedikt Bollig, Carsten Kern, Joost-Pieter Katoen, Martin Leucker. Smyle: a Tool for Synthesizing Distributed Models from Scenarios by Learning, CONCUR 2008 - concurrency theory : 19. international conference (CONCUR 2008), Volume 5201 of LNCS, 162-166, Springer, 2008.
DOI [bibtex]
@inbook{CMMTMC2008,
title = {Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains},
author = {Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {Springer},
booktitle = {LNCS},
volume = {4981},
pages = {244-258},
type = {Book Chapter},
year = {2008},
doi = {10.1007/978-3-540-78929-1_18},
url = { https://publications.rwth-aachen.de/record/83795},
}×
[issue]
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Compositional Modeling and Minimization of Time-inhomogeneous Markov Chains, Volume 4981 of LNCS, 244-258, Springer, 2008.
DOI [bibtex]
@inbook{HFFIYPMCAEPC2008,
title = {How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison},
author = {David N. Jansen and Joost-Pieter Katoen and Marcel Oldenkamp and Marielle Stoelinga and Ivan S. Zapreev},
publisher = {Springer},
booktitle = {LNCS},
volume = {4899},
pages = {69-85},
type = {Book Chapter},
year = {2008},
doi = {10.1007/978-3-540-77966-7_9},
url = { https://publications.rwth-aachen.de/record/83796},
}×
[issue]
David N. Jansen, Joost-Pieter Katoen, Marcel Oldenkamp, Marielle Stoelinga, Ivan S. Zapreev. How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison, Volume 4899 of LNCS, 69-85, Springer, 2008.
DOI [bibtex]
@conference{ASSEMS2008,
title = {Abstraction for Stochastic Systems by Erlang's Method of Stages},
author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf},
publisher = {Springer},
booktitle = {LNCS},
volume = {5201},
pages = {279-294},
type = {Conference Paper},
year = {2008},
doi = {10.1007/978-3-540-85361-9_24},
url = { https://publications.rwth-aachen.de/record/83797},
}×
[issue]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Abstraction for Stochastic Systems by Erlang's Method of Stages, CONCUR 2008 - concurrency theory : 19. international conference (CONCUR 2008), Volume 5201 of LNCS, 279-294, Springer, 2008.
DOI [bibtex]
@inbook{MCHOPCIMC2008,
title = {Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains},
author = {Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {Springer},
booktitle = {LNCS},
volume = {5215},
pages = {203-217},
type = {Book Chapter},
year = {2008},
doi = {10.1007/978-3-540-85778-5_15},
url = { https://publications.rwth-aachen.de/record/83798},
}×
[issue]
Joost-Pieter Katoen, Alexandru Mereacre. Model Checking HML On Piecewise-Constant Inhomogeneous Markov Chains, Volume 5215 of LNCS, 203-217, Springer, 2008.
[bibtex]
@book{P2008,
title = {Principles of model checking},
author = {Christel Baier and Joost-Pieter Katoen},
publisher = {MIT Press},
booktitle = {Computer science},
pages = {XVII, 975 S.. : graph. Darst.},
type = {Book},
year = {2008},
url = { https://publications.rwth-aachen.de/record/94602},
}×
[issue]
Christel Baier, Joost-Pieter Katoen. Principles of model checking, Computer science, XVII, 975 S.. : graph. Darst., MIT Press, 2008.
DOI [bibtex]
@conference{S2008,
title = {Symmetry reduction for stochastic hybrid systems},
author = {Manuela Bujorianu and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {233-238},
type = {Conference Paper},
year = {2008},
doi = {10.1109/CDC.2008.4739086},
url = { https://publications.rwth-aachen.de/record/100535},
}×
[issue]
Manuela Bujorianu, Joost-Pieter Katoen. Symmetry reduction for stochastic hybrid systems, 47. IEEE Conference on Decision and Control (CDC 2008), 233-238, IEEE, 2008.
DOI [bibtex]
@conference{TABPTA2008,
title = {Time-Abstracting Bisimulation for Probabilistic Timed Automata},
author = {Taolue Chen and Tingting Han and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {177-184},
type = {Conference Paper},
year = {2008},
doi = {10.1109/TASE.2008.29},
url = { https://publications.rwth-aachen.de/record/100536},
}×
[issue]
Taolue Chen, Tingting Han, Joost-Pieter Katoen. Time-Abstracting Bisimulation for Probabilistic Timed Automata, 2.IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 177-184, IEEE, 2008.
DOI [bibtex]
@conference{REPC2008,
title = {Regular Expressions for PCTL Counterexamples},
author = {Berteun Damman and Tingting Han and Joost-Pieter Katoen},
publisher = {IEEE},
pages = {179-188},
type = {Conference Paper},
year = {2008},
doi = {10.1109/QEST.2008.11},
url = { https://publications.rwth-aachen.de/record/100537},
}×
[issue]
Berteun Damman, Tingting Han, Joost-Pieter Katoen. Regular Expressions for PCTL Counterexamples, 5. edition of the International Conference on Quantitative Evaluation of Systems (QUEST 2008), 179-188, IEEE, 2008.
DOI [bibtex]
@conference{A2008,
title = {Approximate parameter synthesis for probabilistic time-bounded reachability},
author = {Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {IEEE},
pages = {173-182},
type = {Conference Paper},
year = {2008},
doi = {10.1109/RTSS.2008.19},
url = { https://publications.rwth-aachen.de/record/100538},
}×
[issue]
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Approximate parameter synthesis for probabilistic time-bounded reachability, 2008 Real-Time Systems Symposium (RTSS 2008), 173-182, IEEE, 2008.
DOI [bibtex]
@conference{H2008,
title = {How to model and analyze gossiping protocols?},
author = {Joost-Pieter Katoen},
publisher = {ACM},
pages = {3-6},
type = {Conference Paper},
year = {2008},
doi = {10.1145/1481506.1481509},
url = { https://publications.rwth-aachen.de/record/100539},
}×
[issue]
Joost-Pieter Katoen. How to model and analyze gossiping protocols?, 2008 International Conference on Measurement & Modeling of Computer Systems (SIGMETRIC 2008), 3-6, ACM, 2008.
DOI [bibtex]
@conference{PPV2008,
title = {Perspectives in Probabilistic Verification},
author = {Joost-Pieter Katoen},
publisher = {IEEE},
pages = {3-10},
type = {Conference Paper},
year = {2008},
doi = {10.1109/TASE.2008.44},
url = { https://publications.rwth-aachen.de/record/100540},
}×
[issue]
Joost-Pieter Katoen. Perspectives in Probabilistic Verification, 2.IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering, 3-10, IEEE, 2008.
DOI [bibtex]
@conference{QEESDTMAT2008,
title = {Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques},
author = {Joost-Pieter Katoen},
publisher = {IEEE Service Center},
booktitle = {Design Automation and Test in Europe Conference and Expo},
pages = {86-87},
type = {Conference Paper},
year = {2008},
doi = {10.1109/DATE.2008.4484665},
url = { https://publications.rwth-aachen.de/record/100541},
}×
[issue]
Joost-Pieter Katoen. Quantitative Evaluation in Embedded System Design: Trends in Modeling and Analysis Techniques, Design, automation and test in Europe (DATE 2008), Design Automation and Test in Europe Conference and Expo, 86-87, IEEE Service Center, 2008.
DOI [bibtex]
@conference{TSRCTACD2008,
title = {The Surprising Robustness of (Closed) Timed Automata against Clock-Drift},
author = {Mani Swaminathan and Martin Fränzle and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {IFIP},
volume = {273},
pages = {537-553},
type = {Conference Paper},
year = {2008},
doi = {10.1007/978-0-387-09680-3_36},
url = { https://publications.rwth-aachen.de/record/100542},
}×
[issue]
Mani Swaminathan, Martin Fränzle, Joost-Pieter Katoen. The Surprising Robustness of (Closed) Timed Automata against Clock-Drift, 5.IFIP International Conference on Theoretical Computer Science (TCS 2008), Volume 273 of IFIP, 537-553, Springer, 2008.
2007
fulltext PDF [bibtex]
@techreport{BM2007,
title = {Bisimulation and logical preservation for continuous-time Markov decision processes},
author = {Martin R. Neuhäußer and Joost-Pieter Katoen},
publisher = {RWTH, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2007,10},
pages = {26 S.},
type = {Tech Report},
year = {2007},
url = { https://publications.rwth-aachen.de/record/47948},
}×
[issue]
Martin R. Neuhäußer, Joost-Pieter Katoen. Bisimulation and logical preservation for continuous-time Markov decision processes, Volume 2007,10 of Aachener Informatik-Berichte, 26 S., RWTH, Department of Computer Science, 2007.
fulltext PDF [bibtex]
@techreport{T2007,
title = {Three-valued abstraction for probabilistic systems},
author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf},
publisher = {RWTH Aachen, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2007,20},
pages = {49 Bl. : graph. Darst.},
type = {Tech Report},
year = {2007},
url = { https://publications.rwth-aachen.de/record/47949},
}×
[issue]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Three-valued abstraction for probabilistic systems, Volume 2007,20 of Aachener Informatik-Berichte, 49 Bl. : graph. Darst., RWTH Aachen, Department of Computer Science, 2007.
fulltext PDF [bibtex]
@techreport{CM2007,
title = {Compositional modeling and minimization of time-inhomogeneous Markov chains},
author = {Tingting Han and Joost-Pieter Katoen and Alexandru Mereacre},
publisher = {RWTH, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2007,21},
pages = {39 Bl. : graph. Darst.},
type = {Tech Report},
year = {2007},
url = { https://publications.rwth-aachen.de/record/47950},
}×
[issue]
Tingting Han, Joost-Pieter Katoen, Alexandru Mereacre. Compositional modeling and minimization of time-inhomogeneous Markov chains, Volume 2007,21 of Aachener Informatik-Berichte, 39 Bl. : graph. Darst., RWTH, Department of Computer Science, 2007.
[bibtex]
@inbook{S2007,
title = {Stochastic model checking},
author = {Joost-Pieter Katoen},
publisher = {CRC, Taylor & Francis},
booktitle = {Automation and control engineering},
volume = {24},
type = {Book Chapter},
year = {2007},
url = { https://publications.rwth-aachen.de/record/88200},
}×
[issue]
Joost-Pieter Katoen. Stochastic model checking, Volume 24 of Automation and control engineering, CRC, Taylor & Francis, 2007.
DOI [bibtex]
@conference{MM2007,
title = {Motor: the MoDeST tool environment},
author = {Henrik Bohnenkamp and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4424},
pages = {500-504},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-71209-1_38},
url = { https://publications.rwth-aachen.de/record/88934},
}×
[issue]
Henrik Bohnenkamp, Holger Hermanns, Joost-Pieter Katoen. Motor: the MoDeST tool environment, 13. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Volume 4424 of LNCS, 500-504, Springer, 2007.
DOI [bibtex]
@conference{BM2007,
title = {Bisimulation and logical preservation for continuous-time Markov decision processes},
author = {Martin R. Neuhäußer and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4703},
pages = {412-427},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-74407-8_28},
url = { https://publications.rwth-aachen.de/record/89821},
}×
[issue]
Martin R. Neuhäußer, Joost-Pieter Katoen. Bisimulation and logical preservation for continuous-time Markov decision processes, Concurrency theory : 18. international conference (CONCUR 2007), Volume 4703 of LNCS, 412-427, Springer, 2007.
DOI [bibtex]
@conference{TVACTMC2007,
title = {Three-Valued Abstraction for Continuous-Time Markov Chains},
author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf},
publisher = {Springer},
booktitle = {LNCS},
volume = {4590},
pages = {311-324},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-73368-3_37},
url = { https://publications.rwth-aachen.de/record/89823},
}×
[issue]
Joost-Pieter Katoen, Daniel Klink, Martin Leucker, Verena Wolf. Three-Valued Abstraction for Continuous-Time Markov Chains, Computer aided verification : 19. international conference (CAV 2007), Volume 4590 of LNCS, 311-324, Springer, 2007.
DOI [bibtex]
@conference{PC2007,
title = {Providing evidence of likely being on time: counterexample generation for CTMC model checking},
author = {Tingting Han and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4762},
pages = {331-346},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-75596-8_24},
url = { https://publications.rwth-aachen.de/record/89824},
}×
[issue]
Tingting Han, Joost-Pieter Katoen. Providing evidence of likely being on time: counterexample generation for CTMC model checking, 5. International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), Volume 4762 of LNCS, 331-346, Springer, 2007.
DOI [bibtex]
@conference{A2007,
title = {Abstraction of probabilistic systems},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4763},
pages = {1-3},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-75454-1_1},
url = { https://publications.rwth-aachen.de/record/89826},
}×
[issue]
Joost-Pieter Katoen. Abstraction of probabilistic systems, 5. International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2007), Volume 4763 of LNCS, 1-3, Springer, 2007.
DOI [bibtex]
@conference{C2007,
title = {Counterexamples in probabilistic model checking},
author = {Tingting Han and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4424},
pages = {72-86},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-71209-1_8},
url = { https://publications.rwth-aachen.de/record/89827},
}×
[issue]
Tingting Han, Joost-Pieter Katoen. Counterexamples in probabilistic model checking, 13. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Volume 4424 of LNCS, 72-86, Springer, 2007.
DOI [bibtex]
@conference{R2007,
title = {Replaying play in and play out: synthesis of design models from scenarios by learning},
author = {Benedikt Bollig and Joost-Pieter Katoen and Carsten Kern and Martin Leucker},
publisher = {Springer},
booktitle = {LNCS},
volume = {4424},
pages = {435-450},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-71209-1_33},
url = { https://publications.rwth-aachen.de/record/89828},
}×
[issue]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. Replaying play in and play out: synthesis of design models from scenarios by learning, 13. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Volume 4424 of LNCS, 435-450, Springer, 2007.
fulltext PDF [bibtex]
@techreport{VL2007,
title = {Verifying concurrent list-manipulating programs by LTL model checking},
author = {Joost-Pieter Katoen and Thomas Noll and Stefan Rieger},
publisher = {RWTH, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2007,6},
pages = {26 Bl. : graph. Darst.},
type = {Tech Report},
year = {2007},
url = { https://publications.rwth-aachen.de/record/96680},
}×
[issue]
Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying concurrent list-manipulating programs by LTL model checking, Volume 2007,6 of Aachener Informatik-Berichte, 26 Bl. : graph. Darst., RWTH, Department of Computer Science, 2007.
fulltext PDF [bibtex]
@conference{VL2007,
title = {Verifying concurrent list-manipulating programs by LTL model checking},
author = {Joost-Pieter Katoen and Thomas Noll and Stefan Rieger},
pages = {94-113},
type = {Conference Paper},
year = {2007},
url = { https://publications.rwth-aachen.de/record/115549},
}×
[issue]
Joost-Pieter Katoen, Thomas Noll, Stefan Rieger. Verifying concurrent list-manipulating programs by LTL model checking, Workshop on Heap Analysis and Verification (HAV 2007), 94-113, 2007.
DOI [bibtex]
@conference{B2007,
title = {Bisimulation minimisation mostly speeds up probabilistic model checking},
author = {Joost-Pieter Katoen and Tim Kemna and Ivan S. Zapreev and David N. Jansen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4424},
pages = {87-101},
type = {Conference Paper},
year = {2007},
doi = {10.1007/978-3-540-71209-1_9},
url = { https://publications.rwth-aachen.de/record/117989},
}×
[issue]
Joost-Pieter Katoen, Tim Kemna, Ivan S. Zapreev, David N. Jansen. Bisimulation minimisation mostly speeds up probabilistic model checking, Tools and algorithms for the construction and analysis of systems (TACAS 2007), Volume 4424 of LNCS, 87-101, Springer, 2007.
DOI [bibtex]
@article{M2007,
title = {Model checking mobile stochastic logic},
author = {Rocco de Nicola and Joost-Pieter Katoen and Diego Latella and Michele Loreti and Mieke Massink},
publisher = {Elsevier},
journal = {Theoretical computer science},
volume = {382.2007(1)},
pages = {pages 42-70},
type = {Journal Article},
year = {2007},
doi = {10.1016/j.tcs.2007.05.008},
url = { https://publications.rwth-aachen.de/record/158135},
}×
[issue]
Rocco de Nicola, Joost-Pieter Katoen, Diego Latella, Michele Loreti, Mieke Massink. Model checking mobile stochastic logic, Theoretical computer science 382.2007 (1), pages 42-70, Elsevier, 2007.
2006
[bibtex]
@techreport{R2006,
title = {Replaying play in and play out: synthesis of design models from scenarios by learning},
author = {Benedikt Bollig and Joost-Pieter Katoen and Carsten Kern and Martin Leucker},
booktitle = {Aachener Informatik-Berichte},
volume = {2006,12},
pages = {26 Bl. : graph. Darst.},
type = {Tech Report},
year = {2006},
url = { https://publications.rwth-aachen.de/record/47925},
}×
[issue]
Benedikt Bollig, Joost-Pieter Katoen, Carsten Kern, Martin Leucker. Replaying play in and play out: synthesis of design models from scenarios by learning, Volume 2006,12 of Aachener Informatik-Berichte, 26 Bl. : graph. Darst., 2006.
fulltext PDF [bibtex]
@techreport{C2006,
title = {Counterexamples in probabilistic model checking},
author = {Tingting Han and Joost-Pieter Katoen},
publisher = {RWTH, Department of Computer Science},
booktitle = {Aachener Informatik-Berichte},
volume = {2006,9},
pages = {35 Bl. : graph. Darst.},
type = {Tech Report},
year = {2006},
url = { https://publications.rwth-aachen.de/record/47927},
}×
[issue]
Tingting Han, Joost-Pieter Katoen. Counterexamples in probabilistic model checking, Volume 2006,9 of Aachener Informatik-Berichte, 35 Bl. : graph. Darst., RWTH, Department of Computer Science, 2006.
DOI [bibtex]
@inbook{S2006,
title = {Safety and liveness in concurrent pointer programs},
author = {Dino Distefano and Joost-Pieter Katoen and Arend Rensink},
publisher = {Springer},
booktitle = {LNCS},
volume = {4111},
pages = {280-312},
type = {Book Chapter},
year = {2006},
doi = {10.1007/11804192_14},
url = { https://publications.rwth-aachen.de/record/88260},
}×
[issue]
Dino Distefano, Joost-Pieter Katoen, Arend Rensink. Safety and liveness in concurrent pointer programs, Volume 4111 of LNCS, 280-312, Springer, 2006.
DOI [bibtex]
@article{M2006,
title = {MoDeST: a compositional modeling formalism for real-time and stochastic systems},
author = {Henrik Bohnenkamp and Pedro R. D'Argenio and Holger Hermanns and Joost-Pieter Katoen},
publisher = {IEEE},
journal = {IEEE transactions on software engineering},
volume = {32(10)},
pages = {pages 812-830},
type = {Journal Article},
year = {2006},
doi = {10.1109/TSE.2006.104},
url = { https://publications.rwth-aachen.de/record/152843},
}×
[issue]
Henrik Bohnenkamp, Pedro R. D'Argenio, Holger Hermanns, Joost-Pieter Katoen. MoDeST: a compositional modeling formalism for real-time and stochastic systems, IEEE transactions on software engineering 32 (10), pages 812-830, IEEE, 2006.
DOI [bibtex]
@article{YM2006,
title = {YMCA: why Markov chain algebra?},
author = {Mario Bravetti and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Electronic notes in theoretical computer science},
volume = {162},
pages = {pages 107-112},
type = {Journal Article},
year = {2006},
doi = {10.1016/j.entcs.2005.12.108},
url = { https://publications.rwth-aachen.de/record/152846},
}×
[issue]
Mario Bravetti, Holger Hermanns, Joost-Pieter Katoen. YMCA: why Markov chain algebra?, Electronic notes in theoretical computer science 162, pages 107-112, Elsevier, 2006.
DOI [bibtex]
@article{T2006,
title = {Towards a logic for performance and mobility},
author = {Rocco de Nicola and Joost-Pieter Katoen and Diego Latella and Mieke Massink},
publisher = {Elsevier},
journal = {Electronic notes in theoretical computer science},
volume = {153(2)},
pages = {pages 161-175},
type = {Journal Article},
year = {2006},
doi = {10.1016/j.entcs.2005.10.037},
url = { https://publications.rwth-aachen.de/record/152847},
}×
[issue]
Rocco de Nicola, Joost-Pieter Katoen, Diego Latella, Mieke Massink. Towards a logic for performance and mobility, Electronic notes in theoretical computer science 153 (2), pages 161-175, Elsevier, 2006.
DOI [bibtex]
@conference{S2006,
title = {Safe on-the-fly steady-state detection for time-bounded reachability},
author = {Joost-Pieter Katoen and Ivan S. Zapreev},
publisher = {IEEE Computer Society},
pages = {301-310},
type = {Conference Paper},
year = {2006},
doi = {10.1109/QEST.2006.47},
url = { https://publications.rwth-aachen.de/record/153112},
}×
[issue]
Joost-Pieter Katoen, Ivan S. Zapreev. Safe on-the-fly steady-state detection for time-bounded reachability, 3.International Conference on the Quantitative Evaluation of Systems (QEST 2006), 301-310, IEEE Computer Society, 2006.
DOI [bibtex]
@conference{P2006,
title = {Probably on time and within budget: on reachability in priced probabilistic timed automata},
author = {Jasper Berendsen and David N. Jansen and Joost-Pieter Katoen},
publisher = {IEEE Computer Society},
pages = {311-320},
type = {Conference Paper},
year = {2006},
doi = {10.1109/QEST.2006.43},
url = { https://publications.rwth-aachen.de/record/153113},
}×
[issue]
Jasper Berendsen, David N. Jansen, Joost-Pieter Katoen. Probably on time and within budget: on reachability in priced probabilistic timed automata, 3.International Conference on the Quantitative Evaluation of Systems (QEST 2006), 311-320, IEEE Computer Society, 2006.
DOI [bibtex]
@article{GICQESQ2006,
title = {Guest editors introduction to the special section on the first International Conference on the Quantitative Evaluation of SysTems (QEST)},
author = {Giuliana Franceschinis and Joost-Pieter Katoen and Murray Woodside},
publisher = {IEEE},
journal = {IEEE transactions on software engineering},
volume = {32(8)},
pages = {pages 529-530},
type = {Journal Article},
year = {2006},
doi = {10.1109/TSE.2006.80},
url = { https://publications.rwth-aachen.de/record/187818},
}×
[issue]
Giuliana Franceschinis, Joost-Pieter Katoen, Murray Woodside. Guest editors introduction to the special section on the first International Conference on the Quantitative Evaluation of SysTems (QEST), IEEE transactions on software engineering 32 (8), pages 529-530, IEEE, 2006.
2005
DOI [bibtex]
@book{M2005,
title = {Model-based testing of reactive systems},
author = {},
editor = {Manfred Broy and Bengt Jonsson and Joost-Pieter Katoen and Martin Leucker and Alexander Pretschner},
publisher = {Springer},
booktitle = {LNCS},
volume = {3472},
pages = {VIII, 659 S.. : graph. Darst.},
type = {Book},
year = {2005},
doi = {10.1007/b137241},
url = { https://publications.rwth-aachen.de/record/49521},
}×
[issue]
Manfred Broy (ed), Bengt Jonsson (ed), Joost-Pieter Katoen (ed), Martin Leucker (ed), Alexander Pretschner (ed). Model-based testing of reactive systems, Volume 3472 of LNCS, VIII, 659 S.. : graph. Darst., Springer, 2005.
DOI [bibtex]
@conference{A2005,
title = {Are you still there?: a lightweight algorithm to monitor node presence in self-configuring networks},
author = {Henrik Bohnenkamp and Johan Gorter and Jarno Guidi and Joost-Pieter Katoen},
publisher = {IEEE Computer Society},
pages = {704-709},
type = {Conference Paper},
year = {2005},
doi = {10.1109/DSN.2005.20},
url = { https://publications.rwth-aachen.de/record/112195},
}×
[issue]
Henrik Bohnenkamp, Johan Gorter, Jarno Guidi, Joost-Pieter Katoen. Are you still there?: a lightweight algorithm to monitor node presence in self-configuring networks, International Conference on Dependable Systems and Networks, 704-709, IEEE Computer Society, 2005.
DOI [bibtex]
@conference{AM2005,
title = {A Markov reward model checker},
author = {Joost-Pieter Katoen and Maneesh Khattri and Ivan S. Zapreev},
publisher = {IEEE Computer Society},
pages = {243-244},
type = {Conference Paper},
year = {2005},
doi = {10.1109/QEST.2005.2},
url = { https://publications.rwth-aachen.de/record/113338},
}×
[issue]
Joost-Pieter Katoen, Maneesh Khattri, Ivan S. Zapreev. A Markov reward model checker, 2. International Conference on the Quantitative Evaluation of Systems, 243-244, IEEE Computer Society, 2005.
DOI [bibtex]
@conference{MM2005,
title = {Model checking Markov reward models with impulse rewards},
author = {Lucia Cloth and Joost-Pieter Katoen and Maneesh Khattri and Reza Pulungan},
publisher = {IEEE Computer Society},
pages = {722-731},
type = {Conference Paper},
year = {2005},
doi = {10.1109/DSN.2005.64},
url = { https://publications.rwth-aachen.de/record/114531},
}×
[issue]
Lucia Cloth, Joost-Pieter Katoen, Maneesh Khattri, Reza Pulungan. Model checking Markov reward models with impulse rewards, 2005 International Conference on Dependable Systems and Networks, 722-731, IEEE Computer Society, 2005.
DOI [bibtex]
@article{APIS2005,
title = {A theory of stochastic systems. Part I: Stochastic automata},
author = {Pedro R. D'Argenio and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Information and computation},
volume = {203(1)},
pages = {pages 1-38},
type = {Journal Article},
year = {2005},
doi = {10.1016/j.ic.2005.07.001},
url = { https://publications.rwth-aachen.de/record/156179},
}×
[issue]
Pedro R. D'Argenio, Joost-Pieter Katoen. A theory of stochastic systems. Part I: Stochastic automata, Information and computation 203 (1), pages 1-38, Elsevier, 2005.
DOI [bibtex]
@article{CM2005,
title = {Comparative branching-time semantics for Markov chains},
author = {Christel Baier and Joost-Pieter Katoen and Holger Hermanns and Verena Wolf},
publisher = {Elsevier},
journal = {Information and computation},
volume = {200(2)},
pages = {pages 149-214},
type = {Journal Article},
year = {2005},
doi = {10.1016/j.ic.2005.03.001},
url = { https://publications.rwth-aachen.de/record/156685},
}×
[issue]
Christel Baier, Joost-Pieter Katoen, Holger Hermanns, Verena Wolf. Comparative branching-time semantics for Markov chains, Information and computation 200 (2), pages 149-214, Elsevier, 2005.
DOI [bibtex]
@article{APIP2005,
title = {A theory of stochastic systems. Part II: Process algebra},
author = {Pedro R. D'Argenio and Joost-Pieter Katoen},
publisher = {Elsevier},
journal = {Information and computation},
volume = {200(1)},
pages = {pages 39-74},
type = {Journal Article},
year = {2005},
doi = {10.1016/j.ic.2005.07.002},
url = { https://publications.rwth-aachen.de/record/157058},
}×
[issue]
Pedro R. D'Argenio, Joost-Pieter Katoen. A theory of stochastic systems. Part II: Process algebra, Information and computation 200 (1), pages 39-74, Elsevier, 2005.
DOI [bibtex]
@article{M2005,
title = {Model checking meets performance evaluation},
author = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Association for Computing Machinery},
journal = {Performance evaluation review},
volume = {32(4)},
pages = {pages 10-15},
type = {Journal Article},
year = {2005},
doi = {10.1145/1059816.1059819},
url = { https://publications.rwth-aachen.de/record/157918},
}×
[issue]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Model checking meets performance evaluation, Performance evaluation review 32 (4), pages 10-15, Association for Computing Machinery, 2005.
2002
DOI [bibtex]
@conference{M2002,
title = {Model checking performability properties},
author = {Boudewijn R. Haverkort and Lucia Cloth and Holger Hermanns and Joost-Pieter Katoen and Christel Baier},
publisher = {IEEE Computer Society},
pages = {103-112},
type = {Conference Paper},
year = {2002},
doi = {10.1109/DSN.2002.1028891},
url = { https://publications.rwth-aachen.de/record/117614},
}×
[issue]
Boudewijn R. Haverkort, Lucia Cloth, Holger Hermanns, Joost-Pieter Katoen, Christel Baier. Model checking performability properties, International Conference on Dependable Systems and Networks, 103-112, IEEE Computer Society, 2002.
DOI [bibtex]
@conference{A2002,
title = {Automated performance and dependability evaluation using model checking},
author = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {2459},
pages = {261-289},
type = {Conference Paper},
year = {2002},
doi = {10.1007/3-540-45798-4_12},
url = { https://publications.rwth-aachen.de/record/117723},
}×
[issue]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. Automated performance and dependability evaluation using model checking, IFIP WG 7.3 International Symposium on Computer Modeling, Measurement and Evaluation, Volume 2459 of LNCS, 261-289, Springer, 2002.
2000
DOI [bibtex]
@conference{OLCPP2000,
title = {On the Logical Characterisation of Performability Properties},
author = {Christel Baier and Boudewijn R. Haverkort and Holger Hermanns and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {1853},
pages = {780-792},
type = {Conference Paper},
year = {2000},
doi = {10.1007/3-540-45022-X_65},
url = { https://publications.rwth-aachen.de/record/198220},
}×
[issue]
Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. On the Logical Characterisation of Performability Properties, 27. international colloquium (ICALP 2000), Volume 1853 of LNCS, 780-792, Springer, 2000.