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

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

The paper entitled “Synthesizing FDIR Recovery Strategies From Non-Deterministic Dynamic Fault Trees” by Sascha Müller, Andreas Gerndt (both from the German Aerospace Center (DLR)), and Thomas Noll has been accepted for publication in the Journal of Aerospace Information Systems. It shows how appropriate recovery strategies for dealing with failures in aerospace control systems can be […]

The paper entitled “Harrsh: A Tool for Unified Reasoning about Symbolic-Heap Separation Logic” by Jens Katelaan, Christoph Matheja, Thomas Noll and Florian Zuleger has been accepted for presentation at the 13th International Workshop on the Implementation of Logics (IWIL 2018). The paper presents a tool for unified reasoning about the symbolic-heap fragment of separation logic. […]

The paper entitled “Synthesizing and Optimizing FDIR Recovery Strategies From Fault Trees” by Liana Mikaelyan, Sascha Müller, Andreas Gerndt and Thomas Noll has been accepted at the 6th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2018) at Gold Coast, Australia. The key idea of the paper is to synthesize failure recovery strategies for […]

The paper “Graph-Based Shape Analysis Beyond Context-Freeness” by Hannah Arndt, Christina Jansen, Christoph Matheja and Thomas Noll has been accepted for publication at the 16th International Conference on Software Engineering and Formal Methods (SEFM 2018). It introduces a shape analysis for reasoning about relational properties of data structures that are maintained by a pointer program, […]

Joost-Pieter Katoen is awarded the prestigious ERC Advanced Grant from the European Research Council. It will allow to fund a project on formal reasoning techniques for probabilistic programs over a period of five years. ERC Advanced Grants are intended to support the very best research to be conducted in EU member states and associated countries. […]

The German Research Foundation (DFG) has approved to extend the funding period of the ATTESTOR project for another two-year period. The aim of the follow-up project is to develop novel techniques and tools to support formal reasoning on relational shape properties of (concurrent) pointer programs, allowing e.g. to reason about balanced tree data structures. The […]

The MOVES group is co-organising a seminar on Analysis and Verification of Pointer Programs, which will be held from October 2 to 5, 2017, as an NII Shonan Meeting at Shonan Village Center in Japan. This meeting will be a scientific event bringing together both theoreticians and practitioners working on different techniques for heap abstraction […]

The MOVES group proudly announces that Professor Joost-Pieter Katoen has received a Honorary Doctorate from Aalborg University, Denmark. He was awarded for his distinguished efforts in the field of Computer Science, in particular Computer-Aided Verification. The (Danish) laudation can be found here.