  Go is a popular concurrent programming language thanks to its ability to
efficiently combine concurrency and systems programming. In Go programs, a
number of concurrency bugs can be caused by a mixture of data races and
communication problems. In this paper, we develop a theory based on behavioural
types to statically detect data races and deadlocks in Go programs. We first
specify lock safety and liveness and data race properties over a Go program
model, using the happens-before relation defined in the Go memory model. We
represent these properties of programs in a $\mu$-calculus model of types, and
validate them using type-level model-checking. We then extend the framework to
account for Go's channels, and implement a static verification tool which can
detect concurrency errors. This is, to the best of our knowledge, the first
static verification framework of this kind for the Go language, uniformly
analysing concurrency errors caused by a mix of shared memory accesses and
asynchronous message-passing communications.
