* 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 Chair(s): Jon Whittle

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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Models and Modeling IITechnical Papers / Journal first papers at G1 room
Chair(s): Jon WhittleMonash University
14:00
20m
Talk
Programming Not Only by Example
Technical Papers
Hila PelegTechnion, Israel, Sharon ShohamTel Aviv university, Eran YahavTechnion
Pre-print Media Attached
14:20
20m
Talk
Goal-Conflict Likelihood Assessment based on Model Counting
Technical Papers
Renzo DegiovanniUniversidad Nacional de Río Cuarto, Pablo Castro, Marcelo Arroyo, Marcelo RuizDept. of Mathematics, FCEFQyN, University of Río Cuarto, Argentina , Nazareno AguirreDept. of Computer Science FCEFQyN, University of Rio Cuarto, Marcelo F. FriasDept. of Software Engineering Instituto Tecnológico de Buenos Aires
Pre-print File Attached
14:40
20m
Talk
A Posteriori Typing for Model-Driven Engineering: Concepts, Analysis, and Applications
Journal first papers
15:00
20m
Talk
A Static Verification Framework for Message Passing in Go using Behavioural Types
Technical Papers
Julien LangeUniversity of Kent, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London
DOI Pre-print Media Attached
15:20
10m
Talk
Q&A in groups
Technical Papers