Our project aims to make it possible to catch more errors at compile-time when working with Kotlin. We are developing various compile-time checks, such as:

• Cyclic dependencies in static initialization.

• Equality comparisons between objects of unrelated types.

• Incorrect usage of scoped resources like files and coroutines.

We are also developing a Kotlin compiler plugin for formal verification, Snakt (https://github.com/jesyspa/snakt/), which translates Kotlin into Viper. There are several potential internship projects here, such as:

• Verification of higher order functions.

• Implementing a uniqueness type system.

The Kotlin compiler builds a control flow graph of the code, and many of our projects require working with this graph. We have prepared the following test task to help you familiarise yourself with this kind of data structure.

• Currently pursuing or recently graduated from a Computer Science degree, or a degree in a related field.

• Excellent command of oral and written English

• Programming experience (familiarity with Kotlin is a plus)

• Experience with compilers or formal verification is a plus