Show simple item record

dc.contributor.authorLau, Sen
dc.contributor.authorGomes, VBFen
dc.contributor.authorMemarian, Kayvanen
dc.contributor.authorPichon-Pharabod, Jeanen
dc.contributor.authorSewell, Peteren
dc.date.accessioned2019-05-24T23:30:24Z
dc.date.available2019-05-24T23:30:24Z
dc.date.issued2019-01-01en
dc.identifier.isbn9783030255398en
dc.identifier.issn0302-9743
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/293121
dc.description.abstractC remains central to our infrastructure, making verification of C code an essential and much-researched topic, but the semantics of C is remarkably complex, and important aspects of it are still unsettled, leaving programmers and verification tool builders on shaky ground. This paper describes a tool, Cerberus-BMC, that for the first time provides a principled reference semantics that simultaneously supports (1) a choice of concurrency memory model (including substantial fragments of the C11, RC11, and Linux kernel memory models), (2) a modern memory object model, and (3) a well-validated thread-local semantics for a large fragment of the language. The tool should be useful for C programmers, compiler writers, verification tool builders, and members of the C/C++ standards committees.
dc.publisherSpringer Verlag
dc.rightsAttribution 4.0 International
dc.rights.urihttps://creativecommons.org/licenses/by/4.0/
dc.titleCerberus-BMC: A Principled Reference Semantics and Exploration Tool for Concurrent and Sequential Cen
dc.typeConference Object
prism.endingPage397
prism.publicationDate2019en
prism.publicationNameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en
prism.startingPage387
prism.volume11561 LNCSen
dc.identifier.doi10.17863/CAM.40269
dcterms.dateAccepted2019-04-16en
rioxxterms.versionofrecord10.1007/978-3-030-25540-4_22en
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2019-01-01en
dc.identifier.eissn1611-3349
rioxxterms.typeConference Paper/Proceeding/Abstracten
pubs.funder-project-idEPSRC (EP/K008528/1)
pubs.funder-project-idEuropean Commission Horizon 2020 (H2020) ERC (789108)
cam.orpheus.successThu Nov 05 11:53:59 GMT 2020 - The item has an open VoR version.*
rioxxterms.freetoread.startdate2100-01-01


Files in this item

Thumbnail
Thumbnail

This item appears in the following Collection(s)

Show simple item record

Attribution 4.0 International
Except where otherwise noted, this item's licence is described as Attribution 4.0 International