{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,21]],"date-time":"2026-03-21T02:34:36Z","timestamp":1774060476660,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":25,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,7,8]],"date-time":"2020-07-08T00:00:00Z","timestamp":1594166400000},"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":[[2020,7,8]]},"DOI":"10.1145\/3373718.3394766","type":"proceedings-article","created":{"date-parts":[[2020,5,26]],"date-time":"2020-05-26T00:23:18Z","timestamp":1590452598000},"page":"886-899","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["On Computability of Logical Approaches to Branching-Time Property Verification of Programs"],"prefix":"10.1145","author":[{"given":"Takeshi","family":"Tsukada","sequence":"first","affiliation":[{"name":"The University of Tokyo, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,7,8]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535860"},{"key":"e_1_3_2_1_2_1","volume-title":"Solving Existentially Quantified Horn Clauses. In The 25th International Conference on Computer Aided Verification (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.)","volume":"8044","author":"Beyene Tewodros A.","year":"2013","unstructured":"Tewodros A. Beyene , Corneliu Popeea , and Andrey Rybalchenko . 2013 . Solving Existentially Quantified Horn Clauses. In The 25th International Conference on Computer Aided Verification (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.) , Vol. 8044 . Springer, 869--882. Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In The 25th International Conference on Computer Aided Verification (Lecture Notes in Computer Science), Natasha Sharygina and Helmut Veith (Eds.), Vol. 8044. Springer, 869--882."},{"key":"e_1_3_2_1_3_1","volume-title":"Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science), Lev D","author":"Bj\u00f8rner Nikolaj","unstructured":"Nikolaj Bj\u00f8rner , Arie Gurfinkel , Kenneth L. McMillan , and Andrey Rybalchenko . 2015. Horn Clause Solvers for Program Verification . In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science), Lev D . Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, and Wolfram Schulte (Eds.), Vol. 9300 . Springer , 24--51. Nikolaj Bj\u00f8rner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 2015. Horn Clause Solvers for Program Verification. In Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (Lecture Notes in Computer Science), Lev D. Beklemishev, Andreas Blass, Nachum Dershowitz, Bernd Finkbeiner, and Wolfram Schulte (Eds.), Vol. 9300. Springer, 24--51."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00217-X"},{"key":"e_1_3_2_1_5_1","volume-title":"Fixpoint Alternation and the Game Quantifier. In The 8th EACSL Annual Conference on Computer Science Logic (Lecture Notes in Computer Science), J\u00f6rg Flum and Mario Rodr\u00edguez-Artalejo (Eds.)","volume":"1683","author":"Bradfield Julian C.","year":"1999","unstructured":"Julian C. Bradfield . 1999 . Fixpoint Alternation and the Game Quantifier. In The 8th EACSL Annual Conference on Computer Science Logic (Lecture Notes in Computer Science), J\u00f6rg Flum and Mario Rodr\u00edguez-Artalejo (Eds.) , Vol. 1683 . Springer, 350--361. Julian C. Bradfield. 1999. Fixpoint Alternation and the Game Quantifier. In The 8th EACSL Annual Conference on Computer Science Logic (Lecture Notes in Computer Science), J\u00f6rg Flum and Mario Rodr\u00edguez-Artalejo (Eds.), Vol. 1683. Springer, 350--361."},{"key":"e_1_3_2_1_6_1","volume-title":"The 39th International Symposium on Mathematical Foundations of Computer Science (Lecture Notes in Computer Science), Erzs\u00e9bet Csuhaj-Varj\u00fa, Martin Dietzfelbinger, and Zolt\u00e1n \u00c9sik (Eds.)","author":"Bruse Florian","unstructured":"Florian Bruse . 2014. Alternating Parity Krivine Automata . In The 39th International Symposium on Mathematical Foundations of Computer Science (Lecture Notes in Computer Science), Erzs\u00e9bet Csuhaj-Varj\u00fa, Martin Dietzfelbinger, and Zolt\u00e1n \u00c9sik (Eds.) , Vol. 8634 . Springer , 111--122. Florian Bruse. 2014. Alternating Parity Krivine Automata. In The 39th International Symposium on Mathematical Foundations of Computer Science (Lecture Notes in Computer Science), Erzs\u00e9bet Csuhaj-Varj\u00fa, Martin Dietzfelbinger, and Zolt\u00e1n \u00c9sik (Eds.), Vol. 8634. Springer, 111--122."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.226.8"},{"key":"e_1_3_2_1_8_1","volume-title":"Lecture Notes in Computer Science","volume":"2500","author":"Gr\u00e4del Erich","year":"2002","unstructured":"Erich Gr\u00e4del , Wolfgang Thomas , and Thomas Wilke ( Eds .). 2002 . Automata, Logics, and Infinite Games: A Guide to Current Research . Lecture Notes in Computer Science , Vol. 2500 . Springer. Erich Gr\u00e4del, Wolfgang Thomas, and Thomas Wilke (Eds.). 2002. Automata, Logics, and Infinite Games: A Guide to Current Research. Lecture Notes in Computer Science, Vol. 2500. Springer."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4993"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273936"},{"key":"e_1_3_2_1_11_1","volume-title":"Theory of recursive functions and effective computability","author":"Hartley Rogers Jr.","unstructured":"Hartley Rogers Jr. 1987. Theory of recursive functions and effective computability . MIT Press . Hartley Rogers Jr. 1987. Theory of recursive functions and effective computability. MIT Press."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009854"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_20"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.29"},{"key":"e_1_3_2_1_15_1","volume-title":"Higher-Order Program Verification via HFL Model Checking. CoRR abs\/1710.08614","author":"Kobayashi Naoki","year":"2017","unstructured":"Naoki Kobayashi , Takeshi Tsukada , and Keiichi Watanabe . 2017. Higher-Order Program Verification via HFL Model Checking. CoRR abs\/1710.08614 ( 2017 ). arXiv:1710.08614 Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. 2017. Higher-Order Program Verification via HFL Model Checking. CoRR abs\/1710.08614 (2017). arXiv:1710.08614"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_25"},{"key":"e_1_3_2_1_17_1","volume-title":"Theory of Computation","author":"Kozen Dexter","unstructured":"Dexter Kozen . 2006. Theory of Computation . Springer . Dexter Kozen. 2006. Theory of Computation. Springer."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275338"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_3_2_1_20_1","volume-title":"Transition Invariants. In The 19th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 32--41","author":"Podelski Andreas","year":"2004","unstructured":"Andreas Podelski and Andrey Rybalchenko . 2004 . Transition Invariants. In The 19th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 32--41 . Andreas Podelski and Andrey Rybalchenko. 2004. Transition Invariants. In The 19th IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 32--41."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158100"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_33"},{"key":"e_1_3_2_1_24_1","volume-title":"Lambda Y-Calculus With Priorities. In The 34th Annual ACM\/IEEE Symposium on Logic in Computer Science. IEEE, 1--13","author":"Walukiewicz Igor","year":"2019","unstructured":"Igor Walukiewicz . 2019 . Lambda Y-Calculus With Priorities. In The 34th Annual ACM\/IEEE Symposium on Logic in Computer Science. IEEE, 1--13 . Igor Walukiewicz. 2019. Lambda Y-Calculus With Priorities. In The 34th Annual ACM\/IEEE Symposium on Logic in Computer Science. IEEE, 1--13."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3294032.3294077"}],"event":{"name":"LICS '20: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","location":"Saarbr\u00fccken Germany","acronym":"LICS '20","sponsor":["SIGLOG ACM Special Interest Group on Logic and Computation","EACSL European Association for Computer Science Logic","IEEE-CS\\DATC IEEE Computer Society"]},"container-title":["Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394766","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3373718.3394766","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:35Z","timestamp":1750197755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3373718.3394766"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,8]]},"references-count":25,"alternative-id":["10.1145\/3373718.3394766","10.1145\/3373718"],"URL":"https:\/\/doi.org\/10.1145\/3373718.3394766","relation":{},"subject":[],"published":{"date-parts":[[2020,7,8]]},"assertion":[{"value":"2020-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}