Show simple item record

dc.contributor.authorLau, S
dc.contributor.authorGomes, VBF
dc.contributor.authorMemarian, K
dc.contributor.authorPichon-Pharabod, J
dc.contributor.authorSewell, P
dc.date.accessioned2019-05-24T23:30:24Z
dc.date.available2019-05-24T23:30:24Z
dc.date.issued2019
dc.identifier.isbn9783030255398
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 International Publishing
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 C
dc.typeConference Object
prism.endingPage397
prism.publicationDate2019
prism.publicationNameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
prism.startingPage387
prism.volume11561 LNCS
dc.identifier.doi10.17863/CAM.40269
dcterms.dateAccepted2019-04-16
rioxxterms.versionofrecord10.1007/978-3-030-25540-4_22
rioxxterms.versionVoR
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserved
rioxxterms.licenseref.startdate2019-01-01
dc.contributor.orcidMemarian, Kayvan [0000-0003-3723-636X]
dc.contributor.orcidSewell, Peter [0000-0001-9352-1013]
dc.identifier.eissn1611-3349
rioxxterms.typeConference Paper/Proceeding/Abstract
pubs.funder-project-idEngineering and Physical Sciences Research Council (EP/K008528/1)
pubs.funder-project-idEuropean Research Council (789108)
cam.issuedOnline2019-07-12
pubs.conference-nameCAV 2019: Proc. 31st International Conference on Computer-Aided Verification
pubs.conference-start-date2019-07-15
cam.orpheus.successThu Nov 05 11:53:59 GMT 2020 - The item has an open VoR version.
pubs.conference-finish-date2019-07-18
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