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

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Bounded verification of message-passing concurrency in Go using Promela and Spin Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:AcademicArticle, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/ConferenceItemEPrint http://eprints.org/ontology/EPrint Article Academic Article
seeAlso	HTML Summary of #80588 Bounded verification of message-passing concurrency in Go using Promela and Spin
http://eprints.org/ontology/hasAccepted	Bounded verification of message-passing concurrency in Go using Promela and Spin (PDF)
http://eprints.org/ontology/hasDocument	Bounded verification of message-passing concurrency in Go using Promela and Spin (PDF) Bounded verification of message-passing concurrency in Go using Promela and Spin (Other) Bounded verification of message-passing concurrency in Go using Promela and Spin (Other) Bounded verification of message-passing concurrency in Go using Promela and Spin (Other) Bounded verification of message-passing concurrency in Go using Promela and Spin (Other) Bounded verification of message-passing concurrency in Go using Promela and Spin (Other)
dc:hasVersion	Bounded verification of message-passing concurrency in Go using Promela and Spin (PDF)
Title	Bounded verification of message-passing concurrency in Go using Promela and Spin
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3
Date	2020-03-13
Creator	Julien Lange Nicolas Dilley
status	forthcoming peer reviewed
Publisher	EPTCS
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.
Is Part Of	PLACES 2020 https://kar.kent.ac.uk/id/repository
Subject	QA 75 Electronic computers. Computer science
list of authors	https://kar.kent.ac.uk/id/eprint/80588#authors
presented at	12th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric Software
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #80588 Bounded verification of message-passing concurrency in Go using Promela and Spin

Faceted Search & Find service v1.17_git149 as of Dec 03 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 29 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software