If you are looking for a final project, please contact me so we can have a discussion. Below are suggestions for possible projects. You are also free to contact me with your own project idea.
The mCRL2 toolset has its own input language for formal specification of behaviour, which is very versatile. There are, however, many more formal specification languages, for example PNML (for Petri nets), NuSMV and Promela (for Kripke structures) and many more. The goal of this project is to implement one or more translations from these other languages to mCRL2. With this translation/these translations, we can execute various experiments to assess the performance of the mCRL2 model checking engine compared to other state-of-the-art tools.
AuDaLa (Autonomous Data Language) is a programming language developped at the Formal System Analysis group at the TU/e.The purpose of this language is to make massive parallel programming easier, requiring less study of a language such as CUDA and all its advanced features. Currently, there is a complete formalisation of the language [1,2], including syntax and an operational semantics. Furthermore, there is a prototype compiler [3] from AuDaLa to CUDA, which enables running AuDaLa programs on a graphics processing unit (GPU).
The goal of this project is to improve the compiler so that it generates highly-optimised CUDA code. This requires studying the AuDaLa language, CUDA and the current compiler written in Rust. If necessary, AuDaLa may also be extended with new features to further boost the performance. Experiments with a range of AuDaLa programs should show how it compares to traditional parallel implementations.
[1]: Tom T.P. Franken, Thomas Neele, Jan Friso Groote. An Autonomous Data Language. ICTAC 2023. LNCS, vol. 14446, pages 158-177. (link)
[2]: Gijs Leemrijse. Towards relaxed memory semantics for the Autonomous Data Language. MSc thesis, Eindhoven University of Technology. 2023. (link)
[3]: AuDaLaC compiler github.com/GPLeemrijse/AuDaLaC.