{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T21:14:46Z","timestamp":1718054086909},"reference-count":48,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"12","license":[{"start":{"date-parts":[[2015,12,1]],"date-time":"2015-12-01T00:00:00Z","timestamp":1448928000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2015,12,1]]},"DOI":"10.1109\/tse.2015.2467371","type":"journal-article","created":{"date-parts":[[2015,8,13]],"date-time":"2015-08-13T22:41:33Z","timestamp":1439505693000},"page":"1202-1216","source":"Crossref","is-referenced-by-count":5,"title":["Round-Up: Runtime Verification of Quasi Linearizability for Concurrent Data Structures"],"prefix":"10.1109","volume":"41","author":[{"given":"Lu","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arijit","family":"Chattopadhyay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985824"},{"key":"ref38","first-page":"328","article-title":"Trace-based symbolic analysis for atomicity violations","author":"wang","year":"0","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_27"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.1599419"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168864"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065013"},{"key":"ref37","first-page":"279","article-title":"Automatic discovery of transition symmetry in multithreaded programs using dynamic analysis","author":"yang","year":"0","journal-title":"Proc International SPIN Workshop on Model Checking of Software"},{"key":"ref36","first-page":"256","article-title":"Symbolic predictive analysis for concurrent programs","author":"wang","year":"0","journal-title":"Proc Int Symp Formal Methods"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375618"},{"key":"ref34","first-page":"52","article-title":"Monitoring atomicity in concurrent programs","author":"farzan","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122992"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882301"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_21"},{"key":"ref12","first-page":"261","article-title":"Experience with model checking linearizability","author":"vechev","year":"0","journal-title":"Proc International SPIN Workshop on Model Checking of Software"},{"key":"ref13","first-page":"465","article-title":"Model checking of linearizability of concurrent list implementations","author":"cern\u00fd","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref14","first-page":"205","article-title":"LLVM: A low-level virtual instruction set architecture","author":"adve","year":"0","journal-title":"Proc of the ACM\/IEEE Int Symp on Microarchitecture"},{"key":"ref15","article-title":"Inspect: A runtime model checker for multithreaded C programs","author":"yang","year":"2008"},{"key":"ref16","first-page":"288","article-title":"Efficient stateful dynamic partial order reduction","author":"yang","year":"0","journal-title":"Proc 15th Int'l SPIN Workshop Model Checking Software"},{"key":"ref17","author":"salzburg","year":"2013"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806634"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693061"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2011.5970516"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/1993806.1993869"},{"key":"ref27","first-page":"315","article-title":"Causal atomicity","author":"farzan","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref3","first-page":"395","article-title":"Quasi-Linearizability: Relaxed consistency for improved concurrency","author":"afek","year":"0","journal-title":"Proc Int Conf Principles Distrib Syst"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228523"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964023"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33078-0_20"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/2482767.2482789"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429109"},{"key":"ref2","author":"herlihy","year":"2008","journal-title":"The Art of Multiprocessor Programming"},{"key":"ref9","first-page":"335","article-title":"Shape-value abstraction for verifying linearizability","author":"vafeiadis","year":"0","journal-title":"Proc Int Conf Verification Model Checking Abstract Interpretation"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/78969.78972"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_20"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0373-2"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001438"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2430536.2430542"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_1"},{"key":"ref47","first-page":"136","article-title":"Maximal causal models for sequentially consistent systems","author":"serbanuta","year":"0","journal-title":"Proc Int'l Conf Runtime Verification"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39176-7_3"},{"key":"ref42","first-page":"313","article-title":"Generating data race witnesses by an SMT-based analysis","author":"said","year":"0","journal-title":"Proc 3rd Int Conf NASA Formal Methods"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/185675.185815"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926433"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"ref44","first-page":"434","article-title":"Universal causality graphs: A precise happens-before model for detecting bugs in concurrent programs","author":"kahlon","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781169"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_2"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1435417.1435432"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/7349123\/07192659.pdf?arnumber=7192659","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:46:43Z","timestamp":1642006003000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7192659\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,1]]},"references-count":48,"journal-issue":{"issue":"12"},"URL":"https:\/\/doi.org\/10.1109\/tse.2015.2467371","relation":{},"ISSN":["0098-5589","1939-3520"],"issn-type":[{"value":"0098-5589","type":"print"},{"value":"1939-3520","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,1]]}}}