{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:16:02Z","timestamp":1784232962716,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":10,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,23]],"date-time":"2022-09-23T00:00:00Z","timestamp":1663891200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,9,23]]},"DOI":"10.1145\/3558819.3558822","type":"proceedings-article","created":{"date-parts":[[2022,10,27]],"date-time":"2022-10-27T01:37:33Z","timestamp":1666834653000},"page":"13-18","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Zookeeper based on Model-Based runtime Trace-Checking using TLA+"],"prefix":"10.1145","author":[{"given":"Zhi","family":"Niu","sequence":"first","affiliation":[{"name":"ZTE Corporation, China and \rState Key Laboratory of Mobile Network and Mobile Multimedia Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Luming","family":"Dong","sequence":"additional","affiliation":[{"name":"ZTE Corporation, China and \rState Key Laboratory of Mobile Network and Mobile Multimedia Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yong","family":"Zhu","sequence":"additional","affiliation":[{"name":"ZTE Corporation, China and \rState Key Laboratory of Mobile Network and Mobile Multimedia Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Li","family":"Chen","sequence":"additional","affiliation":[{"name":"ZTE Corporation, China and \rState Key Laboratory of Mobile Network and Mobile Multimedia Technology, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,26]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"search of an understandable consensus algorithm (extended version)","author":"Ongaro Diego","year":"2013","unstructured":"Diego Ongaro and John Ousterhout , \u201cIn search of an understandable consensus algorithm (extended version) \u201d, 2013 . Diego Ongaro and John Ousterhout, \u201cIn search of an understandable consensus algorithm (extended version)\u201d, 2013."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/501978.501980"},{"key":"e_1_3_2_1_3_1","volume-title":"France","author":"Kroening Daniel","year":"2014","unstructured":"Daniel Kroening , Michael Tautschnig . CBMC-C Bounded Model Checcker\/\/Springer. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , April 5-13, 2014, Grenoble , France . TACAS : Springer , 2014 : 389-391. Daniel Kroening, Michael Tautschnig.CBMC-C Bounded Model Checcker\/\/Springer.International Conference on Tools and Algorithms for the Construction and Analysis of Systems, April 5-13, 2014, Grenoble, France. TACAS: Springer, 2014: 389-391."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-020-0538-7"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.icte.2019.07.002"},{"key":"e_1_3_2_1_6_1","volume-title":"Semantic-based Automated Reasoning for AWS Access Policies using SMT\/\/IEEE. 2018 Formal Methods in Computer Aided Design, 30 Oct-2","author":"Backes John","year":"2018","unstructured":"John Backes , Pauline Bolignano , Byron Cook , Semantic-based Automated Reasoning for AWS Access Policies using SMT\/\/IEEE. 2018 Formal Methods in Computer Aided Design, 30 Oct-2 Nov , 2018 , Austin , TX, USA. NJ : IEEE , 2018: 9. John Backes, Pauline Bolignano, Byron Cook, Semantic-based Automated Reasoning for AWS Access Policies using SMT\/\/IEEE. 2018 Formal Methods in Computer Aided Design, 30 Oct-2 Nov, 2018, Austin, TX, USA. NJ: IEEE, 2018: 9."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_8"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-020-0538-7"},{"key":"e_1_3_2_1_10_1","volume-title":"Model-based trace-checking. CoRR, abs\/1111.2825","author":"Howard Y.","year":"2011","unstructured":"Y. Howard , Stefan Gruner , Andrew M. Gravell , Carla Ferreira , and Juan Carlos Augusto . Model-based trace-checking. CoRR, abs\/1111.2825 , 2011 . Y. Howard, Stefan Gruner, Andrew M. Gravell, Carla Ferreira, and Juan Carlos Augusto. Model-based trace-checking. CoRR, abs\/1111.2825, 2011."}],"event":{"name":"ICCSIE2022: 7th International Conference on Cyber Security and Information Engineering","location":"Brisbane QLD Australia","acronym":"ICCSIE2022"},"container-title":["Proceedings of the 7th International Conference on Cyber Security and Information Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3558819.3558822","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3558819.3558822","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:28Z","timestamp":1750186828000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3558819.3558822"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,23]]},"references-count":10,"alternative-id":["10.1145\/3558819.3558822","10.1145\/3558819"],"URL":"https:\/\/doi.org\/10.1145\/3558819.3558822","relation":{},"subject":[],"published":{"date-parts":[[2022,9,23]]},"assertion":[{"value":"2022-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}