September 29, 2023
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 for them, and reports on experimental results.
September 28, 2023
MOVES has successfully organised the 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung (KPS 2023). KPS is a traditional, bi-annual series of workshops for computer scientists from Germany, Austria and Switzerland working on the foundations, design, implementation, and usage of programming languages. This year’s edition featured 41 participants and a scientific programme with 31 presentations.
September 27, 2023
The paper entitled “Provably Bounding Neural Network Preimages” by Christopher Brix, Suhas Kotha (CMU), Huan Zhang (UIUC), Zico Kolter (CMU), Krishnamurthy (Dj) Dvijotham (Google DeepMind) has been accepted for publication in the thirty-seventh Conference on Neural Information Processing Systems. The paper presents a way to compute bounds on the preimage of the output of a neural network by transforming the problem such that it can be optimized by state-of-the-art tools for the forward…
Read more about Paper in NeurIPSAugust 31, 2023
Our group has to offer two PhD positions in Interdisciplinary Doctoral Program in Quantum Systems Integration at RWTH Aachen University. The first is about formal methods for supporting the development of zero-defect quantum programs, while the second aims to provide a systematic framework for compiling quantum software to computing architectures featuring qubit shuttling. For details, please refer to the respective job posting.
July 30, 2023
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 parametric BNs. The approach improves upon the state of the art by—most importantly—being able to handle an unbounded number…
Read more about Paper in JAIRJuly 3, 2023
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 probabilistic analogue of Boogie: its central components are an intermediate…
Read more about Paper at OOPSLA 2023June 19, 2023
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 chains and Markov decision processes. We focus on three problems: (a) do all…
Read more about Paper in FMSD JournalMay 25, 2023
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 dependability measures for continuous-time Markov chain models. More information can be found here.…
Read more about Jean-Claude Laprie AwardMay 3, 2023
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 software tool equipped with a professional GUI for the modelling and analysis of static and dynamic fault trees. Under the…
Read more about Paper at ESREL 2023April 26, 2023
The paper entitled “Search and Explore: Symbiotic Policy Synthesis in POMDPs” by Roman Andriushchenko (Brno University of Technology), Alexander Bork, Milan Ceska (Brno), Sebastian Junges (Radboud University, Netherlands), Joost-Pieter Katoen and Filip Macak (Brno) has been accepted for presentation at the 33th Conference on Computer-Aided Verification in Paris. The paper presents a symbiotic anytime algorithm that tightly integrates a belief-based and an inductive approach for finite-state…
Read more about Paper at CAV 2023April 19, 2023
The paper entitled “Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks” by Bahare Salmani and Joost-Pieter Katoen has been accepted for presentation at IJCAI 2023 (the 32nd Int. Joint Conf. on Artificial Intelligence) in Macao. Out of 4566 full-paper submissions, about 15% has been accepted. The paper gives an algorithm for estimating the sensitivity of a given fully-specified Bayesian network to small perturbations in the values of local conditional probabilities.
April 5, 2023
The paper entitled “On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata” by Tobias Winkler and Joost-Pieter Katoen has been accepted for presentation at the IEEE/ACM Annual Symposium on Logic on Computer Science 2023 to be held in Boston. The paper studies certification of numerical characteristics of probabilistic pushdown systems, that is, how one can witness that the termination probability (or expected running time) is above/below a certain threshold.
March 21, 2023
The paper entitled “A Compositional Semantics of Boolean-logic Driven Markov Processes” by Shahid Khan, Joost-Pieter Katoen andMarc Bouissou (EDF) has been accepted as regular paper for IEEE Transactions on Dependable and Secure Computing. This paper provides a compositional and operational semantics (using Markov automata) of BDMPs, a prominent dynamic extension of static fault trees to model repairable and complex dynamic systems.
March 1, 2023
The proceedings of the 25th Symposium on Formal Methods (FM 2023), edited by Marsha Chechik (Toronto), Joost-Pieter Katoen and Martin Leucker (Lübeck), and published as LNCS volume 14000, are available from March 2 and accessible under: https://link.springer.com/book/10.1007/978-3-031-27481-7.
February 28, 2023
The project proposal “Probabilistic Model Checking under Partial Observability with Multiple Objectives” (POMPOM) has been granted for funding by the German Research Council. The project aims to develop new model-checking algorithms for combinations of qualitative, stochastic and total expected reward objectives for partially observable Markov decision processes (and games). The funding is for two years and Raphael Berthon, a former PhD student of Jean-Francois Raskin and Guillermo Perez, will…
Read more about DFG Project Proposal Granted