I am a PhD student in the MPI-SWS’s Models of Computation group headed by Georg Zetzsche. My research interests lie mainly in increasing the safety and reliability of programs. I approach this from two perspectives: Extending programming languages with capabilities that help certify invariants (e.g. dependent type systems) and investigating the foundations of formal verification, the underlying models of computations.
A pushdown vector addition system with states (PVASS) extends the model of vector addition systems with a pushdown store. A PVASS is said to be bidirected if every transition (pushing/popping a symbol or modifying a counter) has an accompanying opposite transition that reverses the effect. Bidirectedness arises naturally in many models; it can also be seen as a overapproximation of reachability. We show that the reachability problem for bidirected PVASS is decidable in Ackermann time and primitive recursive for any fixed dimension.
Giving tight estimates for output bounds is key to an accurate network analysis using the stochastic network calculus (SNC) framework. In order to upper bound the delay for a flow of interest in the network, one typically has to calculate output bounds of cross-traffic flows several times. Thus, an improvement in the output bound calculation pays off considerably. In this paper, we propose a new output bound calculation in the SNC framework by making use of Jensen’s inequality.
The FAIR control system (CS) is an alarm-based design and employs White Rabbit time synchronization over a GbE network to issue commands executed accurate to 1 ns. In such a network based CS, graphs of possible machine com- mand sequences are specified in advance by physics frame- works. The actual traffic pattern, however, is determined at runtime, depending on interlocks and beam requests from experiments and accelerators. In ’unlucky’ combinations, large packet bursts can delay commands beyond their deadline, potentially causing emergency shutdowns.