A static verification framework for message passing in Go using behavioural types

Julien Lange, Nicholas Ng, Bernardo Toninho, Nobuko Yoshida

Abstract

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.

BibTeX

@inproceedings{Lange-al:ICSE18,
  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 = {ICSE},
  pages     = {1137--1148},
  publisher = {{ACM}},
  year      = {2018},
}

A static verification framework for message passing in Go using behavioural types

Abstract

Related papers