The specific scope for the topics below can be adjusted for either Bachelor or Master Students.
- Implementing and Proving Algorithms in SPARK
SPARK is an Ada-based programming language, which is used for the developement of dedicated secure software. SPARK supports the specification and the verification of the information flow of an implementation, as well as pre- and postconditions. The goal is to implement easy algorithms in SPARK (sorting and searching, the arithmetic of big numbers, etc.), and to prove the implementations using the SPARK toolset.
- A Simulator/Demonstrator for Grover and Other Quantum Algorithms
Quantum algorithms have the reputation of being difficult to grasp. To some degree, this reputation may be well-deserved -- but not all quantum algorithms are so difficult. The main goal for the thesis is a simplified quantum simulator with a visual interface to implement some simple quantum algorithms, such as Grover's quantum search algorithm. The simulator shall be used to give junior students a first impression of quantum algorithms, e.g., in the context of "Byte the Bytes".
- Evaluation of RUST as a language for secure and reliable software.
RUST is a language which has been introduced with the development of reliable
software in mind. To evaluate RUST, some cryptographic library shall be
used and some security protocols shall be implemented, and compared to
implementations in other languages, such as the Ada language or C and C++.