In this talk, first I give an overview of activities in our session type group in Imperial and how mCRL2 is used in our researches.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work, we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by mCRL2. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioral types, where the types are model checked for liveness and safety.