Felix Stutz

Felix Stutz

Postdoc at University of Luxembourg | Former PhD student at MPI-SWS

Research Prototypes and Frameworks

I have been coding for different kind of projects. For some types of problems, tool support or an implementation is crucial – like the shell script parallelization framework PaSh. But some of my research has quite a theoretical focus so this is not necessarily the case. I still usually implement a prototype to play around with our ideas and evaluate them.

  • For our work on asynchronous multiparty session types, I developed the prototype AMGC [code] which implements our technique to generate verified participant specifications from global protocol specifications. For the theoretical foundations, check out our CONCUR21 paper.

  • I have contributed to the shell script parallelization framework PaSh [code]. Mainly, I designed, implemented and integrated an annotation library for command invocations [code, PyPI] that provides means to specify command invocation behaviours in the form of annotations. For PaSh, it provides parallelizability and input-output information. The accuracy of this information is crucial both for correctness and performance. Input-output information is required for the translation between actual shell scripts and our internal model for transformations.

  • Together with Julian Haas, I have built Heimdall [code] which provides message interception and scheduling utilities for Erlang applications. Erlang has built-in primitives to send and receive messages as well as standard libraries for message-passing programs. We instrumented these libraries to intercept and control the delivery of messages with different schedulers. This can be used to test Erlang programs with different scheduling algorithms.

  • The prototype Lemma9 [code] implements our approach for verifying cryptographic protocols that we presented at CONCUR20. It can infer and check inductive invariants for protocols with an unbounded number of sessions.

  • As an undergraduate assistant, I helped with the initial version of PROSA, which is a Coq framework of and for definitions and proofs for real-time schedulability analysis.