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
}