{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T14:28:54Z","timestamp":1730298534875,"version":"3.28.0"},"reference-count":32,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,9,1]],"date-time":"2022-09-01T00:00:00Z","timestamp":1661990400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2022,9,1]],"date-time":"2022-09-01T00:00:00Z","timestamp":1661990400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62025202"],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,9]]},"DOI":"10.1109\/srds55811.2022.00018","type":"proceedings-article","created":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T16:53:56Z","timestamp":1672764836000},"page":"82-93","source":"Crossref","is-referenced-by-count":2,"title":["Compositional Model Checking of Consensus Protocols via Interaction-Preserving Abstraction"],"prefix":"10.1109","author":[{"given":"Xiaosong","family":"Gu","sequence":"first","affiliation":[{"name":"Nanjing University,State Key Laboratory for Novel Software Technology,Nanjing,China"}]},{"given":"Wei","family":"Cao","sequence":"additional","affiliation":[{"name":"Alibaba Group,Hangzhou,China"}]},{"given":"Yicong","family":"Zhu","sequence":"additional","affiliation":[{"name":"Alibaba Group,Hangzhou,China"}]},{"given":"Xuan","family":"Song","sequence":"additional","affiliation":[{"name":"Alibaba Group,Hangzhou,China"}]},{"given":"Yu","family":"Huang","sequence":"additional","affiliation":[{"name":"Nanjing University,State Key Laboratory for Novel Software Technology,Nanjing,China"}]},{"given":"Xiaoxing","family":"Ma","sequence":"additional","affiliation":[{"name":"Nanjing University,State Key Laboratory for Novel Software Technology,Nanjing,China"}]}],"member":"263","reference":[{"year":"0","key":"ref13"},{"key":"ref12","first-page":"399","article-title":"Samc: Semantic-aware model checking for fast discovery of deep bugs in cloud systems","author":"leesatapornwongsa","year":"2014","journal-title":"Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation"},{"year":"0","key":"ref15"},{"year":"0","key":"ref14"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043582"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035392"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.14778\/3229863.3229872"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/3360549"},{"key":"ref2","first-page":"305","article-title":"In search of an understandable consensus algorithm","author":"ongaro","year":"2014","journal-title":"Proceedings of the 2014 USENIX Conference on USENIX Annual Technical Conference"},{"key":"ref1","first-page":"51","article-title":"Paxos made simple","author":"lamport","year":"2001","journal-title":"ACM SIGACT News (Distributed Computing Column) 32 4 (Whole Number 121 December 2001)"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.21655\/ijsi.1673-7288.00257"},{"year":"0","key":"ref16"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.14778\/3397230.3397233"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_42"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.187"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"journal-title":"Transition from Global to Modular Temporal Reasoning about Programs","first-page":"123","year":"1989","author":"pnueli","key":"ref26"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39190"},{"journal-title":"Model checking","year":"2000","author":"clarke","key":"ref20"},{"journal-title":"Compositional model checking of consensus protocols specified in tla+ via interaction-preserving abstraction","year":"2022","author":"gu","key":"ref22"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028765"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211911"},{"key":"ref8","first-page":"251","article-title":"Spanner: Google's globally-distributed database","author":"corbett","year":"0","journal-title":"Proc OSDI'12 USENIX Symposium on Operating Systems Design and Implementation USENIX 2012"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/1281100.1281103"},{"journal-title":"Microsoft Azure Cosmos DB Revealed A Multi-Model Database Designed for the Cloud","year":"2018","author":"paz","key":"ref9"},{"key":"ref4","first-page":"145","article-title":"ZooKeeper: wait-free coordination for internet-scale systems","author":"hunt","year":"0","journal-title":"2010 USENIX Annual Technical Conference USENIX ATC'10"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2011.5958223"},{"key":"ref6","first-page":"335","article-title":"The Chubby lock service for loosely-coupled distributed systems","author":"burrows","year":"0","journal-title":"Proc OSDI'06 USENIX Symposium on Operating Systems Design and Implementation USENIX 2006"},{"year":"0","key":"ref5"}],"event":{"name":"2022 41st International Symposium on Reliable Distributed Systems (SRDS)","start":{"date-parts":[[2022,9,19]]},"location":"Vienna, Austria","end":{"date-parts":[[2022,9,22]]}},"container-title":["2022 41st International Symposium on Reliable Distributed Systems (SRDS)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9996590\/9996823\/09996903.pdf?arnumber=9996903","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T15:04:53Z","timestamp":1675091093000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9996903\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9]]},"references-count":32,"URL":"https:\/\/doi.org\/10.1109\/srds55811.2022.00018","relation":{},"subject":[],"published":{"date-parts":[[2022,9]]}}}