This year’s RaW projects will be all about characterizing and checking behavioral equivalences (bisimilarity, trace equivalence, etc) using a nice game-theoretic framework. The topic connects to a wide range of exciting research areas such as program semantics, concurrency theory, model checking, graph algorithms, quantitative games, and modal logics.

We will mainly use the proof assistant Isabelle/HOL to formalize our work. There might also be groups who implement aspects in Scala.