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:

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

• Use of metaheuristics to solve the team formation problem

Supervisors: Yeray Barrios FleitasEduardo Lalla

Suppose we want to create the most optimal student teams in a sample of N students based on X team characteristics. Of course, you could use a greedy algorithm that analyzes all possible combinations and always finds the optimal solution. However, the search for this solution becomes difficult to execute in polynomial time after a specific sample size.

This is known as an NP-hard problem. One way to solve this problem is using metaheuristics, a heuristic method that offers quality solutions (close to the optimum) in a reasonable time.

Among the goal of this project, you must:

1. Identify the threshold where the sample size and the number of considered criteria make this problem impossible to run in polynomial time.
2. Review the metaheuristics used in the literature to solve this problem in the form of a taxonomy.
3. Run a performance analysis on an actual data set to determine which metaheuristics work best with this problem.

As supervisors, we will provide you with the sources of knowledge and material necessary to write a research paper successfully. If the student obtains significant results and is interested, s/he may consider writing a scientific article for publication in a conference or journal.

• Debug information for verified programming

Supervisors: Edoardo Putti, Peter Lammich

Once you proved your program correct there is no need to debug it! Unfortunately all tools for performance analysis require debug information. We want to generate debug information for our verified program so that we can optimize them further. In this project you will learn how to use LLVM to generate debug information so that profilers and debuggers can be used with our verified toolchain.