Diploma proposals

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.

Topics of interest

Blockchain related projects

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.

Semantics for real-life programming languages

This project consists in formally defining an existing programming language in a dedicated framework (e.g., K, Coq, Agda, Isabelle, Maude, etc.)

An example of such a framework in K. There are several programming languages defined in K: Javascript, C, [Java](K-Java: A Complete Semantics of Java), etc. The existing K definitions reveal several problems in the existing language standards (see this page for details)[http://www.kframework.org/index.php/K_Publications]. This project aims for finding other problems in the design of other languages at your choice.

Static analysis tools and benchmarks

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

Verification of challenging algorithms using logics for program verification

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.