Tim Quatmann has been awarded a KI-Starter Grant for his project proposal “Verifying AI Systems under Partial Observability“. The KI-Starter Grant is an initiative of the State North-Rhine Westphalia to strengthen its position in AI and in particular stimulates young researchers in their academic career. Tim’s project focuses on the automated verification using model checking […]

The paper entitled “Programmatic Strategy Synthesis: Resolving Nondeterminism in  Probabilistic Programs” by Kevin Batz, Tom Biskup, Joost-Pieter Katoen, and Tobias Winkler has been accepted at the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024). The paper shows how to use deductive verification to resolve pure nondeterminism in probabilistic programs such that the obtained determinized program […]

The paper entitled “Model Checking Temporal Properties of Recursive Probabilistic Programs” by Tobias Winkler, Christina Gehnen and Joost-Pieter Katoen has been accepted for the special issues devoted to FoSSaCS 2022 in the journal Logical Methods in Computer Science. The paper shows that model checking a probabilistic pushdown automata against omega visibly push-down languages (e.g., expressed […]

The paper “A Deductive Verification Infrastructure for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja received a distinguished artifact award at OOPSLA 2023. The artifact consists of the deductive verifier Caesar together with a couple of benchmark examples. Caesar has a website at www.caesarverifier.org where the tool can be […]

The paper entitled “Parameter Synthesis for Markov Models” by Sebastian Junges, Erika Abraham, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk has been accepted for publication in the journal Formal Methods in System Design. The paper gives a comprehensive overview of several synthesis problems on parametric Markov chains and MDPs, presents algorithms […]

The paper entitled “Automatically Finding the Right Probabilities in Bayesian Networks” by Bahare Salmani and Joost-Pieter Katoen has been accepted for publication in the Journal of Artificial Intelligence Research. The paper presents a way to use probabilistic model checking to perform inference on Bayesian networks (BNs) and find suitable parameter values in the case of […]

The paper entitled “A Deductive Verification Infrastructure for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski (Saarland University and UCL), Joost-Pieter Katoen and Christoph Matheja (TU Denmark) has been accepted for publication at OOPSLA 2023. The paper presents a quantitative program verification infrastructure for discrete probabilistic programs. This infrastructure can be viewed as the […]

The paper “Parameter Synthesis for Markov Models: Covering the Parameter Space” by Sebastian Junges (Nijmegen), Erika Abraham, Christian Hensel (Amazon), Nils Jansen (Nijmegen), Joost-Pieter Katoen, Tim Quatmann and Matthias Volk (Twente) has been accepted for publication in the journal Formal Methods in Systems Design. The paper (85 pages) presents various analysis algorithms for parametric discrete-time Marko […]

The Jean-Claude Laprie Award 2023 in Dependable Computing has been awarded to the paper “Model-checking algorithms for continuous-time Markov chains”, authored by Christel Baier, Boudewijn Haverkort, Holger Hermanns, and Joost-Pieter Katoen, and published in IEEE Transactions on Software Engineering, 2003. It presents a unifying theory and algorithm to evaluate a wide variety of performance and […]

The paper entitled “SAFEST: the static and dynamic fault tree analysis tool” by Matthias Volk (Twente), Muzammil Ibne Irshad (DGB), Joost-Pieter Katoen, Falak Sher (DGB), Marielle Stoelinga (Twente) and Ahmad Zafar (DGB) has been accepted for presentation at the European Conference On Safety And Reliability (ESREL) 2023 in Southampton, UK. The paper presents a powerful […]