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
[img]
Preview

Abstract

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: Faculties > Sciences > School of Computing
Depositing User: Julien Lange
Date Deposited: 23 Mar 2020 14:10 UTC
Last Modified: 24 Mar 2020 09:52 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/80588 (The current URI for this page, for reference purposes)
Lange, Julien: https://orcid.org/0000-0001-9697-1378
  • Depositors only (login required):

Downloads

Downloads per month over past year