Bounded verification of message-passing concurrency in Go using Promela and Spin
This work addresses verification challenges for concurrent Go programs, particularly those with runtime uncertainties, offering a practical tool for developers, though it is incremental as it builds on prior methods.
The paper tackles the problem of verifying message-passing concurrency in Go programs with unknown parameters, such as variable thread counts or channel capacities, by developing a static verification framework that extracts over-approximated models encoded in Promela for efficient checking with Spin, achieving bounded verification with user-provided bounds.
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.