Felix Stutz

Felix Stutz

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

Research Prototypes and Frameworks

I have worked on a variety of problems that give rise to different kinds of software artifacts. Some projects require concrete implementations or tool support, like the annotation library for PaSh. Others are more theoretical – focused on formalization and proofs – yet we still enjoy building prototype tools to explore our ideas and validate our findings.

  • Sprout – Symbolic Protocol Verifier [code]
    Sprout is an implementability checker for symbolic multiparty protocols. It takes as input a global protocol specification with dependent refinements on message values and loop memory. It then determines if the desired behaviour can be realised in a distributed setting. Our OOPSLA 2025 paper provides the theoretical foundations while our CAV 2025 paper gives details on the implementation.

  • AMGC – From Global Protocol Specifications to Participant Specifications [code]
    For our work on asynchronous multiparty session types, we implemented our techniques to generate verified participant specifications from global protocol specifications. For the theoretical foundations, check out our CONCUR21 and CAV23 papers.

  • Annotation Library for Command Invocations in PaSh [code, PyPI]
    I designed, implemented and integrated an annotation library for command invocations that provides means to specify command invocation behaviours in the form of annotations. For PaSh, it provides parallelizability and input-output information and its accuracy is crucial both for correctness and performance.

  • Heimdall – Message Interception and Scheduling Utilities for Erlang Applications [code]
    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.

  • Lemma9 – Inductive Invariants for Security Protocols [code]
    This prototype implements our approach for verifying security protocols, presented     at CONCUR20. It can infer and check inductive invariants for protocols with an unbounded number of sessions.

  • PROSA – Coq framework of and for definitions and proofs for real-time schedulability [repo]
    As an undergraduate assistant, I helped with the initial version of this framework, which has been presented at ECRTS16.