I am interested in projects that explore the correctness of concurrent and distributed systems. This includes developing tools for visualisation, simulation and other applications. Students will benefit most from working in groups of two or three. I am happy to supervise projects from all study programmes, both at the BSc and MSc level, including MSc theses.

Projects

• Communication Protocol Visualisation
  • Develop a tool that reads a specification of a communication protocol (in a choreographic language or some other simple DSL) and produces an interactive visualisation that represents the protocol. By interacting with it, one can explore the different possible runs of the protocol, including branching choices, concurrent steps, and parallel interactions. The project will require designing a small protocol language, implementing the visualisation tool, and exploring case studies. The project deliverables include a working prototype with at least two use cases and a report. As an optional extension, the tool may simulate probabilistic message delivery.
  • Keywords: visualisation, distributed protocols, concurrency, tooling
  • Level: BSc/MSc

• Extracting and Verifying Communication Protocols from Distributed (Rust) Code
  • Develop a tool that analyses distributed programs (preferably in Rust but other programming languages are possible) and automatically extracts all communication operations, abstracting them into a protocol representation or state machine. The tool should then translate this representation into the input language of a model checker such as SPIN (Promela) or TLA+ (TLC), enabling verification of properties like functional correctness, deadlock freedom, or other protocol-level guarantees. Students will experiment with real Rust implementations and demonstrate the approach on a few concrete examples. As an optional extension, the tool may handle dropped or out-of-order messages to explore robustness under realistic distributed conditions.
  • Keywords: messaging, protocols, distributed systems, model checking
  • Level: BSc/MSc

• Neural Network-Based Protocol Mining
  • Develop a tool that trains a neural network to infer communication protocols from network traces. The network is trained on observed traces paired with known protocol specifications and, once trained, can predict unknown or partially observed protocol behaviors. The protocol language may include probabilistic elements, capturing message choices, delays, or failures. The project will require designing the neural network, generating synthetic training data (e.g., via an automatic protocol generator), and validating predictions through simulations. The deliverables include a working prototype capable of learning from traces and producing estimated protocol representations.
  • Keywords: neural networks, protocol mining, distributed systems, tool, simulation
  • Level: BSc/MSc
• Interactive DSL for Structured Content in Jupyter (with Dan W. Hansen)