et en

Kalmeri 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, and for the master level, acceleration of fixpoint calculation. You may propose your own 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)

Programming language course

We used to have a course called Programming Languages, where we taught different programming languages. As it was mandatory for informatics students, we did not get to any interesting topics. If you love a programming language (such as Rust) then why not develop some course materials for us such that it displays the strengths of that language. If we collect enough teaching materials for different languges, we can create a real course out of them.

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

Completed theses