Colloquium Computer Science - Prof. N. Yoshida

Title:
Behavioural Type-Based Static Verification Framework for Go

Abstract:
The talk gives an overview of our several works on the programming language Go:
- POPL'17: Fencing off go: liveness and safety for channel-based programming
- ICSE'18:  A Static Verification Framework for Message Passing in Go
using Behavioural Types
- POPL'19: Distributed Programming Using Role Parametric Session Types in Go.

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.

We present a static verification framework for liveness and safety in
Go programs, able to detect communication errors and deadlocks by
model checking. Our toolchain infers from a Go program a faithful
representation of its communication patterns as behavioural types,
where the types are model checked for liveness and safety.
We also present a recent code generation for Go.