{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T04:27:45Z","timestamp":1743049665516,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030242954"},{"type":"electronic","value":"9783030242961"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24296-1_43","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:06:36Z","timestamp":1561755996000},"page":"546-555","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Methods of Formal Software Verification in the Context of Distributed Systems"],"prefix":"10.1007","author":[{"given":"Anna","family":"Fatkina","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Iakushkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dmitry","family":"Selivanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Korkhov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"key":"43_CR1","unstructured":"Proof General. A generic Emacs interface for proof assistants. \n                      https:\/\/proofgeneral.github.io\/\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR2","unstructured":"Leslie Lamport: The TLA+ Toolbox. \n                      https:\/\/lamport.azurewebsites.net\/tla\/toolbox.html\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR3","unstructured":"Verdi. Formally Verifying Distributed Systems. \n                      http:\/\/verdi.uwplse.org\/\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR4","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming With Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant","author":"A Chlipala","year":"2013","unstructured":"Chlipala, A.: Certified Programming With Dependent Types: A Pragmatic Introduction to the Coq Proof Assistant. MIT Press, Cambridge (2013)"},{"key":"43_CR5","unstructured":"The Coq Proof Assistant. \n                      https:\/\/coq.inria.fr\/\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR6","unstructured":"Coq Tactics Cheatsheet. \n                      https:\/\/www.cs.cornell.edu\/courses\/cs3110\/2017fa\/a5\/coq-tactics-cheatsheet.html\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR7","unstructured":"Coq Tactic Index. \n                      https:\/\/coq.inria.fr\/distrib\/current\/refman\/coq-tacindex.html\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR8","unstructured":"The Isabelle development team. Isabelle. \n                      https:\/\/isabelle.in.tum.de\/\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR9","unstructured":"Paulson, T.N.L.C., Wenzel, M.: A Proof Assistant for Higher-Order Logic (2013). \n                      http:\/\/isabelle.in.tum.de"},{"key":"43_CR10","unstructured":"Isabelle Archive of Formal Proofs. \n                      https:\/\/www.isa-afp.org\/\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR11","unstructured":"Yushkovskiy, A., Tripakis, S.: Comparison of Two Theorem Provers: Isabelle\/HOL and Coq (2018)"},{"key":"43_CR12","unstructured":"Palmskog, K., Gligoric, M., Pe\u00f1a, L., Moore, B., Rosu, G.: Verification of Casper in the Coq Proof Assistant (2018)"},{"key":"43_CR13","unstructured":"PoS related formal methods. \n                      https:\/\/github.com\/palmskog\/pos\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR14","doi-asserted-by":"crossref","unstructured":"Woos, D., Wilcox, J.R., Anton, S., Tatlock, Z., Ernst, M.D., Anderson, T.: Planning for change in a formal verification of the raft consensus protocol. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 154\u2013165. ACM (2016)","DOI":"10.1145\/2854065.2854081"},{"key":"43_CR15","unstructured":"Ongaro, D., Ousterhout, J.: In search of an understandable consensus algorithm. In: 2014 USENIX Annual Technical Conference (USENIXATC 2014), pp. 305\u2013319 (2014)"},{"key":"43_CR16","unstructured":"TLA+ User Guide. \n                      https:\/\/learntla.com\/tla\/\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR17","doi-asserted-by":"crossref","unstructured":"P\u00eerlea, G., Sergey, I.: Mechanising blockchain consensus. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 78\u201390. ACM (2018)","DOI":"10.1145\/3167086"},{"key":"43_CR18","doi-asserted-by":"crossref","unstructured":"Charapko, A., Ailijiang, A., Demirbas, M.: Bridging Paxos and Blockchain Consensus (2018)","DOI":"10.1109\/Cybermatics_2018.2018.00260"},{"key":"43_CR19","doi-asserted-by":"publisher","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in Isabelle\/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018), pp. 66\u201377. ACM, New York (2018). \n                      https:\/\/doi.org\/10.1145\/3167084","DOI":"10.1145\/3167084"},{"key":"43_CR20","unstructured":"Verdi GitHub repository. \n                      https:\/\/github.com\/uwplse\/verdi\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR21","unstructured":"Verdi Runtime library repository. \n                      https:\/\/github.com\/DistributedComponents\/verdi-runtime\n                      \n                    . Accessed 20 Mar 2019"},{"key":"43_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1007\/978-3-319-89884-1_22","volume-title":"Programming Languages and Systems","author":"V Rahli","year":"2018","unstructured":"Rahli, V., Vukotic, I., V\u00f6lp, M., Esteves-Verissimo, P.: Velisarios: Byzantine fault-tolerant protocols powered by Coq. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 619\u2013650. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89884-1_22"},{"key":"43_CR23","unstructured":"Vukotic, I.: An Ecosystem for Verifying Implementations of BFT Protocols (2018)"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24296-1_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T22:20:12Z","timestamp":1561760412000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24296-1_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242954","9783030242961"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24296-1_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICCSA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computational Science and Its Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Saint Petersburg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Russia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"iccsa2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.iccsa.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}