The paper entitled “Stochastic Games with Lexicographic Objectives” by Krishnendu Chatterjee (IST Austria), Joost-Pieter Katoen, Stephanie Moor (TU Munich), Maximilian Weininger (Tu Munich), and Tobias Winkler has been accepted for publication in Formal Methods in System Design. This paper presents a detailed study of stochastic turn-based games (SG) with lexicographic objectives. The paper is an extended version of CAV’20 paper providing new results on lexicographic omega-regular objectives in…
Three papers of the MOVES group have been accepted for TACAS 2023! “A Practitioner’s Guide to MDP Model Checking Algorithms” by Arnd Hartmanns, Sebastian Junges, Tim Quatmann and Maximilian Weininger presents an empirical evaluation of various algorithms (different forms of value iteration, policy iteration and direct algorithms) to compute reachability probabilities in Markov decision processes. “Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants” by Kevin Batz,…
The paper entitled “First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)” by Christopher Brix, Mark Müller (ETH Zurich), Stanley Bak (Stony Brook University), Taylor T Johnson (Vanderbilt University), and Changliu Liu (Carnegie Mellon University) has been accepted for publication in the journal STTT ExPLAIn. The paper summarizes the organization and results from 2020 to 2022 of the VNN-COMP, where the performance of tools designed for the verification of…
The paper entitled “A Calculus for Amortized Expected Runtimes” by Kevin Batz, Benjamin Kaminski (Saarland/UCL), Joost-Pieter Katoen, Christoph Matheja (DTU Lyngby) and Lena Verscht has been accepted for presentation at the 50th ACM Symposium on Principles of Programming Languages (POPL). The paper presents a weakest precondition-style calculus to determine the amortized expected run-time of randomized algorithms that manipulate dynamic data structures such as trees and lists.
Philipp Schroer and Joost-Pieter Katoen receive a Research Award from WhatsApp, through its parent company, Meta Platforms, Inc. for their research proposal “A Deductive Verification Infrastructure for Probabilistic Programs”. Out of 62 research proposals that were submitted to WhatsApp Privacy Aware Program Analysis, 6 projects have been awarded. For more information, see here.
The paper entitled “Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming” by Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, and Joost-Pieter Katoen has been accepted for publication in the journal Information and Computation. The paper presents a novel condition on barrier certificates that witnesses unbounded-time safety of differential dynamical systems and provides algorithms to check these conditions. (This is an extended version of paper…
The paper entitled “The Probabilistic Termination Tool Amber” by Ezio Bartocci, Marcel Moosbrugger, Joost-Pieter Katoen and Laura Kovacs has been accepted in a special issue devoted to the Formal Methods Symposium 2021 in the journal Formal Methods in System Design. The paper describes a tool that can automatically check whether a probabilistic program (of a particular shape) is (positive) almost surely terminating, or not.
The paper entitled “Stochastic Games with Lexicographic Objectives” by Krishnendu Chatterjee (IST), Joost-Pieter Katoen, Stephanie Mohr (TUM), Maximilain Weininger (TUM) and Tobias Winkler has been accepted fior publication in special issue devoted to CAV 2020 in the journal Formal Methods in System Design. The paper considers presents a detailed study of stochastic turn-based games (SG) with lexicographic objectives and provides new results on lexicographic omega-regular objectives in Markov…
The paper entitled “Generative Datalog with Continuous Distributions” by Martin Grohe, Benjamin Kaminski, Joost-Pieter Katoen and Peter Lindner has been accepted in Journal of the ACM. The paper defines a formal semantics (based on stochastic kernels and Markov processes) of a probabilistic version of the Datalog querying language for probabilistic databases storing data with continuous distributions.
The paper entitled “Reasoning about Distributed Reconfigurable Systems” by Emma Ahrens (RWTH), Marius Bozga (Grenoble), Radu Iosif (Grenoble) and Joost-Pieter Katoen has been accepted for presentation at the ACM Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 2022) in Auckland, New Zealand. The paper presents a resource-based program logic for (local) reasoning about safety properties of distributed reconfigurable systems. This is the second paper with an…
The paper entitled “Towards Concurrent Quantitative Separation Logic” by Ira Fesefeldt, Joost-Pieter Katoen and Thomas Noll has been accepted at the 33rd International Conference on Concurrency Theory (CONCUR), to be held in Warsaw. The paper proposes a variant of Quantitative Separation Logic (QSL) for reasoning about concurrent probabilistic programs.
The paper entitled “Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining” by Th. Noll, J. Berger (both MOVES), W. Lenze, B. Kogel (both Institute of Transport Science, RWTH Aachen University), S. Schotten, Th. Büker (both quattron management consulting GmbH), and M. Fietze (German Centre for Rail Traffic Research) has been accepted for presentation at the 27th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2022) in Warsaw, Poland. It…
The paper entitled “Identification of bottlenecks in rail infrastructure” by W. Lenze, B. Kogel (both Institute of Transport Science, RWTH Aachen University), S. Schotten, Th. Büker (both quattron management consulting GmbH), Th. Noll, J. Berger (both MOVES) and M. Fietze (German Centre for Rail Traffic Research) has been accepted for presentation at the 5th International Conference on Railway Technology: Research, Development and Maintenance (RAILWAYS 2022) in Montpellier, France. It presents…
The paper entitled “POMDP Controllers With Optimal Budget” by Jip Spel, Svenja Stein and Joost-Pieter Katoen has been accepted for presentation at the 18th International Conference on Quantitative Evaluation of SysTems (QEST) in Warsaw, Poland. The paper tackles the problem of finding “almost optimal” valuations for parametric Markov chains, such that the expected reward to reach a target set is minimised, and applies them to controller synthesis in POMDPs.
The paper entitled “Inductive Synthesis of Finite-State Controllers for POMDPs” by Roman Andriushchenko_,_ Milan Ceska_,_ Sebastian Junges_,_ Joost-Pieter Katoen has been accepted for the 38th Conference on Uncertainty in Artificial Intelligence (UAI) in Eindhoven, The Netherlands. The paper was one of the 230 accepted papers out of 718 submissions. The paper proposes an inductive synthesis-based approach for the synthesis of finite memory controllers for indefinite-horizon reachability of…