Suggestions for Theses and Project Topics

 

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.

 

Area: Functional Programming

  • 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.

  • Design and Implementation of a generic policy-specified, AI-driven customer relationship management systems in F# (Gagan Madaan).

  • Desgin and Implementation of an library for dual-rail functional types and their application in the synchronisation of shared memory multi-threading (F# or Haskell).

  • Graphical simulation of a concurrent execution of λ-calculus with scheduling policies in the IO monad

  • Programming and benchmarking of distributed algorithms in Haskell

  • Simulation of the operational semantics of functional programming using diagrammatic graph rewriting tools, e.g. see the SPARTAN diagrammatic visualiser

     

    Area: Cryptography and Protocols

    • Design and Implementation of Trusted Smart Contracts Using Block Chain Technology (thesis only)

    • Design and Implementation of an Electronic Voting Protocol (Tenzin Gyurmey)

    • Design and Implementation of Zero-Knowledge Protocols for Internet Applications

    • Survey of Logics for the Formal Verification of Security Protocols (thesis only)

    • Design and Implementation of a Cryptolibrary in the SCADE Design Tool Suite

    • Implementation and Benchmarking of the E-Pass Protocol Standard in the SCADE Design Tool Suite

     

    Area: Distributed Algorithms

    • 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: Deterministic/Synchronous Programming

    • Synchronous embedded programming of XDK Nodes for physiotherapeutic applications

    • Synchronous Scheduling Policies in Java - A Case Study

    • Monte Carlo Scheduling of Policy-constructive Synchronous Programming (BSc thesis, Sina Fricke)

    • Evaluation of a Haskell Library for Deterministic Concurrent Programming.

    • 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 or any other concurrent programming language.

    • Static analysis of synchronous imperative code: Implementation of scheduling policies via dynamic priorities.
       
    • Thread-safe translaction level modelling in the TLM 2.0 Standard for SystemC.

      SystemC is a library in C++, to build hardware system simulation models. It supports thread processes, events, clock signals, mutex, locks, FIFO channels. In the TLM 2.0 standard for Transaction Level modelling the safe synchronisation channels have been removed, with the effect that now threads can enter data structures freely. This is efficient in simulation but potentially unsafe. The project will investigate the use of synchronisation policies to guard such data structures to regain thread-safety by implementing associated conflict-freeness checks. This conflict analysis (= causality analysis) will ensure that concurrent execution does not invalidate the sequential SystemC standard.

    • 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

    • AADD Affine arithmetic decision diagrams (Christoph Grimm FDL2018, TCAD 2018)
      Instrumentation of SystemC code to turn normal semantics to symbolic execution semantics. Investigate as a staged computation model using modal types (Pfenning & Davies) to generate safe programming of mixed-concrete-symbolic C++ code. Investigate their use for model-predictive control; for computing predictions in constructive scheduling.

     

    Area: Applications of Formal Logic

    • Formal Specification of Degree Programme Requirements in Description Logic

    • Student Decision Support Tool in Constraint Logic Programming

    • Modelling Degree Progamme Regulations in 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 (Jonas Huisl)
       
    • Implementation of a Fitch-style proof system for constructive modal logic

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

     

    General Structure of Theses

    The following is copied (and slightly modified) from the guidelines of the Computer Networks and Communication Systems Group at Friedrich-Alexander University of Erlangen:

     

    Document Structure

    The ratio between the main sections (3.-5. below) is 1/3 to 1/3 to 1/3!

    1. Abstract / Kurzfassung: each about 1/2 page

    • How to write an abstract
    • Motivation (Why do we care?)
    • Problem statement (What specific problem are you trying to solve?)
    • Approach (How did you go about it)
    • Results (What are your findings?)
    • Conclusion (What are the implications?)

    2. Introduction (general motivation for your work, context and objectives): 1-2 pages

    • Context: make sure to describe where and how your work fits in
    • Problem: e.g., knowledge gap, too expensive, too slow, a deficiency, superseded technology
    • Strategy: the way you will address the problem

    3. Fundamentals / environment and related work: 1/3

    • employed hardware and software
    • describe methods and techniques that build the basis of your work
    • introduce any necessary mathematical notation and terminology
    • review related work

    4. Developed architecture / system design / algorithms / implementation: 1/3

    • start with a theoretical approach
    • describe the developed system/algorithm/method from a high-level point of view
    • go ahead in presenting your developments in more detail

    5. Measurement results / analysis / evaluation / discussion: 1/3

    • whatever you have done, you must comment it, compare it to other systems, evaluate it
    • usually, adequate graphs help to show the benefits of your approach
    • each result/graph must be discussed! what’s the reason for this peak or why have you ovserved this effect

    6. Conclusion: 1 page

    • summarize again what your paper did, but now emphasize more the results, and comparisons
    • write conclusions that can be drawn from the results found and the discussion presented in the paper
    • open problems, future work (be very brief, explain what, but not much how)

    7. References

    • all papers and articles used in the thesis must be cited (and each reference must be used in the thesis!)
    • a rough number is 20 references for a bachelor thesis and 30-40 for a master’s thesis
    • avoid to cite web sites, in any case add date of last visit
    • We highly recommend to use Endnote or BibTeX for creating the references and citings
    • Further information: IEEE Rules, BibTeX

     

    Writing style

     

    • Avoid colloquial or emotional language
    • Avoid passive voice, active voice is easier to read. There is nothing wrong saying I (or we) did it
    • Avoid negative sentences: write in a positive (affirmative) voice, they are easier to understand.
    • Always use vector graphics for figures (PDF, EPS, …)
    • Use a spell checker to eliminate typos

    No Plagiarism

     

    • Note that any form of plagiarism is seriously punished. For a definition and the different forms of plagiarism please see e.g. the definition on Wikipedia
    • As a rule: Never copy any text literally from other sources without both clearly citing the source and explicitly quoting the text passages that are copied.
    • Warning: Even if you cite the source at the beginning of a paragraph and then literally reproduce pieces of text from cited external sources without quoting the respective passages you effectively claim that the wording is your own intellectual property. Since this is a false claim you can get punished for plagiarism. This normally means your work is rejected as failed and unmarked.  

    Last Minute Checks

     

    • Did I spell out the main points of the interpretation of results?
    • Are all equations, figures, tables numbered?
    • Do all graphs, tables, diagrams have descriptive captions?
    • Are all axes and scale carefully chosen to show the relevant effects?
    • Are all axes labelled? Do the labals include the measurement units?
    • Are citations in the caption (if a graph is borrowed)?

     

    Further reading