@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},
}×

@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)},
type = {Journal Article},
year = {2024},
doi = {10.1145/3649844},
url = { https://publications.rwth-aachen.de/record/981709},
}×

@unpublished{EPIUGF2023,
title = {Exact Probabilistic Inference Using Generating Functions},
author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen},
type = {Preprint},
year = {2023},
url = { https://publications.rwth-aachen.de/record/862300},
}×

@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},
}×

@article{S2023,
title = {Stochastic games with lexicographic objectives},
author = {Krishnendu Chatterjee and Joost-Pieter Katoen and Stefanie Mohr and Maximilian Weininger and Tobias Winkler},
publisher = {Springer},
journal = {Formal methods in system design},
pages = {41 Seiten},
type = {Journal Article},
year = {2023},
doi = {10.1007/s10703-023-00411-4},
url = { https://publications.rwth-aachen.de/record/954240},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@conference{OCERTPPA2023,
title = {On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata},
author = {Tobias Winkler and Joost-Pieter Katoen},
publisher = {IEEE},
type = {Conference Paper},
year = {2023},
doi = {10.1109/LICS56636.2023.10175714},
url = { https://publications.rwth-aachen.de/record/972664},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@unpublished{TCQSL2022,
title = {Towards Concurrent Quantitative Separation Logic},
author = {Ira Justus Fesefeldt and Joost-Pieter Katoen and Thomas Noll},
pages = {[1]-62},
type = {Preprint},
year = {2022},
doi = {10.18154/RWTH-2022-08799},
url = { https://arxiv.org/abs/2207.02822},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
url = { https://arxiv.org/abs/2004.14835},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
url = { https://arxiv.org/abs/2007.06327},
}×

@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},
url = { https://arxiv.org/abs/2010.14548},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
url = { https://arxiv.org/abs/2004.13283},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
url = { https://arxiv.org/abs/1802.10467},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
url = { https://arxiv.org/abs/1702.04311},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
url = { https://arxiv.org/abs/1305.5055},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
url = { https://arxiv.org/abs/1312.3979},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@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},
}×

@inbook{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 = {Book Chapter},
year = {2007},
doi = {10.1007/978-3-540-74407-8_28},
url = { https://publications.rwth-aachen.de/record/89821},
}×

@inbook{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 = {Book Chapter},
year = {2007},
doi = {10.1007/978-3-540-73368-3_37},
url = { https://publications.rwth-aachen.de/record/89823},
}×

@inbook{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 = {Book Chapter},
year = {2007},
doi = {10.1007/978-3-540-75596-8_24},
url = { https://publications.rwth-aachen.de/record/89824},
}×

@inbook{A2007,
title = {Abstraction of probabilistic systems},
author = {Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {4763},
pages = {1-3},
type = {Book Chapter},
year = {2007},
doi = {10.1007/978-3-540-75454-1_1},
url = { https://publications.rwth-aachen.de/record/89826},
}×

@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},
}×

@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},
}×

@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},
}×