Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/103347
Full metadata record
DC FieldValueLanguage
dc.contributor.authorDong, Jin Songen
dc.contributor.authorLiu, Yanhong A.en
dc.contributor.authorZhang, Shao Jieen
dc.contributor.authorSun, Junen
dc.contributor.authorLiu, Yangen
dc.contributor.authorChen, Weien
dc.date.accessioned2013-10-25T08:40:43Zen
dc.date.accessioned2019-12-06T21:10:35Z-
dc.date.available2013-10-25T08:40:43Zen
dc.date.available2019-12-06T21:10:35Z-
dc.date.copyright2013en
dc.date.issued2013en
dc.identifier.citationLiu, Y., Chen, W., Liu, Y. A., Sun, J., Zhang, S. J., & Dong, J. S. (2013).Verifying linearizability via optimized refinement checking. IEEE transactions on software engineering, 39(7), 1018-1039.en
dc.identifier.issn0098-5589en
dc.identifier.urihttps://hdl.handle.net/10356/103347-
dc.description.abstractLinearizability is an important correctness criterion for implementations of concurrent objects. Automatic checking of linearizability is challenging because it requires checking that: (1) All executions of concurrent operations are serializable, and (2) the serialized executions are correct with respect to the sequential semantics. In this work, we describe a method to automatically check linearizability based on refinement relations from abstract specifications to concrete implementations. The method does not require that linearization points in the implementations be given, which is often difficult or impossible. However, the method takes advantage of linearization points if they are given. The method is based on refinement checking of finite-state systems specified as concurrent processes with shared variables. To tackle state space explosion, we develop and apply symmetry reduction, dynamic partial order reduction, and a combination of both for refinement checking. We have built the method into the PAT model checker, and used PAT to automatically check a variety of implementations of concurrent objects, including the first algorithm for scalable nonzero indicators. Our system is able to find all known and injected bugs in these implementations.en
dc.language.isoenen
dc.relation.ispartofseriesIEEE transactions on software engineeringen
dc.subjectDRNTU::Engineering::Computer science and engineering::Softwareen
dc.titleVerifying linearizability via optimized refinement checkingen
dc.typeJournal Articleen
dc.contributor.schoolSchool of Computer Engineeringen
dc.identifier.doi10.1109/TSE.2012.82en
item.grantfulltextnone-
item.fulltextNo Fulltext-
Appears in Collections:SCSE Journal Articles

SCOPUSTM   
Citations 20

15
Updated on Jul 13, 2020

PublonsTM
Citations 20

11
Updated on Feb 3, 2021

Page view(s) 50

489
Updated on Aug 5, 2022

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.