Out-of-the-Box Ideas

Think outside the box!

You are always welcome to submit your own project proposals, even if they do not fit in any of the categories (as long as they are somehow related to software technology or formal methods ;) ) Just contact any supervisor that you think might fit your idea.

Available Project Proposals

Moreover, here are some project proposals that do not fit elsewhere:

  • Timeline Verifier

    This project is about developing a format for expressing timelines of fictional universes and placing characters on them, together with predicates that bind them in some sort of relationships ("is a teacher of", "is friends with", "has met", "is killed by"), and writing a small piece of software that verifies that that timeline is, indeed, consistent.

    See the full project description. Get in touch with your potential future supervisor to discuss details!

  • Build and Optimize a DRAT certificate checker

    Supervisors: Peter Lammich
    In this project, you will design and optimize a drat certificate checker. DRAT is used to certify the outputs of SAT solvers. While the certificate checker is less complex than a SAT solver, it still has to perform some time-critical operations, that can profit a lot from low-level optimizations.

  • Prove your Theorem with an Interactive Theorem Prover

    Supervisors: Peter Lammich
    Interactive Theorem Provers (ITPs) provide a way to develop computer checked (mathematical) proofs. In this project, you will learn to use an ITP, and apply it to formalize some interesting theory. The theory to be formalized will be chosen in coordination with the supervisor, to suit your interests and be realistically achievable for a BsC project.