Moves News

Three Papers at CAV 2020

The following three papers from the MOVES Group have been accepted for presentation at CAV 2020: “PrIC3: Property Directed Reachability for MDPs” by Kevin Batz, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja and Philipp Schröer “Stochastic Games with Lexicographic Reachability-Safety Objectives” by Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger and Tobias Winkler, and “Unbounded-Time […]

Paper at PODS 2020

The paper entitled “Generative Datalog with Continuous Distributions” by Martin Grohe, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Peter Lindner has been accepted for presentation at PODS 2020, the ACM Conference on Principles of Database Systems. The paper provides a semantics to the probabilistic programming (aka: querying) language Datalog with continuous distributions.

Paper at NFM 2020

The paper “Benchmarking Software Model Checkers on Automotive Code” by Lukas Westhofen (OFFIS), Philipp Berger and Joost-Pieter Katoen has been accepted for presentation at the 12th NASA Formal Methods Symposium. The paper reports on applying 12 SVComp and one commercial software model checkers on two C programs from automotive. Bottom line: the tools from SVComp […]

Principles of Model Checking in Chinese

We are pleased to announce that Tsinghua University Press is about to publish a Chinese translation of the book “Principles of Model Checking” by Christel Baier and Joost-Pieter Katoen (MIT Press, 2008).

New Job Opportunities as Student Assistant

As Prof. Katoen has become the head of the ICT Profilearea, we are looking for two new student assistants. Further information can be seen in the following document: Job Information

Paper in Acta Informatica

The paper “Indecision and Delays are the Parents of Failure — Taming them Algorithmically by Synthesizing Delay-Resilient Control” by Mingshuai Chen (RWTH), Martin Fränzle, Yangjia Li, Peter N. Mosaad and Naijun Zhan was accepted for publication in the journal Acta Informatica.

Four Papers at TACAS 2020

Four papers have been accepted to TACAS 2020 in Dublin in which our group is involved: “Learning One-Clock Timed Automata” by Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang, and“Interpretation-Based Violation Witness Validation for C: NITWIT” by Jan Svejda, Philipp Berger and Joost-Pieter Katoen, and“Scenario-Based Verification of Uncertain MDPs” by Murat Cubuktepe, […]

EAPLS PhD Dissertation Award 2018

We are excited to announce that Christian Hensel has won the EAPLS (European Association of Programming Language and Systems) PhD Dissertation Award 2018. His dissertation on “The Probabilistic Model Checker Storm” has been selected by an international jury among all nominated dissertations. The official announcement can be found here.

Incubator Grant for COMPASS

Anzen Engineering has been granted an ESA-BIC Incubator Grant to further develop the COMPASS 3.0 tool that has been developed by the MOVES group in close cooperation with the Embedded Systems Group at FBK Trento (Italy) in the context of several ESA-funded projects. They will further develop the COMPASS technology with the aim to open […]

Paper in STTT

The paper entitled “IC3 Software Model Checking” by Tim Lange, Martin R. Neuhäußer (Siemens AG), Thomas Noll, and Joost-Pieter Katoen has been accepted for the International Journal on Software Tools for Technology Transfer (STTT). The paper introduces an extension of the IC3 verification algorithm for computer software that employs an explicit representation of a program’s […]