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, Promela and TLA+ (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.
The FSA research cluster maintains the model checking tool set mCRL2 (https://mcrl2.org/). To improve verfication performance, the tool contains a variety of static analysis techniques aimed at simplifying the input before further analysis. A new and experimental tool in this category is lpsparvalues. The basic idea it implements is to use dataflow analysis to deduce which values can be reached for each process parameter. Thus the tool effectively produces and invariant, if it terminates. The goal of this project is experiment with various inputs to see how the tool behaves. Then, the objective is to describe the underlying algorithm and consider various improvements to boost the performance or practical applicability.
Over the past decades, tools for deciding the Boolean satisfiability problem (so called SAT solvers) have made great advances. They are now used in a wide variety of applications, including verification. Since Boolean satisfiability is NP-complete, SAT solvers are a natural target for solving other NP-complete problems. In this project, we investigate how NP-complete puzzles can be encoded in SAT and how the encoding can be optimised to solve larger instances. This requires studying SAT literature, creating a suitable encoding in SAT, implementing this encoding using one of the state-of-the-art tools and performing experiments with this implementation.
Students: Trayana Gerova, Matthijs Smulders, Shashwat Tewari, Szonja Sipos, Robert Abernethy, Claudia Arribas Morales