{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:36Z","timestamp":1772164056075,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":41,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,6,16]],"date-time":"2013-06-16T00:00:00Z","timestamp":1371340800000},"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":[[2013,6,16]]},"DOI":"10.1145\/2491956.2491969","type":"proceedings-article","created":{"date-parts":[[2013,6,11]],"date-time":"2013-06-11T12:03:50Z","timestamp":1370952230000},"page":"219-230","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Reasoning about nondeterminism in programs"],"prefix":"10.1145","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[{"name":"Microsoft Research Cambridge & University College London, Cambridge, United Kingdom"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"New York University, New York, NY, USA"}]}],"member":"320","published-online":{"date-parts":[[2013,6,16]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"142","volume-title":"CAV'94","author":"Bernholtz O.","year":"1994","unstructured":"Bernholtz , O. , Vardi , M. Y. , and Wolper , P . An automata-theoretic approach to branching-time model checking (extended abstract) . In CAV'94 ( 1994 ), D. L. Dill, Ed ., vol. 818 , Springer , pp. 142 -- 155 . Bernholtz, O., Vardi, M. Y., and Wolper, P. An automata-theoretic approach to branching-time model checking (extended abstract). In CAV'94 (1994), D. L. Dill, Ed., vol. 818, Springer, pp. 142--155."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11589976_5"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664590"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926431"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0153-5"},{"key":"e_1_3_2_1_11_1","first-page":"333","volume-title":"CAV'11","author":"Cook B.","year":"2011","unstructured":"Cook , B. , Koskinen , E. , and Vardi , M. Y . Temporal property verification as a program analysis task . In CAV'11 ( 2011 ), G. Gopalakrishnan and S. Qadeer, Eds ., vol. 6806 , Springer , pp. 333 -- 348 . Cook, B., Koskinen, E., and Vardi, M. Y. Temporal property verification as a program analysis task. In CAV'11 (2011), G. Gopalakrishnan and S. Qadeer, Eds., vol. 6806, Springer, pp. 333--348."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103687"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021870"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021854"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_3_2_1_17_1","first-page":"87","volume-title":"CAV'96","volume":"1102","author":"Emerson E. A.","year":"1996","unstructured":"Emerson , E. A. , and Namjoshi , K. S . Automatic verification of parameterized synchronous systems (extended abstract) . In CAV'96 ( 1996 ), vol. 1102 , pp. 87 -- 98 . Emerson, E. A., and Namjoshi, K. S. Automatic verification of parameterized synchronous systems (extended abstract). In CAV'96 (1996), vol. 1102, pp. 87--98."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_24"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328459"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_18"},{"key":"e_1_3_2_1_24_1","volume-title":"SAS","author":"Harris W. R.","year":"2010","unstructured":"Harris , W. R. , Lal , A. , Nori , A. V. , and Rajamani , S. K . Alternation for termination . In SAS ( 2010 ). Harris, W. R., Lal, A., Nori, A. V., and Rajamani, S. K. Alternation for termination. In SAS (2010)."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_22"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_47"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.023"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333987"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706326"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/69558.69559"},{"key":"e_1_3_2_1_32_1","volume-title":"IJCAI'01","author":"Pistore M.","year":"2001","unstructured":"Pistore , M. , and Traverso , P . Planning as model checking for extended goals in non-deterministic domains . In IJCAI'01 ( 2001 ), Springer . Pistore, M., and Traverso, P. Planning as model checking for extended goals in non-deterministic domains. In IJCAI'01 (2001), Springer."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_38"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_3_2_1_35_1","first-page":"404","volume-title":"ACM","author":"Solar-Lezama A.","unstructured":"Solar-Lezama , A. , Tancau , L. , Bod\u00edk , R. , Seshia , S. A. , and Saraswat , V. A . Combinatorial sketching for finite programs. In PLDI (2006) , ACM , pp. 404 -- 415 . Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S. A., and Saraswat, V. A. Combinatorial sketching for finite programs. In PLDI (2006), ACM, pp. 404--415."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_9"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646480.693772"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-006-0026-x"},{"key":"e_1_3_2_1_39_1","first-page":"62","volume-title":"CAV","volume":"1102","author":"Walukiewicz I.","year":"1996","unstructured":"Walukiewicz , I. Pushdown processes : Games and model checking . In CAV ( 1996 ), vol. 1102 , pp. 62 -- 74 . Walukiewicz, I. Pushdown processes: Games and model checking. In CAV (1996), vol. 1102, pp. 62--74."},{"key":"e_1_3_2_1_40_1","first-page":"127","volume-title":"FSTTCS","author":"Walukiewicz I.","year":"2000","unstructured":"Walukiewicz , I. Model checking ctl properties of pushdown systems . In FSTTCS ( 2000 ), S. Kapoor and S. Prasad , Eds ., vol. 1974 , pp. 127 -- 138 . Walukiewicz, I. Model checking ctl properties of pushdown systems. In FSTTCS (2000), S. Kapoor and S. Prasad, Eds., vol. 1974, pp. 127--138."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00255-7_22"}],"event":{"name":"PLDI '13: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Seattle Washington USA","acronym":"PLDI '13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2491969","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491956.2491969","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:39:10Z","timestamp":1750221550000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491956.2491969"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,16]]},"references-count":41,"alternative-id":["10.1145\/2491956.2491969","10.1145\/2491956"],"URL":"https:\/\/doi.org\/10.1145\/2491956.2491969","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2499370.2491969","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,6,16]]},"assertion":[{"value":"2013-06-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}