Prof. Dr. Roland Meyer, TU Braunschweig - Pointer Race Freedom:
We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results.
(1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection.
(2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speed-up of up to two orders of magnitude.
Prof. Dr. Anne Remke, Universität Münster - Critical Infrastructures:
Critical infrastructures are (remotely) controlled by ICT networks and subject to cyber and physical failures that pose a serious threat to their dependability and survivability. It is important to be able to quantify the impact of failures on the physical process and to be able to analyse how quickly such systems recover to acceptable levels of service after the occurrence of failures, e.g., leakages or component breakdowns.
The so-called survivability expresses how quickly systems recover to acceptable levels of service, using so-called Given the Occurrence Of Disaster (GOOD) models. We use Stochastic timed logic (STL) to rigorously define the notion of survivability and evaluate STL formulas using model checking techniques e.g. on Hybrid Petri nets.
This modeling formalism of Hybrid Petri nets incorporates continuous and discrete elements as well as stochastic variables to describe the occurrence of random events, and their fluid dynamics. New efficient techniques are needed to evaluate the evolution of the system over time. Both, symbolic and numeric techniques are currently investigated in order to tackle systems with a large number of stochastic events.