ICSE 2018
Sun 27 May - Sun 3 June 2018 Gothenburg, Sweden
Fri 1 Jun 2018 15:00 - 15:20 at G1 room - Models and Modeling II

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.

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.

Fri 1 Jun

14:00 - 15:30: Technical Papers - Models and Modeling II at G1 room
icse-2018-Technical-Papers152785440000014:00 - 14:20
icse-2018-Technical-Papers152785560000014:20 - 14:40
icse-2018-Technical-Papers152785680000014:40 - 15:00
icse-2018-Technical-Papers152785800000015:00 - 15:20
icse-2018-Technical-Papers152785920000015:20 - 15:30