MobilityReadingGroup

π-calculus, Session Types research at Imperial College

A Static Verification Framework for Message Passing in Go using Behavioural Types
Julien LANGE, Nicholas NG, Bernardo TONINHO, Nobuko YOSHIDA
To appear in
40th International Conference on Software Engineering (ICSE 2018)

The Go programming language has been heavily adopted in industry as a language that efficiently combines systems programming with concurrency. Go’s concurrency primitives, inspired by process calculi such as CCS and CSP, feature channel-based communication and lightweight threads, providing a distinct means of structuring concurrent software. Despite its popularity, the Go programming ecosystem offers little to no support for guaranteeing the correctness of message-passing concurrent programs.

This work proposes a practical verification framework for message passing concurrency in Go by developing a robust static analysis that infers an abstract model of a program’s communication behaviour in the form of a behavioural type, a powerful process calculi typing discipline. We make use of our analysis to deploy a model and termination checking based verification of the inferred behavioural type that is suitable for a range of safety and liveness properties of Go programs, providing several improvements over existing approaches. We evaluate our framework and its implementation on publicly available real-world Go code.

The tool for this paper Godel Checker is available here

@inproceedings{LNTY2018,
  author = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida},
  title = {{A Static Verification Framework for Message Passing in Go using Behavioural Types}},
  booktitle = {40th International Conference on Software Engineering},
  pages = {--},
  publisher = {ACM},
  year = 2018
}
@inproceedings{LNTY2018,
  author = {Julien Lange and Nicholas Ng and Bernardo Toninho and Nobuko Yoshida},
  title = {{A Static Verification Framework for Message Passing in Go using Behavioural Types}},
  booktitle = {40th International Conference on Software Engineering},
  pages = {--},
  publisher = {ACM},
  year = 2018
}