Skip to content

Laboratory for Software Science

Kalmer Apinis

Formal Verification of an Algorithm in Rocq

Thanks to AI, it is nowadays rather easy to formally prove the correctness of many algorithms. One such system is the Rocq Prover, where you can implement an algorithm, prove properties about it, and extract the algorithm to OCaml or Haskell.

It is best if you propose your own algorithm, but we may be able to find tasks related to static analysis.

Topics

  • Prove the correctness of an algorithm of your choice
  • Prove something related to static analysis.

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 20 years. However, practically usable tools for everyday users are hard to find.

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

Topics

  • Explanation of relational analysis results (suitable for a scientific paper)
  • 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.

Topics

  • projektitööd õppematerjalide loomine kursusele FP
  • mingi muu teema, mis teeb FP kursust paremaksSolving 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

Accept Cookies