et en

Kalmer Apinis

Formal Verification of an Algorithm in Rocq

One way to obtain a correct piece of code is to generate it from Rocq code, where correctness can be formally proven. Since formal verification is rather complex, it is not possible to choose a very complicated algorithm for a thesis. At the bachelor’s level, I suggest interval arithmetic. It would be great if someone could continue the work of Aksel Õim and create a practically usable correct implementation of the Push-Relabel algorithm. You may also propose your own favorite algorithm.

Another option would be to continue the work of Kadi Sammul and prove something related to our PRG project. In that case, there could also be a possibility to pay a scholarship.

Topics

  • Prove the correctness of an algorithm of your choice
  • Develop a practical implementation of the Push-Relabel algorithm
  • Prove something related to solvers for systems of equations

Static Analysis of Java Bytecode

Our research group has extensive experience with static program analysis of the C language. Now we would like to extend this to analyzing programs in the Java world. Static program analysis computes invariants of a program based on its code. On this basis, one can make assessments about the program’s (correctness). Of course, this depends on which analyses are run (i.e., which invariants are sought).

According to the theory of abstract interpretation, static program analysis was essentially solved already in the 1970s. Our research group members have also been writing scientific papers and programs on program analysis for 15 years. However, practically usable tools suitable for everyday users hardly exist.

Since this topic is related to our PRG project, we may also discuss the possibility of paying a scholarship for these topics.

Topics

  • Implementation of solvers for systems of equations (based on scientific papers)
  • Explanation of relational analysis results (suitable for a scientific paper)
  • Integration of memory analysis into the system
  • Improving the Põder analyzer to compete at SV-COMP
  • General improvements to the Põder analyzer

Teaching Materials for Functional Programming

There are many different directions to start from, but in the end, our goal is to obtain more high-quality, meaningful, and challenging assignments for the FP course. For example, translating some reactive programming solution from Haskell to Idris, studying/solving a typical data science problem in Idris, or exploring an interesting algorithm.

Topics

  • Project work on developing teaching materials for the FP course
  • Any other topic that makes the FP course better

Functional Programming

We know that FP is nice in theory. But is it actually nice to use in practice? To explore such questions, we are willing to supervise a task proposed by you, provided that its solution involves functional programming on a sufficiently large scale.

There is also the possibility of supplementing the FP textbook.

Teemad

  • projektitööd õppematerjalide loomine kursusele FP
  • mingi muu teema, mis teeb FP kursust paremaks

Topics

  • Solving a problem you propose with a modern FP language (e.g., Elm or Elixir)
  • Solving a problem you propose with a classic FP language (e.g., Haskell or OCaml)
  • Making tasks for FP textbook
  • Additional chapters of FP textbook -- OCaml, Elm, Haskell

Contact: Kalmer Apinis ([kalmer.apinis@ut.ee](kalmer.apinis@ut.ee))

Completed theses