{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:13:33Z","timestamp":1784837613547,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":68,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["S11403,S11405,P27722,W1255-N23"],"award-info":[{"award-number":["S11403,S11405,P27722,W1255-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT15-103"],"award-info":[{"award-number":["ICT15-103"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009860","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"719-734","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms"],"prefix":"10.1145","author":[{"given":"Igor","family":"Konnov","sequence":"first","affiliation":[{"name":"Vienna University of Technology, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marijana","family":"Lazi\u0107","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Josef","family":"Widder","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"318","volume-title":"LNCS","author":"Abdulla P. A.","year":"1998","unstructured":"P. A. Abdulla , A. Bouajjani , and B. Jonsson . On-the-fly analysis of systems with unbounded, lossy FIFO channels. In CAV , LNCS , pages 305\u2013 318 , 1998 . P. A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy FIFO channels. In CAV, LNCS, pages 305\u2013318, 1998."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_6"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_19"},{"key":"e_1_3_2_1_5_1","volume-title":"Principles of model checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P. Katoen . Principles of model checking . MIT Press , 2008 . C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1416588.1416589"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2013.6575306"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2886151"},{"key":"e_1_3_2_1_10_1","first-page":"386","volume-title":"LNCS","author":"Bouajjani A.","year":"2004","unstructured":"A. Bouajjani , P. Habermehl , and T. Vojnar . Abstract regular model checking. In CAV , LNCS , pages 372\u2013 386 , 2004 . A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract regular model checking. In CAV, LNCS, pages 372\u2013386, 2004."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/4221.214134"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"crossref","unstructured":"F. V.\n      Brasileiro F.\n      Greve A.\n      Most\u00e9faoui and \n      M.\n      Raynal\n  . \n  Consensus in one communication step\n  . \n  In\n  PaCT volume \n  2127\n   of \n  LNCS pages 42\u2013\n  50 2001\n  .   F. V. Brasileiro F. Greve A. Most\u00e9faoui and M. Raynal. Consensus in one communication step. In PaCT volume 2127 of LNCS pages 42\u201350 2001.","DOI":"10.1007\/3-540-44743-1_4"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01108590"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/226643.226647"},{"key":"e_1_3_2_1_15_1","first-page":"273","article-title":"Formal verification of a consensus algorithm in the heard-of model","volume":"3","author":"Charron-Bost B.","year":"2009","unstructured":"B. Charron-Bost and S. Merz . Formal verification of a consensus algorithm in the heard-of model . IJSI , 3 (2\u20133): 273 \u2013 303 , 2009 . B. Charron-Bost and S. Merz. Formal verification of a consensus algorithm in the heard-of model. IJSI, 3(2\u20133):273\u2013303, 2009.","journal-title":"IJSI"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_12"},{"key":"e_1_3_2_1_17_1","volume-title":"Model Checking","author":"Clarke E.","year":"1999","unstructured":"E. Clarke , O. Grumberg , and D. Peled . Model Checking . MIT Press , 1999 . E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 1999."},{"key":"e_1_3_2_1_18_1","volume-title":"Springer","author":"Clarke E.","year":"2008","unstructured":"E. Clarke , M. Talupur , and H. Veith . Proving Ptolemy right: the environment abstraction framework for model checking concurrent systems. In TACAS\u201908\/ETAPS\u201908, pages 33\u201347 . Springer , 2008 . E. Clarke, M. Talupur, and H. Veith. Proving Ptolemy right: the environment abstraction framework for model checking concurrent systems. In TACAS\u201908\/ETAPS\u201908, pages 33\u201347. Springer, 2008."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646733.701301"},{"key":"e_1_3_2_1_20_1","series-title":"LNCS","first-page":"340","volume-title":"TACAS","author":"De Moura L.","unstructured":"L. De Moura and N. Bj\u00f8rner . Z3: An efficient SMT solver . In TACAS , volume 1579 of LNCS , pages 337\u2013 340 . 2008. L. De Moura and N. Bj\u00f8rner. Z3: An efficient SMT solver. In TACAS, volume 1579 of LNCS, pages 337\u2013340. 2008."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2006.55"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512965"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480885"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199468"},{"key":"e_1_3_2_1_27_1","first-page":"370","volume-title":"LICS","author":"Emerson E. A.","unstructured":"E. A. Emerson and V. Kahlon . Model checking guarded protocols . In LICS , pages 361\u2013 370 . IEEE, 2003. E. A. Emerson and V. Kahlon. Model checking guarded protocols. In LICS, pages 361\u2013370. IEEE, 2003."},{"key":"e_1_3_2_1_28_1","first-page":"359","volume-title":"LICS","author":"Esparza J.","unstructured":"J. Esparza , A. Finkel , and R. Mayr . On the verification of broadcast protocols . In LICS , pages 352\u2013 359 . IEEE Computer Society, 1999. J. Esparza, A. Finkel, and R. Mayr. On the verification of broadcast protocols. In LICS, pages 352\u2013359. IEEE Computer Society, 1999."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2953"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220880.3220973"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3149.214121"},{"key":"e_1_3_2_1_33_1","series-title":"LNCS","first-page":"331","volume-title":"TACAS","author":"Fisman D.","unstructured":"D. Fisman , O. Kupferman , and Y. Lustig . On verifying fault tolerance of distributed protocols . In TACAS , volume 4963 of LNCS , pages 315\u2013 331 . Springer, 2008. D. Fisman, O. Kupferman, and Y. Lustig. On verifying fault tolerance of distributed protocols. In TACAS, volume 4963 of LNCS, pages 315\u2013331. Springer, 2008."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2005.47"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07317-0_4"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s446-002-8027-4"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/1405716"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250755"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_6"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009860"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.006"},{"key":"e_1_3_2_1_45_1","first-page":"21","volume-title":"PSI","volume":"9609","author":"Konnov I.","year":"2015","unstructured":"I. Konnov , H. Veith , and J. Widder . What you always wanted to know about model checking of fault-tolerant distributed algorithms . In PSI 2015 , Revised Selected Papers , volume 9609 of LNCS, pages 6\u2013 21 . Springer, 2016. I. Konnov, H. Veith, and J. Widder. What you always wanted to know about model checking of fault-tolerant distributed algorithms. In PSI 2015, Revised Selected Papers, volume 9609 of LNCS, pages 6\u201321. Springer, 2016."},{"key":"e_1_3_2_1_46_1","series-title":"LNCS","first-page":"572","volume-title":"CAV","author":"Kroening D.","year":"2011","unstructured":"D. Kroening , J. Ouaknine , O. Strichman , T. Wahl , and J. Worrell . Linear completeness thresholds for bounded model checking . In CAV , volume 6806 of LNCS , pages 557\u2013 572 , 2011 . D. Kroening, J. Ouaknine, O. Strichman, T. Wahl, and J. Worrell. Linear completeness thresholds for bounded model checking. In CAV, volume 6806 of LNCS, pages 557\u2013572, 2011."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/FTCS.1993.627343"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289237"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2003.1209964"},{"key":"e_1_3_2_1_53_1","volume-title":"5 lessons we have learned using AWS","year":"2010","unstructured":"Netflix. 5 lessons we have learned using AWS . 2010 . Netflix. 5 lessons we have learned using AWS. 2010."},{"key":"e_1_3_2_1_54_1","unstructured":"retrieved on Nov. 7 2016. http:\/\/techblog.netflix.com\/2010\/ 12\/5-lessons-weve-learned-using-aws.html.  retrieved on Nov. 7 2016. http:\/\/techblog.netflix.com\/2010\/ 12\/5-lessons-weve-learned-using-aws.html."},{"key":"e_1_3_2_1_55_1","first-page":"320","volume-title":"USENIX ATC","author":"Ongaro D.","year":"2014","unstructured":"D. Ongaro and J. Ousterhout . In search of an understandable consensus algorithm . In USENIX ATC , pages 305\u2013 320 , 2014 . D. Ongaro and J. Ousterhout. In search of an understandable consensus algorithm. In USENIX ATC, pages 305\u2013320, 2014."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322188"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2016.23"},{"key":"e_1_3_2_1_59_1","first-page":"343","volume-title":"LNCS","author":"Pnueli A.","year":"2000","unstructured":"A. Pnueli and E. Shahar . Liveness and acceleration in parameterized verification. In CAV , LNCS , pages 328\u2013 343 , 2000 . A. Pnueli and E. Shahar. Liveness and acceleration in parameterized verification. In CAV, LNCS, pages 328\u2013343, 2000."},{"key":"e_1_3_2_1_60_1","series-title":"LNCS","first-page":"111","volume-title":"CAV","author":"Pnueli A.","unstructured":"A. Pnueli , J. Xu , and L. Zuck . Liveness with (0,1,\u221e)counter abstraction . In CAV , volume 2404 of LNCS , pages 93\u2013 111 . 2002. A. Pnueli, J. Xu, and L. Zuck. Liveness with (0,1,\u221e)counter abstraction. In CAV, volume 2404 of LNCS, pages 93\u2013111. 2002."},{"key":"e_1_3_2_1_61_1","first-page":"72","article-title":"Formal specification, verification, and implementation of fault-tolerant systems using EventML","author":"Rahli V.","year":"2015","unstructured":"V. Rahli , D. Guaspari , M. Bickford , and R. L. Constable . Formal specification, verification, and implementation of fault-tolerant systems using EventML . ECEASST , 72 , 2015 . V. Rahli, D. Guaspari, M. Bickford, and R. L. Constable. Formal specification, verification, and implementation of fault-tolerant systems using EventML. ECEASST, 72, 2015.","journal-title":"ECEASST"},{"key":"e_1_3_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/645431.652475"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.018"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87779-0_30"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01667080"},{"key":"e_1_3_2_1_66_1","unstructured":"TLA. TLA+ toolbox. http:\/\/research.microsoft.com\/en-us\/ um\/people\/lamport\/tla\/tools.html.  TLA. TLA+ toolbox. http:\/\/research.microsoft.com\/en-us\/ um\/people\/lamport\/tla\/tools.html."},{"key":"e_1_3_2_1_67_1","first-page":"331","volume-title":"LICS","author":"Vardi M. Y.","year":"1986","unstructured":"M. Y. Vardi and P. Wolper . An automata-theoretic approach to automatic program verification . In LICS , pages 322\u2013 331 , 1986 . M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS, pages 322\u2013331, 1986."},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908129"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009860","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009860","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:22Z","timestamp":1750203382000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009860"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":68,"alternative-id":["10.1145\/3009837.3009860","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009860","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009860","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}