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)

PDF - Publisher pdf

Creative Commons Licence
This work is licensed under a Creative Commons Attribution 4.0 International License.
Download (348kB) Preview
[img]
Preview
PDF - Author's Accepted Manuscript
Restricted to Repository staff only
Contact us about this Publication Download (398kB)
[img]
Official URL
https://dx.doi.org/10.1145/3180155.3180157

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 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: https://kar.kent.ac.uk/id/eprint/65587 (The current URI for this page, for reference purposes)
Lange, Julien: https://orcid.org/0000-0001-9697-1378
  • Depositors only (login required):

Downloads

Downloads per month over past year