For your quick reference, here is a selection of thesis topics and projects for BSc or MSc students which are currently on offer from the Informatics Theory Group. If you are a committed student with mathematical interests who would like to join in foundational research, then the following projects might be of interest to you. The language for all projects is German or English. The staff of the Theory Group are happy to provide more detailed information about the projects listed below.

The concrete definition of the work (scope and deliverables) will be done in consultation with the supervisor depending on your study level (BSc or MSc) and whether you are conducting a project or a thesis.

The following list reflects the research interests of the Theory Group. As such it is an indication only of what sort of projects could be accommodated. You are invited to negotiate other (also practical programming-oriented) topics within the following research areas with us.

• NEW:  Studying the soundness of SHAP explanations of machine learning predictions,(78.8 KB)Co-supervised MSc thesis with internship at the University of Montpellier, France.

Area: Synchronous Reactive or Embedded Programming

• Clock-synchronised Shared Memory and automatic causality analysis for sequentially constructive synchronous programs using SPIN/Promela
   
• Synchronous Programming in Rust
   
• A System-C Library extension for synchronous programming (Esterel constructive circuits, SCCharts, Blech)
   
• Design of a simulator for sequentially constructive kernel language SCPL and a translation of the Blech real-time embedded programming language into SCPL.
   
• Development of a Cloud IDE for a synchronous programming language (e.g., Blech, Esterel, Lustre, ...) with graph visualisation using Theia & Sprotty
   
• Synchronous embedded programming of XDK Nodes for physiotherapeutic applications
   
• Synchronous Scheduling Policies in Java/Typescript - A Case Study in Concurrency (for Typescript, see e.g., Hiphop, http://hop.inria.fr; http://hop.inria.fr/hiphop)
   
• Monte Carlo Scheduling of Policy-constructive Synchronous Programming. A compiler-optimisation problem in CompPy.
  .
• Syntax Highlighting, Type Checking, Schedulability Analysis and Symbolic Simulator for Policy-synchronised shared memory programming using the Microsoft Language Server Protocol.
   
• Concurrent Programming via Synchronous Scheduling Policies in C++11/F#/Haskell/Go/Rust/Typescript or any other concurrent programming language.
   
• Static analysis of synchronous imperative code: Implementation of scheduling policies via dynamic priorities.
   
• Synchronous Policies as an Eclipse Compiler Plugin for the KIELER Model-based Design Suite (MSc thesis only)
   
• WCRT Timing Analysis for Synchronous Programs.
   
• Speed-independent hardware implementation of a sequentially constructive language (SCL) using Inertial Delays
   
• Implementation of synchronous real-time programs using Time-sensitive Networks (TSN)

Area: Functional Programming

• Impelementation of policy-interfaces for determininistic black-box procedures in synchronous programming language Blech (F# compiler)
   
• Design and Implementation of a library for deterministic shared memory multi-threading (F# or Haskell).
   
• Implementation and benchmarking of a clock calculus for synchronisation of the dataflow functional programming language Lustre (Haskell, SCADE).
   
• (M)ILP Design and implementation of a domain-specific library for dataflow process networks in Haskell, combining different models of synchronisation such as KPN (Kahn Process Networks), BDF (Boolean Dataflow), SDF (Synchronous Dataflow), HSDF (Homogeneous Synchronous Dataflow), CSDF (Cyclostatic Dataflow), DDF (Dynamic Dataflow) and SADF (Scenario-aware Dataflow).
   
• Implementation and benchmarking of synchronous control flow programs in a functional language (such as Haskell or F#)
   
• Implementation and benchmarking of deterministic shared data structures (IVar, MVar, LVars, ...) on multi-core processors
   
• Specification and automatic verification of synchronisation interface policies using refinement types in LiquidHaskell.
   
• Graphical simulation of a concurrent execution of λ-calculus with scheduling policies in the IO monad
   
• Simulation of the operational semantics of functional programming using diagrammatic graph rewriting tools, e.g. see the SPARTAN diagrammatic visualiser

Area: Distributed Algorithms

• Simulator for a concurrent process algebra with priorities (Concurrency Worksbench)
   
• Specification and Verification of Clock Synchronisation Protocols using the SPIN/Promela modelling language and temporal Logic modelchecker
   
• Fault-tolerant, Self-stabilising Synchronous Web Programming
   
• Development and Validation of Haskell API for Concurrent Programming of a Railway Control System (BiDiB library in C, Example Command line programs (REST server + client).

Area: Applications of Formal Logic
 

• Implementing an interactive theorem prover for constructive modal logic
   
• Modelling Degree Progamme Regulations in Descriprion Logic and Answer Set Programming
   
• Formal Modelling and Verification of Synchronisation Protocols for Deterministic Concurrency.
   
• Automatic translation of Fitch-style induction Proofs into natural language.
   
• Diagrammatic visualisation of the formal semantics of natural language (parsing and generation of LaTeX graphics).
   
• Implementation of the computational semantics of the modal lambda calculus Lambda-CK

• Implementation of Proof Tactics for Constructive General Multiple Winner Logic in a theorem prover such as ISABELLE