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.

We presented our results on benchmarking software model-checkers on automotive code at the virtual NFM2020 symposium. Check out the video at https://youtu.be/XLzIXVNCIuk?t=19941 !

We are happy to inform you that Joost-Pieter Katoen has been appointed Chair of the TACAS Steering Committee. TACAS is one of the flagship conferences on formal analysis techniques and tools for computer systems. He takes over this role from Bernhard Steffen (TU Dortmund) who has been SC chair since the foundation of TACAS in […]

The paper “Synthesizing and Optimizing FDIR Recovery Strategies From Fault Trees“ by Sascha Müller, Liana Mikaelyan, Andreas Gerndt (DLR German Aerospace Center, Braunschweig) and Thomas Noll has been accepted for publication by the Science of Computer Programming Journal. It investigates the synthesis of efficient recovery strategies for Failure Detection, Isolation and Recovery (FDIR) for space […]