Skip to main content

A Static Verification Framework for Message Passing in Go using Behavioural Types

Lange, Julien and Ng, Nicholas and Toninho, Bernardo and Yoshida, Nobuko (2018) A Static Verification Framework for Message Passing in Go using Behavioural Types. In: Proceedings of the 40th International Conference on Software Engineering. ICSE International Conference on Software Engineering . ACM, New York, USA, pp. 1137-1148. ISBN 978-1-4503-5660-2. (doi:10.1145/3180155.3180157) (KAR id:65587)

PDF Publisher pdf
Language: English

Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (348kB) Preview
PDF Author's Accepted Manuscript
Language: English

Restricted to Repository staff only
Contact us about this Publication
Official URL


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 guarantee- ing 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.

Item Type: Book section
DOI/Identification number: 10.1145/3180155.3180157
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Faculties > Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 15 Jan 2018 17:50 UTC
Last Modified: 22 Jan 2020 16:41 UTC
Resource URI: (The current URI for this page, for reference purposes)
Lange, Julien:
  • Depositors only (login required):


Downloads per month over past year