The paper entitled “Natural Strategic Ability in Stochastic Multi-Agent Systems” by Raphael Berthon, Monyque Myttelmann, Antoniello Murano and Joost-Pieter Katoen has been accepted for the 38th AAAI Conference on Artificial Intelligence (AAAI 2024) in Vancouver, Canada. The paper present complexity result on the model checking of the probabilistic alternating temporal logics PATL and PATL∗ under […]

Two papers were accepted at the Dafny 2024 workshop. The paper “Caesar: A Verifier for Probabilistic Programs” by Philipp Schröer, Kevin Batz, Benjamin Kaminski (Saarland University and UCL), Joost-Pieter Katoen and Christoph Matheja (TU Denmark) presents a quantitative program verification infrastructure for discrete probabilistic programs, building on our work published at OOPSLA 2023. The paper […]

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 […]

Tom Biskup has received the Berthold Vöcking Master Award 2023 for his thesis “Invariant-based Strategy Synthesis for Nondeterministic Probabilistic Programs”. The thesis addresses the problem of making provably good decisions in face of stochastic uncertainty which is key in, e.g., complex planning tasks. Tom’s solution draws on well-known principles from deductive program verification such as […]

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 […]

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.

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 […]