Abstract: Many compiler verification and optimization problems come down to reasoning about aliasing: determining when two references may point to the same object. This talk presents a methodology for reasoning about aliasing in Kotlin using locality and uniqueness properties implemented in SnaKt, a formal verification compiler plugin developed with the Kotlin team. The locality checker lets us specify that a reference must not leak into global state, while the uniqueness checker lets us specify that a variable holds the only usable copy of a reference. Together, these properties ensure that operations affect only the intended state, potentially enabling sound reasoning about heap updates in SnaKt and unlocking performance benefits in the Kotlin compiler.

Host: Davide Paolo Tua