{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:15Z","timestamp":1750220055252,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":11,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,2,23]],"date-time":"2023-02-23T00:00:00Z","timestamp":1677110400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"JSPS KAKENH","award":["JP19H04082"],"award-info":[{"award-number":["JP19H04082"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,2,23]]},"DOI":"10.1145\/3587828.3587835","type":"proceedings-article","created":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T15:40:57Z","timestamp":1687275657000},"page":"41-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Specification and Model Checking of Raft Leader Election in Maude*"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-3173-5273","authenticated-orcid":false,"given":"Takanori","family":"Ishibashi","sequence":"first","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4441-3259","authenticated-orcid":false,"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[{"name":"Japan Advanced Institute of Science and Technology, Japan"}]}],"member":"320","published-online":{"date-parts":[[2023,6,20]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 2014 USENIX conference on USENIX Annual Technical Conference (USENIX ATC'14). USENIX Association, USA, 305\u2013320","author":"Ongaro Diego","year":"2014","unstructured":"Diego Ongaro and John Ousterhout . 2014 . In search of an understandable consensus algorithm . In Proceedings of the 2014 USENIX conference on USENIX Annual Technical Conference (USENIX ATC'14). USENIX Association, USA, 305\u2013320 .\u3000https:\/\/dl.acm.org\/doi\/10.5555\/2643634.2643666 Diego Ongaro and John Ousterhout. 2014. In search of an understandable consensus algorithm. In Proceedings of the 2014 USENIX conference on USENIX Annual Technical Conference (USENIX ATC'14). USENIX Association, USA, 305\u2013320.\u3000https:\/\/dl.acm.org\/doi\/10.5555\/2643634.2643666"},{"unstructured":"etcd. [n.d.]. https:\/\/etcd.io.  etcd. [n.d.]. https:\/\/etcd.io.","key":"e_1_3_2_1_2_1"},{"unstructured":"CockroachDB. [n.d.]. https:\/\/github.com\/cockroachdb\/cockroach.  CockroachDB. [n.d.]. https:\/\/github.com\/cockroachdb\/cockroach.","key":"e_1_3_2_1_3_1"},{"unstructured":"YugabyteDB. [n.d.]. https:\/\/github.com\/yugabyte\/yugabyte-db.  YugabyteDB. [n.d.]. https:\/\/github.com\/yugabyte\/yugabyte-db.","key":"e_1_3_2_1_4_1"},{"unstructured":"TiKV. [n.d.]. https:\/\/github.com\/pingcap\/tidb.  TiKV. [n.d.]. https:\/\/github.com\/pingcap\/tidb.","key":"e_1_3_2_1_5_1"},{"volume-title":"Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2013. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions . Springer Science & Business Media . Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media.","key":"e_1_3_2_1_6_1"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude","author":"Clavel M.","year":"2007","unstructured":"M. Clavel , , Ed., All About Maude , ser. Lecture Notes in Computer Science . Springer , 2007 , vol. 4350 . M. Clavel, , Ed., All About Maude, ser. Lecture Notes in Computer Science. Springer, 2007, vol. 4350."},{"key":"e_1_3_2_1_8_1","first-page":"136","volume-title":"International Symposium on Formal Methods","author":"Chand Saksham","unstructured":"Saksham Chand , Yanhong A Liu , and Scott D Stoller . Formal verification of multi-paxos for distributed consensus . In International Symposium on Formal Methods , pages 119\u2013 136 . Springer, 2016. Saksham Chand, Yanhong A Liu, and Scott D Stoller. Formal verification of multi-paxos for distributed consensus. In International Symposium on Formal Methods, pages 119\u2013136. Springer, 2016."},{"key":"e_1_3_2_1_9_1","volume-title":"The TLA+ Language and Tools for Hardware and Software Engineers","author":"L.","year":"2002","unstructured":"Lamport, L. Specifying Systems , The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley , 2002 . Lamport, L. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002."},{"unstructured":"Diego Ongaro. 2014. Consensus: Bridging Theory and Practice. Ph.D. Dissertation. Stanford University. https:\/\/web.stanford.edu\/\u223couster\/cgi-bin\/papers\/OngaroPhD.pdf  Diego Ongaro. 2014. Consensus: Bridging Theory and Practice. Ph.D. Dissertation. Stanford University. https:\/\/web.stanford.edu\/\u223couster\/cgi-bin\/papers\/OngaroPhD.pdf","key":"e_1_3_2_1_10_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/2854065.2854081"}],"event":{"acronym":"ICSCA 2023","name":"ICSCA 2023: 2023 12th International Conference on Software and Computer Applications","location":"Kuantan Malaysia"},"container-title":["Proceedings of the 2023 12th International Conference on Software and Computer Applications"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587828.3587835","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3587828.3587835","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:27Z","timestamp":1750183707000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587828.3587835"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2,23]]},"references-count":11,"alternative-id":["10.1145\/3587828.3587835","10.1145\/3587828"],"URL":"https:\/\/doi.org\/10.1145\/3587828.3587835","relation":{},"subject":[],"published":{"date-parts":[[2023,2,23]]},"assertion":[{"value":"2023-06-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}