Publication:
Reasoning about TSO programs using reduction and abstraction

Simple item page
dc.conference.dateJUL 14-17, 2018
dc.conference.locationOxford, England
dc.conference.organizer30th International Conference on Computer-Aided Verification (CAV) Held as Part of the Federated Logic Conference (FloC)
dc.contributor.coauthorBouajjani, Ahmed
dc.contributor.coauthorEnea, Constantin
dc.contributor.coauthorTasiran, Serdar
dc.contributor.departmentGraduate School of Sciences and Engineering
dc.contributor.facultymemberNo
dc.contributor.kuauthorMutluergil, Süha Orhun
dc.contributor.schoolcollegeinstituteGRADUATE SCHOOL OF SCIENCES AND ENGINEERING
dc.date.accessioned2024-11-09T23:37:16Z
dc.date.issued2018
dc.description.abstractWe present a method for proving that a program running under the Total Store Ordering (TSO) memory model is robust, i.e., all its TSO computations are equivalent to computations under the Sequential Consistency (SC) semantics. This method is inspired by Lipton's reduction theory for proving atomicity of concurrent programs. For programs which are not robust, we introduce an abstraction mechanism that allows to construct robust programs over-approximating their TSO semantics. This enables the use of proof methods designed for the SC semantics in proving invariants that hold on the TSO semantics of a non-robust program. These techniques have been evaluated on a large set of benchmarks using the infrastructure provided by CIVL, a generic tool for reasoning about concurrent programs under the SC semantics.
dc.description.fulltextNo
dc.description.harvestedfromManual
dc.description.indexedbyWOS
dc.description.indexedbyScopus
dc.description.openaccessYES
dc.description.peerreviewstatusN/A
dc.description.publisherscopeInternational
dc.description.readpublishN/A
dc.description.sponsoredbyTubitakEuEU
dc.description.sponsorshipEuropean Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme [678177] This work is supported in part by the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (grant agreement No. 678177).
dc.description.studentonlypublicationYes
dc.description.studentpublicationYes
dc.description.versionN/A
dc.identifier.WoSQuartileQ4
dc.identifier.doi10.1007/978-3-319-96142-2_21
dc.identifier.eissn1611-3349
dc.identifier.embargoN/A
dc.identifier.endpage353
dc.identifier.grantno678177
dc.identifier.isbn9783319961422
dc.identifier.isbn9783319961415
dc.identifier.issn0302-9743
dc.identifier.scopus2-s2.0-85051145992
dc.identifier.startpage336
dc.identifier.urihttps://doi.org/10.1007/978-3-319-96142-2_21
dc.identifier.urihttps://hdl.handle.net/20.500.14288/12786
dc.identifier.volume10982
dc.identifier.wos000491469700021
dc.keywordsMemory
dc.keywordsVerification
dc.keywordsAbstracting
dc.keywordsComputer aided analysis
dc.keywordsSemantics
dc.language.isoeng
dc.publisherSpringer
dc.relation.affiliationKoç University
dc.relation.collectionKoç University Institutional Repository
dc.relation.ispartofComputer Aided Verification, CAV 2018, PT II
dc.relation.openaccessN/A
dc.rightsN/A
dc.subjectComputer science
dc.subjectSoftware engineering
dc.subjectComputer science
dc.titleReasoning about TSO programs using reduction and abstraction
dc.typeConference Proceeding
dspace.entity.typePublication
local.contributor.kuauthorMutluergil, Süha Orhun
relation.isOrgUnitOfPublication3fc31c89-e803-4eb1-af6b-6258bc42c3d8
relation.isOrgUnitOfPublication.latestForDiscovery3fc31c89-e803-4eb1-af6b-6258bc42c3d8
relation.isParentOrgUnitOfPublication434c9663-2b11-4e66-9399-c863e2ebae43
relation.isParentOrgUnitOfPublication.latestForDiscovery434c9663-2b11-4e66-9399-c863e2ebae43

Files

Collections

Publications without Fulltext