{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T02:06:21Z","timestamp":1784167581344,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":44,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,6,2]],"date-time":"2016-06-02T00:00:00Z","timestamp":1464825600000},"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":[[2016,6,2]]},"DOI":"10.1145\/2908080.2908129","type":"proceedings-article","created":{"date-parts":[[2016,6,2]],"date-time":"2016-06-02T15:23:42Z","timestamp":1464881022000},"page":"599-613","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Cardinalities and universal quantifiers for verifying parameterized systems"],"prefix":"10.1145","author":[{"given":"Klaus v.","family":"Gleissenthall","sequence":"first","affiliation":[{"name":"TU Munich, Germany \/ University of California at San Diego, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrey","family":"Rybalchenko","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,6,2]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"CAV","author":"Abdulla P. A.","year":"2007","unstructured":"P. A. Abdulla , G. Delzanno , and A. Rezine . Parameterized verification of infinite-state processes with global conditions . In CAV , 2007 . P. A. Abdulla, G. Delzanno, and A. Rezine. Parameterized verification of infinite-state processes with global conditions. In CAV, 2007."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9323-7"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_6"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_39"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_45"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_9"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_8"},{"key":"e_1_3_2_1_8_1","volume-title":"VMCAI","author":"Bradley A. R.","year":"2006","unstructured":"A. R. Bradley , Z. Manna , and H. B. Sipma . What\u2019s decidable about arrays . In VMCAI , 2006 . A. R. Bradley, Z. Manna, and H. B. Sipma. What\u2019s decidable about arrays. In VMCAI, 2006."},{"key":"e_1_3_2_1_9_1","volume-title":"OSDI","author":"Burrows M.","year":"2006","unstructured":"M. Burrows . The chubby lock service for loosely-coupled distributed systems . In OSDI , 2006 . M. Burrows. The chubby lock service for loosely-coupled distributed systems. In OSDI, 2006."},{"key":"e_1_3_2_1_10_1","volume-title":"Distributed Computing","author":"Charron-Bost B.","year":"2009","unstructured":"B. Charron-Bost and A. Schiper . The heard-of model: computing in distributed systems with benign faults . Distributed Computing , 2009 . B. Charron-Bost and A. Schiper. The heard-of model: computing in distributed systems with benign faults. Distributed Computing, 2009."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54013-4_10"},{"key":"e_1_3_2_1_12_1","volume-title":"Liveness with invisible ranking. STTT, 8(3)","author":"Fang Y.","year":"2006","unstructured":"Y. Fang , N. Piterman , A. Pnueli , and L. D. Zuck . Liveness with invisible ranking. STTT, 8(3) , 2006 . Y. Fang, N. Piterman, A. Pnueli, and L. D. Zuck. Liveness with invisible ranking. STTT, 8(3), 2006."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103693"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535885"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677012"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603097"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_13"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254112"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328468"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480912"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_2_1_25_1","volume-title":"FM","author":"Hojjat H.","year":"2012","unstructured":"H. Hojjat , F. Konecn\u00fd , F. Garnier , R. Iosif , V. Kuncak , and P. R\u00fcmmer . A verification toolkit for numerical transition systems - tool paper . In FM , 2012 . H. Hojjat, F. Konecn\u00fd, F. Garnier, R. Iosif, V. Kuncak, and P. R\u00fcmmer. A verification toolkit for numerical transition systems - tool paper. In FM, 2012."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.169.6"},{"key":"e_1_3_2_1_27_1","volume-title":"USENIX","author":"Hunt P.","year":"2010","unstructured":"P. Hunt , M. Konar , F. P. Junqueira , and B. Reed . ZooKeeper: Waitfree coordination for Internet-scale systems . In USENIX , 2010 . P. Hunt, M. Konar, F. P. Junqueira, and B. Reed. ZooKeeper: Waitfree coordination for Internet-scale systems. In USENIX, 2010."},{"key":"e_1_3_2_1_28_1","volume-title":"CAV","author":"Kahsai T.","year":"2015","unstructured":"T. Kahsai , J. A. Navas , A. Gurfinkel , and A. Komuravelli . The SeaHorn verification framework . In CAV , 2015 . T. Kahsai, J. A. Navas, A. Gurfinkel, and A. Komuravelli. The SeaHorn verification framework. In CAV, 2015."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_11"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294267"},{"key":"e_1_3_2_1_31_1","volume-title":"Second-order SAT solving using program synthesis. CoRR, abs\/1409.4925","author":"Kroening D.","year":"2014","unstructured":"D. Kroening and M. Lewis . Second-order SAT solving using program synthesis. CoRR, abs\/1409.4925 , 2014 . D. Kroening and M. Lewis. Second-order SAT solving using program synthesis. CoRR, abs\/1409.4925, 2014."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_20"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_1_34_1","volume-title":"Mechanically checked safety proof of a byzantine Paxos algorithm","author":"Lamport L.","year":"2015","unstructured":"L. Lamport . Mechanically checked safety proof of a byzantine Paxos algorithm , 2015 . http:\/\/research.microsoft. com\/users\/lamport\/tla\/byzpaxos.html. Concurrent Garbage Collection. .NET Framework 4.6 and 4.5. Microsoft , 2015. L. Lamport. Mechanically checked safety proof of a byzantine Paxos algorithm, 2015. http:\/\/research.microsoft. com\/users\/lamport\/tla\/byzpaxos.html. Concurrent Garbage Collection. .NET Framework 4.6 and 4.5. Microsoft, 2015."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_13"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_2_1_37_1","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 , 2014 . D. Ongaro and J. Ousterhout. In search of an understandable consensus algorithm. In USENIX ATC, 2014."},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_11"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_12"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737964"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_25"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_10"},{"key":"e_1_3_2_1_43_1","volume-title":"CAV","author":"v. Gleissenthall K.","year":"2015","unstructured":"K. v. Gleissenthall , B. K\u00f6pf , and A. Rybalchenko . Symbolic polytopes for quantitative interpolation and verification . In CAV , 2015 . K. v. Gleissenthall, B. K\u00f6pf, and A. Rybalchenko. Symbolic polytopes for quantitative interpolation and verification. In CAV, 2015."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_27"}],"event":{"name":"PLDI '16: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Santa Barbara CA USA","acronym":"PLDI '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2908080.2908129","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2908080.2908129","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:54:50Z","timestamp":1750208090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2908080.2908129"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,6,2]]},"references-count":44,"alternative-id":["10.1145\/2908080.2908129","10.1145\/2908080"],"URL":"https:\/\/doi.org\/10.1145\/2908080.2908129","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2980983.2908129","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,6,2]]},"assertion":[{"value":"2016-06-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}