Skip to main content
Kent Academic Repository

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

Dilley, Nicolas, Lange, Julien (2010) Bounded verification of message-passing concurrency in Go using Promela and Spin. In: EPTCS. Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software. 314. pp. 34-45. EPTCS (doi:10.4204/EPTCS.314.4) (KAR id:80588)


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)
DOI/Identification number: 10.4204/EPTCS.314.4
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: 25 Apr 2022 15:37 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Dilley, Nicolas.

Creator's ORCID:
CReDIT Contributor Roles:

Lange, Julien.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.