{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:38Z","timestamp":1772163998590,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":42,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,1,26]],"date-time":"2011-01-26T00:00:00Z","timestamp":1296000000000},"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":[[2011,1,26]]},"DOI":"10.1145\/1926385.1926431","type":"proceedings-article","created":{"date-parts":[[2011,1,24]],"date-time":"2011-01-24T09:58:22Z","timestamp":1295863102000},"page":"399-410","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Making prophecies with decision predicates"],"prefix":"10.1145","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[{"name":"Microsoft Research & Queen Mary, University of London, Cambridge, United Kingdom"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2011,1,26]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"Cadence SMV. http:\/\/www.kenmcmil.com\/smv.html.  Cadence SMV. http:\/\/www.kenmcmil.com\/smv.html."},{"key":"e_1_3_2_2_2_1","unstructured":"The Z3 Theorem Prover. research.microsoft.com\/projects\/Z3.  The Z3 Theorem Prover. research.microsoft.com\/projects\/Z3."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_2_4_1","volume-title":"CAV","author":"Abdulla P. A.","year":"2004","unstructured":"Abdulla , P. A. , Jonsson , B. , Nilsson , M. , d' Orso , J. , and Saksena , M . Regular model checking for LTL(MSO) . In CAV ( 2004 ). Abdulla, P. A., Jonsson, B., Nilsson, M., d'Orso, J., and Saksena, M. Regular model checking for LTL(MSO). In CAV (2004)."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1218063.1217943"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.02.061"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_2_12_1","volume-title":"Model checking","author":"Clarke E.","year":"1999","unstructured":"Clarke , E. , Grumberg , O. , and Peled , D . Model checking . Springer , 1999 . Clarke, E., Grumberg, O., and Peled, D. Model checking. Springer, 1999."},{"key":"e_1_3_2_2_13_1","volume-title":"LICS","author":"Clarke E.","year":"2002","unstructured":"Clarke , E. , Jha , S. , Lu , Y. , and Veith , H . Tree-like counterexamples in model checking . In LICS ( 2002 ). Clarke, E., Jha, S., Lu, Y., and Veith, H. Tree-like counterexamples in model checking. In LICS (2002)."},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008615614281"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134029"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_11"},{"key":"e_1_3_2_2_21_1","volume-title":"TACS","author":"Esparza J.","year":"2001","unstructured":"Esparza , J. , Kucera , A. , and Schwoon , S . Model-checking LTL with regular valuations for pushdown systems . In TACS ( 2001 ). Esparza, J., Kucera, A., and Schwoon, S. Model-checking LTL with regular valuations for pushdown systems. In TACS (2001)."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0193-x"},{"key":"e_1_3_2_2_23_1","volume-title":"Uber die theorie der einfachen ungleichungen. Journal fur die Reine und Angewandte Mathematik 124","author":"Farkas J.","year":"1902","unstructured":"Farkas , J. Uber die theorie der einfachen ungleichungen. Journal fur die Reine und Angewandte Mathematik 124 ( 1902 ), 1--27. Farkas, J. Uber die theorie der einfachen ungleichungen. Journal fur die Reine und Angewandte Mathematik 124 (1902), 1--27."},{"key":"e_1_3_2_2_24_1","volume-title":"CAV (July","author":"Gastin P.","year":"2001","unstructured":"Gastin , P. , and Oddoux , D . Fast LTL to B\u00fcchi automata translation . In CAV (July 2001 ). Gastin, P., and Oddoux, D. Fast LTL to B\u00fcchi automata translation. In CAV (July 2001)."},{"key":"e_1_3_2_2_25_1","volume-title":"International Journal on Software Tools for Technology Transfer (STTT) 2, 4","author":"Havelund K.","year":"2000","unstructured":"Havelund , K. , and Pressburger , T . Model checking Java programs using Java pathfinder . International Journal on Software Tools for Technology Transfer (STTT) 2, 4 ( 2000 ), 366--381. Havelund, K., and Pressburger, T. Model checking Java programs using Java pathfinder. International Journal on Software Tools for Technology Transfer (STTT) 2, 4 (2000), 366--381."},{"key":"e_1_3_2_2_26_1","volume-title":"CAV","author":"Henzinger T. A.","year":"2002","unstructured":"Henzinger , T. A. , Jhala , R. , Majumdar , R. , Necula , G. C. , Sutre , G. , and Weimer , W . Temporal-safety proofs for systems code . In CAV ( 2002 ). Henzinger, T. A., Jhala, R., Majumdar, R., Necula, G. C., Sutre, G., and Weimer, W. Temporal-safety proofs for systems code. In CAV (2002)."},{"key":"e_1_3_2_2_27_1","volume-title":"ESOP","author":"Hobor A.","year":"2008","unstructured":"Hobor , A. , Appel , A. W. , and Nardelli , F. Z . Oracle semantics for concurrent separation logic . In ESOP ( 2008 ). Hobor, A., Appel, A. W., and Nardelli, F. Z. Oracle semantics for concurrent separation logic. In ESOP (2008)."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647810.738106"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391479"},{"key":"e_1_3_2_2_31_1","volume-title":"FOCS","author":"Maidl M.","year":"2000","unstructured":"Maidl , M. The common fragment of CTL and LTL . In FOCS ( 2000 ). Maidl, M. The common fragment of CTL and LTL. In FOCS (2000)."},{"key":"e_1_3_2_2_32_1","volume-title":"ATVA","author":"Nain S.","year":"2007","unstructured":"Nain , S. , and Vardi , M . Branching vs. linear time: Semantical perspective . In ATVA ( 2007 ). Nain, S., and Vardi, M. Branching vs. linear time: Semantical perspective. In ATVA (2007)."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_38"},{"key":"e_1_3_2_2_35_1","volume-title":"A Complete Method for the Synthesis of Linear Ranking Functions. LNCS","author":"Podelski A.","year":"2003","unstructured":"Podelski , A. , and Rybalchenko , A . A Complete Method for the Synthesis of Linear Ranking Functions. LNCS ( 2003 ), 239--251. Podelski, A., and Rybalchenko, A. A Complete Method for the Synthesis of Linear Ranking Functions. LNCS (2003), 239--251."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_3_2_2_40_1","volume-title":"SAS","author":"Sankaranarayanan S.","year":"2004","unstructured":"Sankaranarayanan , S. , Sipma , H. , and Manna , Z . Constraint-based linear-relations analysis . In SAS ( 2004 ). Sankaranarayanan, S., Sipma, H., and Manna, Z. Constraint-based linear-relations analysis. In SAS (2004)."},{"key":"e_1_3_2_2_41_1","volume-title":"Model checking on product structures. FMCAD","author":"Schneider K.","year":"1998","unstructured":"Schneider , K. Model checking on product structures. FMCAD ( 1998 ). Schneider, K. Model checking on product structures. FMCAD (1998)."},{"key":"e_1_3_2_2_42_1","volume-title":"Workshop on Verification of Infinite-State Systems (INFINITY)","author":"Schuppan V.","year":"2005","unstructured":"Schuppan , V. , and Biere , A . Liveness checking as safety checking for infinite state spaces . In Workshop on Verification of Infinite-State Systems (INFINITY) ( 2005 ). Schuppan, V., and Biere, A. Liveness checking as safety checking for infinite state spaces. In Workshop on Verification of Infinite-State Systems (INFINITY) (2005)."},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_4"},{"key":"e_1_3_2_2_44_1","volume-title":"TACAS","author":"Vardi M.","year":"2001","unstructured":"Vardi , M. Branching time vs. linear time: Final showdown . In TACAS ( 2001 ). Vardi, M. Branching time vs. linear time: Final showdown. In TACAS (2001)."},{"key":"e_1_3_2_2_45_1","volume-title":"LICS","author":"Vardi M. Y.","year":"1986","unstructured":"Vardi , M. Y. , and Wolper , P . An automata-theoretic approach to automatic program verification (preliminary report) . In LICS ( 1986 ). Vardi, M. Y., and Wolper, P. An automata-theoretic approach to automatic program verification (preliminary report). In LICS (1986)."}],"event":{"name":"POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Austin Texas USA","acronym":"POPL '11","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926431","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1926385.1926431","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:59:51Z","timestamp":1750229991000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1926385.1926431"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1,26]]},"references-count":42,"alternative-id":["10.1145\/1926385.1926431","10.1145\/1926385"],"URL":"https:\/\/doi.org\/10.1145\/1926385.1926431","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1925844.1926431","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2011,1,26]]},"assertion":[{"value":"2011-01-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}