et en

Kalmer Apinis

Formally proving some algorithm in Coq

One way to produce a correct software module is to generate it from Coq code, where you can formally prove correctness. As formal proofs are difficult, we cannot choose a very complicated algorithm. For the bachelor level, I propose implementing interval set arithmetic. Another good option would be to continue the work of Aksel Õim and produce a practically usable correct implementation of the Push-Relabel algorithm. But you may also propose your own favorite algorithm.

Static analysis of Java bytecode

We have a lot of experience doing static analysis of C programs. Now we want to also analyse programs in the Java world. Static analysis computes invariants based on the source code and the invariants can be used to assess the correctness of programs. This of course depends on the analysis --- which kinds of invariants can be detected.

Abstract interpretation theoretically solved static analysis already in the seventies. Our group also has been writing analysers and research papers for 15 years. But still there are no practically usable analysis tools which do no require expert knowledge.

Topics

  • implementation ofa a constraint system solver (based on a paper)
  • explaining a relational analysis (possible to write a paper)
  • Fix the Põder analyzer so that it can compete in SV-COMP

Study materials for Functional Programming

There are many different options to start with, but ultimately, we want to get high-quality, meaningful, and challenging assignments for the FP course. For example, translate some reactive programming solutions from Haskell to Idris, study/solve some standard data science problems in Idris, or study some interesting algorithms.

Contact for more info: Kalmer Apinis (kalmer.apinis@ut.ee)

Completed theses