We are delighted to announce that the following papers have been accepted for ACM Principles of Programming Languages 2021:  Relatively Complete Verification of Probabilistic Programs by Kevin Batz, Benjamin Kaminski, Joost-Pieter Katoen and Christoph Matheja, and A Pre-Expectation Calculus for Probabilistic Sensitivity by Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Kaminski, Joost-Pieter Katoen and Christoph […]

Congratulations to Matthias Volk and Norman Weik who got the 3rd place in the Young Researcher Competition in the Category “Rail” for their contribution “Reliability analysis of railway station infrastructure based on dynamic fault trees” at the TRA VISIONS 2020 Conference, see https://www.travisions.eu/TRAVisions/young_researcher_results_2020/

We are looking for a motivated, enthusiastic student assistant to help us develop some features related to Bayesian Networks in the probabilistic model checker, Storm. The job description can be found here.

The paper entitled “Generating Functions for Probabilistic Programs” by Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman and Tobias Winkler has been accepted for presentation at the 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR). The paper presents a denotational semantics for probabilistic programs using generator functions, shows it relation […]

The paper entitled “Residual Nominal Automata” by Joshua Moerman and Matteo Sammartino (Royal Holloway University of London) has been accepted for the 31st International Conference on Concurrency Theory (CONCUR 2020). Out of 112 submissions, 45 papers are accepted. The paper is about formal languages over infinite alphabets. It investigates the class of languages accepted by […]

The paper entitled “Verification of indefinite-horizon POMDPs” by Alexander Bork, Sebastian Junges (UC Berkeley), Joost-Pieter Katoen and Tim Quatmann has been accepted for the 18th Int. Symp. on Automated Technology for Verification and Analysis (ATVA 2020). The key idea is to use abstractions of belief states and apply an abstraction-refinement strategy to verify unbounded reachability […]

The papers entitled “Bayesian Inference by Symbolic Model Checking” by Bahare Salmani and Joost-Pieter Katoen and “Probabilistic Model Checking of AODV” by Mojgan Kamali and Joost-Pieter Katen have been accepted at the 17th Int. Conf. on Quantitative Evaluation of Systems (QEST 2020). Out of 42 submissions to QEST 2020, 10 papers have been unconditionally accepted […]

The paper entitled “Multi-Cost Bounded Trade-off Analysis in MDP” by Arnd Hartmanns, Sebastian Junges, Joost-Pieter Katoen and Tim Quatmann has been accepted for the Journal of Automated Reasoning. The paper presents a memory-efficient algorithm for multi-objective model checking problems on Markov decision processes (MDPs) with multiple cost structures.

The paper entitled “Explaining Boolean-logic Driven Markov Processes using GSPNs” authored by Shahid Khan, Joost-Pieter Katoen and Marc Bouissou (EDF) has been accepted for the European Dependable Computing Conference (EDCC 2020). The paper presents a modular semantics of BDMPs using generalised stochastic Petri nets. Transition priorities are used to resolve possible non-deterministic error propagation.

We are looking for a talented student assistant to apply formal methods in the context of wireless networks. The job description can be found here.