Nicholas Ng

Go concurrency verification

Golang static analysis process calculi behavioural types

The aim of this line of work is to verify channel-based concurrency interaction in Go using techniques from the research area of process calculi and type systems. This is a joint work with Bernardo Toninho (@bernpton), Julien Lange (@julienlange) and Nobuko Yoshida.


nickng/dingo-hunter is a static analyser for Go based on the go/ssa package from the Go project. The tool itself is designed to be an interface to Go programs, performing type inference/model extraction from Go code. Current analysis frontends include:

nickng/gospal is a new static analyser library for Go, also based on the go/ssa package from the Go project. It is a modular library that allows for analysis components to be reused. A context-sensitive MiGo inference tool migoinfer was built using the library which has better code coverage and error handling than the predecessor.