Skip to main content

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

Lange, Julien, Ng, Nicholas, Toninho, Bernardo, 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: Software Engineering Education and Training. ICSE International Conference on Software Engineering . pp. 1137-1148. ACM, New York, USA ISBN 978-1-4503-5660-2. (doi:10.1145/3180155.3180157) (KAR id:65587)

PDF Publisher pdf
Language: English

Download (348kB) Preview
[thumbnail of p1137-lange.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF Author's Accepted Manuscript
Language: English

Restricted to Repository staff only
Contact us about this Publication
[thumbnail of draft.pdf]
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: Conference or workshop item (Proceeding)
DOI/Identification number: 10.1145/3180155.3180157
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 15 Jan 2018 17:50 UTC
Last Modified: 16 Feb 2021 13:52 UTC
Resource URI: (The current URI for this page, for reference purposes)
Lange, Julien:
  • Depositors only (login required):


Downloads per month over past year