This HTML5 document contains 28 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n14https://kar.kent.ac.uk/id/eprint/80588#
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
n11http://purl.org/ontology/bibo/status/
dchttp://purl.org/dc/elements/1.1/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n6https://kar.kent.ac.uk/id/subject/
n16https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n3http://eprints.org/ontology/
n20https://kar.kent.ac.uk/id/event/
bibohttp://purl.org/ontology/bibo/
n8https://kar.kent.ac.uk/id/publication/
n7https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n13https://kar.kent.ac.uk/80588/
n4https://kar.kent.ac.uk/id/document/
n17https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n19https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n18https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:80588
rdf:type
bibo:Article bibo:AcademicArticle n3:ConferenceItemEPrint n3:EPrint
rdfs:seeAlso
n13:
n3:hasAccepted
n4:3204631
n3:hasDocument
n4:3204631 n4:3204632 n4:3204633 n4:3204634 n4:3204635 n4:3204636
dc:hasVersion
n4:3204631
dcterms:title
Bounded verification of message-passing concurrency in Go using Promela and Spin
wdrs:describedby
n16:export_kar_RDFN3.n3 n19:export_kar_RDFN3.n3
dcterms:date
2020-03-13
dcterms:creator
n18:ext-nd315@kent.ac.uk n18:ext-j.s.lange@kent.ac.uk
bibo:status
n11:forthcoming n11:peerReviewed
dcterms:publisher
n7:ext-48a99e52116852c9bda2a92bd703879a
bibo: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.
dcterms:isPartOf
n8:ext-e07db1c83b283e391ea4539c035701a2 n17:repository
dcterms:subject
n6:QA75
bibo:authorList
n14:authors
bibo:presentedAt
n20:ext-33d36f910ac7c01992ca4c829696a8af