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 this file
(PDF/313kB)
[thumbnail of p1137-lange.pdf]
Preview
Request a format suitable for use with assistive technology e.g. a screenreader
PDF Author's Accepted Manuscript
Language: English

Restricted to Repository staff only
Contact us about this Publication
[thumbnail of draft.pdf]
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: 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: 13 Jan 2024 15:45 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/65587 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.