{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:11:01Z","timestamp":1742980261069,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030670665"},{"type":"electronic","value":"9783030670672"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-67067-2_10","type":"book-chapter","created":{"date-parts":[[2021,1,11]],"date-time":"2021-01-11T20:57:20Z","timestamp":1610398640000},"page":"196-218","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Eliminating Message Counters in Synchronous Threshold Automata"],"prefix":"10.1007","author":[{"given":"Ilina","family":"Stoilkovska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Konnov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,1,12]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-73721-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Aminof","year":"2018","unstructured":"Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., Zuleger, F.: Parameterized model checking of synchronous distributed algorithms by abstraction. VMCAI 2018. LNCS, vol. 10747, pp. 1\u201324. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_1"},{"key":"10_CR2","doi-asserted-by":"publisher","DOI":"10.1002\/0471478210","volume-title":"Distributed Computing","author":"H Attiya","year":"2004","unstructured":"Attiya, H., Welch, J.: Distributed Computing, 2nd edn. Wiley, Hoboken (2004)","edition":"2"},{"key":"10_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MITP, United States (2008)"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Bakst, A., von Gleissenthall, K., Kici, R.G., Jhala, R.: Verifying distributed programs via canonical sequentialization. PACMPL 1(OOPSLA), 1\u201327 (2017)","DOI":"10.1145\/3133934"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Balasubramanian, A.R., Esparza, J., Lazi\u0107, M.: Complexity of verification and synthesis of threshold automata. In: ATVA (2020)","DOI":"10.1007\/978-3-030-59152-6_8"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Berman, P., Garay, J.A., Perry, K.J.: Asymptotically Optimal Distributed Consensus. Technical report, Bell Labs (1989). http:\/\/plan9.bell-labs.co\/who\/garay\/asopt.ps","DOI":"10.1109\/SFCS.1989.63511"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Berman, P., Garay, J.A., Perry, K.J.: Towards optimal distributed consensus (Extended Abstract). In: FOCS, pp. 410\u2013415 (1989)","DOI":"10.1109\/SFCS.1989.63511"},{"key":"10_CR8","unstructured":"Bertrand, N., Konnov, I., Lazi\u0107, M., Widder, J.: Verification of randomized consensus algorithms under round-rigid adversaries. In: CONCUR, pp. 1\u201315 (2019)"},{"issue":"40","key":"10_CR9","doi-asserted-by":"publisher","first-page":"5602","DOI":"10.1016\/j.tcs.2010.09.032","volume":"412","author":"M Biely","year":"2011","unstructured":"Biely, M., Schmid, U., Weiss, B.: Synchronous consensus under hybrid process and link failures. Theor. Comput. Sci. 412(40), 5602\u20135630 (2011)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-642-14203-1_27","volume-title":"Automated Reasoning","author":"N Bj\u00f8rner","year":"2010","unstructured":"Bj\u00f8rner, N.: Linear quantifier elimination as an abstract decision procedure. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 316\u2013330. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_27"},{"key":"10_CR11","first-page":"15","volume":"35","author":"N Bj\u00f8rner","year":"2015","unstructured":"Bj\u00f8rner, N., Janota, M.: Playing with quantified satisfaction. LPAR 35, 15\u201327 (2015)","journal-title":"LPAR"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-319-96142-2_23","volume-title":"Computer Aided Verification","author":"A Bouajjani","year":"2018","unstructured":"Bouajjani, A., Enea, C., Ji, K., Qadeer, S.: On the completeness of verifying message passing programs under bounded asynchrony. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 372\u2013391. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_23"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-04420-5_10","volume-title":"Reachability Problems","author":"M Chaouch-Saad","year":"2009","unstructured":"Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 93\u2013106. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04420-5_10"},{"issue":"91\u201399","key":"10_CR14","first-page":"300","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7(91\u201399), 300 (1972)","journal-title":"Mach. Intell."},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-030-25543-5_20","volume-title":"Computer Aided Verification","author":"A Damian","year":"2019","unstructured":"Damian, A., Dr\u0103goi, C., Militaru, A., Widder, J.: Communication-closed asynchronous protocols. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 344\u2013363. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_20"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-54013-4_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Dr\u0103goi","year":"2014","unstructured":"Dr\u0103goi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 161\u2013181. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_10"},{"issue":"2","key":"10_CR18","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"MJ Fischer","year":"1985","unstructured":"Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"10_CR19","unstructured":"Gleissenthall, K.V., G\u00f6khan Kici, R., Bakst, A., Stefan, D., Jhala, R.: Pretend synchrony. In: POPL (2019)"},{"issue":"7","key":"10_CR20","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/3068608","volume":"60","author":"C Hawblitzel","year":"2017","unstructured":"Hawblitzel, C., et al.: Ironfleet: proving safety and liveness of practical distributed systemsp. Commun. ACM 60(7), 83\u201392 (2017)","journal-title":"Commun. ACM"},{"issue":"3","key":"10_CR21","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/28869.28876","volume":"34","author":"TK Srikanth","year":"1987","unstructured":"Srikanth, T.K., Toueg, S.: Optimal clock synchronization. J. ACM 34(3), 626\u2013645 (1987)","journal-title":"J. ACM"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Konnov, I., Lazi\u0107, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL, pp. 719\u2013734 (2017)","DOI":"10.1145\/3093333.3009860"},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.ic.2016.03.006","volume":"252","author":"I Konnov","year":"2017","unstructured":"Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. Inf. Comput. 252, 95\u2013109 (2017). https:\/\/doi.org\/10.1016\/j.ic.2016.03.006","journal-title":"Inf. Comput."},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/2.248873","volume":"27","author":"H Kopetz","year":"1994","unstructured":"Kopetz, H., Gr\u00fcnsteidl, G.: TTP - a protocol for fault-tolerant real-time systems. IEEE Comput. 27(1), 14\u201323 (1994). https:\/\/doi.org\/10.1109\/2.248873","journal-title":"IEEE Comput."},{"key":"10_CR25","unstructured":"Kragl, B., Qadeer, S., Henzinger, T.A.: Synchronizing the asynchronous. In: CONCUR, pp. 1\u201317 (2018)"},{"key":"10_CR26","unstructured":"Kukovec, J., Konnov, I., Widder, J.: Reachability in parameterized systems: all flavors of threshold automata. In: CONCUR. LIPIcs, vol. 118, pp. 1\u201317 (2018)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Lincoln, P., Rushby, J.: A formally verified algorithm for interactive consistency under a hybrid fault model. In: FTCS, pp. 402\u2013411 (1993)","DOI":"10.1007\/3-540-56922-7_24"},{"key":"10_CR28","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufman (1996)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-63390-9_12","volume-title":"Computer Aided Verification","author":"O Mari\u0107","year":"2017","unstructured":"Mari\u0107, O., Sprenger, C., Basin, D.: Cutoff bounds for consensus algorithms. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 217\u2013237. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_12"},{"key":"10_CR30","unstructured":"Presburger, M.: \u00dcber die vollst\u00e4ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. Comptes Rendus du I congres de Math\u00e9maticiens des Pays Slaves, pp. 92\u2013101 (1929)"},{"issue":"8","key":"10_CR31","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/135226.135233","volume":"35","author":"W Pugh","year":"1992","unstructured":"Pugh, W.: A practical algorithm for exact array dependence analysis. Commun. ACM 35(8), 102\u2013114 (1992)","journal-title":"Commun. ACM"},{"key":"10_CR32","unstructured":"Rahli, V., Guaspari, D., Bickford, M., Constable, R.L.: Formal specification, verification, and implementation of fault-tolerant systems using EventML. ECEASST 72 (2015)"},{"issue":"1","key":"10_CR33","first-page":"1","volume":"1","author":"M Raynal","year":"2010","unstructured":"Raynal, M.: Fault-tolerant agreement in synchronous message-passing systems. Synth. Lect. Distrib. Comput. Theory 1(1), 1\u2013189 (2010)","journal-title":"Synth. Lect. Distrib. Comput. Theory"},{"key":"10_CR34","unstructured":"Stoilkovska, I.: Manually Encoded Synchronous Threshold Automata. https:\/\/github.com\/istoilkovska\/syncTA\/algorithms. Accessed Oct 2020"},{"key":"10_CR35","unstructured":"Stoilkovska, I.: Receive Synchronous Threshold Automata. https:\/\/github.com\/istoilkovska\/syncTA\/receiveSTA. Accessed Oct 2020"},{"key":"10_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-030-17465-1_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"I Stoilkovska","year":"2019","unstructured":"Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Verifying safety of synchronous fault-tolerant algorithms by bounded model checking. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 357\u2013374. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_20"},{"key":"10_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-030-59152-6_11","volume-title":"Automated Technology for Verification and Analysis","author":"I Stoilkovska","year":"2020","unstructured":"Stoilkovska, I., Konnov, I., Widder, J., Zuleger, F.: Eliminating message counters in threshold automata. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 196\u2013212. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_11"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Wilcox, J.R., et al.: Verdi: a framework for implementing and formally verifying distributed systems. In: PLDI, pp. 357\u2013368 (2015)","DOI":"10.1145\/2813885.2737958"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67067-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T20:10:50Z","timestamp":1718050250000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-67067-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030670665","9783030670672"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67067-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"12 January 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Copenhagen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Denmark","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 January 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 January 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl21.sigplan.org\/home\/VMCAI-2021","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"48","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3,1","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4,6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference took place virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}