A Static Verification Framework for Message Passing in Go using Behavioural Types
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.
Conference DayFri 1 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30
|Programming Not Only by Example|
Technical PapersPre-print Media Attached
|Goal-Conflict Likelihood Assessment based on Model Counting|
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 AiresPre-print File Attached
|A Posteriori Typing for Model-Driven Engineering: Concepts, Analysis, and Applications|
Journal first papers
|A Static Verification Framework for Message Passing in Go using Behavioural Types|
Julien LangeUniversity of Kent, Nicholas NgImperial College London, Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College LondonDOI Pre-print Media Attached
|Q&A in groups|