This page contains several diploma projects proposed for students. The list below includes several topics which are part of my research field and I'm interested in. I can also accept other proposals coming from students, with the reserve that those proposals are somehow connected to the ones below.
Before choosing me as an advisor, please make sure to establish an appointment with me (Contact). After the meeting we decide whether we can collaborate or not.
The blockchain is a very popular technology in the domain of cryptocurrencies (Bitcoin, Ethereum, Cardano, etc.). Ethereum is a blockchain platform that allows people to create smart contracts, a special type of programs that are executed by the network automatically.
I am interested in creating various DApps in Ethereum. Also, I am searching for people that want to advance the research in this domain by proposing languages, methods and tools for analysing smart contracts and their properties.
This project consists in formally defining an existing programming language in a dedicated framework (e.g., K, Coq, Agda, Isabelle, Maude, etc.)
There is a plethora of tools for static analysis of C/C++ code, but very few benchmarks. It would be interesting to create a tool which tests how well these static analysis tools perform over existing benchmarks. Moreover, it would be interesting to create more challenging benchmarks that cover many C/C++ features. These benchmarks can then be used for clasifying the existing static analysis tools into categories (i.e., how well these perform on finding memory allocations error, or numerical errors, etc.).
This projects aims to verify challenging but very well-known algorithms in the literature. The goal is to show that various logics for program verification (e.g., Hoare Logic, Matching/Reachability Logic, Separation Logic, etc.) can also be used for verifying algorithms. An example is the Knuth-Morris-Pratt algorithm that was proved using Reachability Logic in this paper.