Bounded verification of message-passing concurrency in Go using Promela and Spin

Nicolas Dilley
(University of Kent)
Julien Lange
(University of Kent)

This paper describes a static verification framework for the message-passing fragment of the Go programming language. Our framework extracts models that over-approximate the message-passing behaviour of a program. These models, or behavioural types, are encoded in Promela, hence can be efficiently verified with Spin. We improve on previous works by verifying programs that include communication-related parameters that are unknown at compile-time, i.e., programs that spawn a parameterised number of threads or that create channels with a parameterised capacity. These programs are checked via a bounded verification approach with bounds provided by the user.

In Stephanie Balzer and Luca Padovani: Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES 2020), Dublin, Ireland, 26th April 2020, Electronic Proceedings in Theoretical Computer Science 314, pp. 34–45.
Published: 3rd April 2020.

ArXived at: https://dx.doi.org/10.4204/EPTCS.314.4 Ancillary files bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org