Skip to main content

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

Dilley, Nicolas, Lange, Julien (2020) Bounded verification of message-passing concurrency in Go using Promela and Spin. In: PLACES 2020. . EPTCS (In press) (KAR id:80588)

PDF Author's Accepted Manuscript
Language: English
Download (410kB) Preview
[thumbnail of main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format


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.

Item Type: Conference or workshop item (Paper)
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 23 Mar 2020 14:10 UTC
Last Modified: 16 Feb 2021 14:12 UTC
Resource URI: (The current URI for this page, for reference purposes)
Lange, Julien:
  • Depositors only (login required):


Downloads per month over past year