Date and time: 12.03.2018 14:15-15:00

Speaker: Nobuko Yoshida and Nicholas Ng

Title: Behavioural Type-Based Static Verification Framework for Go

Place: TBA

Slides can be found here (TBA)

Abstract:

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 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.

This is joint work with Julien Lange and Bernardo Toninho