{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:21Z","timestamp":1784837781698,"version":"3.55.0"},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2023,1,9]],"date-time":"2023-01-09T00:00:00Z","timestamp":1673222400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["JP20H04162, JP20K20625, JP22H03564, JP20H05703, JP22H03570"],"award-info":[{"award-number":["JP20H04162, JP20K20625, JP22H03564, JP20H05703, JP22H03570"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-17-1-2787, N00014-22-1-2643"],"award-info":[{"award-number":["N00014-17-1-2787, N00014-22-1-2643"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1618059"],"award-info":[{"award-number":["CCF-1618059"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,1,9]]},"abstract":"<jats:p>We present a novel approach to deciding the validity of formulas in first-order fixpoint logic with background theories and arbitrarily nested inductive and co-inductive predicates defining least and greatest fixpoints. Our approach is constraint-based, and reduces the validity checking problem of the given first-order-fixpoint logic formula (formally, an instance in a language called \u00b5CLP) to a constraint satisfaction problem for a recently introduced predicate constraint language.<\/jats:p><jats:p>Coupled with an existing sound-and-relatively-complete solver for the constraint language, this novel reduction alone already gives a sound and relatively complete method for deciding \u00b5CLP validity, but we further improve it to a novel<jats:italic>modular primal-dual<\/jats:italic>method. The key observations are (1) \u00b5CLP is closed under complement such that each (co-)inductive predicate in the original<jats:italic>primal<\/jats:italic>instance has a corresponding (co-)inductive predicate representing its complement in the<jats:italic>dual<\/jats:italic>instance obtained by taking the standard De Morgan\u2019s dual of the primal instance, and (2)<jats:italic>partial solutions<\/jats:italic>for (co-)inductive predicates synthesized during the constraint solving process of the primal side can be used as sound upper-bounds of the corresponding (co-)inductive predicates in the dual side, and vice versa. By solving the primal and dual problems in parallel and exchanging each others\u2019 partial solutions as sound bounds, the two processes mutually reduce each others\u2019 solution spaces, thus enabling rapid convergence. The approach is also<jats:italic>modular<\/jats:italic>in that the bounds are synthesized and exchanged at granularity of individual (co-)inductive predicates.<\/jats:p><jats:p>We demonstrate the utility of our novel fixpoint logic solving by encoding a wide variety of temporal verification problems in \u00b5CLP, including termination\/non-termination, LTL, CTL, and even the full modal \u00b5-calculus model checking of infinite state programs. The encodings exploit the modularity in both the program and the property by expressing each loops and (recursive) functions in the program and sub-formulas of the property as individual (possibly nested) (co-)inductive predicates. Together with our novel modular primal-dual \u00b5CLP solving, we obtain a novel approach to efficiently solving a wide range of temporal verification problems.<\/jats:p>","DOI":"10.1145\/3571265","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"2111-2140","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":24,"title":["Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"first","affiliation":[{"name":"University of Tsukuba, Japan \/ RIKEN AIP, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5305-4916","authenticated-orcid":false,"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[{"name":"Waseda University, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0036-8967","authenticated-orcid":false,"given":"Yu","family":"Gu","sequence":"additional","affiliation":[{"name":"University of Tsukuba, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7363-634X","authenticated-orcid":false,"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"Stevens Institute of Technology, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"TACAS \u201912","author":"Babiak Tom\u00e1\u0161","unstructured":"Tom\u00e1\u0161 Babiak , Mojm\u00edr K\u0159et\u00ednsk\u00fd , Vojt\u011bch \u0158eh\u00e1k , and Jan Strej\u010dek . 2012. LTL to B\u00fcchi Automata Translation: Fast and More Deterministic . In TACAS \u201912 . Springer , 95\u2013109. Tom\u00e1\u0161 Babiak, Mojm\u00edr K\u0159et\u00ednsk\u00fd, Vojt\u011bch \u0158eh\u00e1k, and Jan Strej\u010dek. 2012. LTL to B\u00fcchi Automata Translation: Fast and More Deterministic. In TACAS \u201912. Springer, 95\u2013109."},{"key":"e_1_2_1_2_1","volume-title":"Rajamani","author":"Ball Thomas","year":"2002","unstructured":"Thomas Ball and Sriram K . Rajamani . 2002 . The SLAM project: debugging system software via static analysis. In POPL \u201902. ACM , 1\u20133. Thomas Ball and Sriram K. Rajamani. 2002. The SLAM project: debugging system software via static analysis. In POPL \u201902. ACM, 1\u20133."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_2_1_4_1","volume-title":"CAV \u201913 (LNCS","author":"Beyene Tewodros A.","unstructured":"Tewodros A. Beyene , Corneliu Popeea , and Andrey Rybalchenko . 2013. Solving Existentially Quantified Horn Clauses . In CAV \u201913 (LNCS , Vol. 8044). Springer, 869\u2013 882 . Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In CAV \u201913 (LNCS, Vol. 8044). Springer, 869\u2013882."},{"key":"e_1_2_1_5_1","volume-title":"Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday (LNCS","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 (LNCS , Vol. 9300). Springer, 24\u2013 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 (LNCS, Vol. 9300). Springer, 24\u201351."},{"key":"e_1_2_1_6_1","volume-title":"CSL \u201999 (LNCS","author":"Bradfield Julian C.","unstructured":"Julian C. Bradfield . 1999. Fixpoint Alternation and the Game Quantifier . In CSL \u201999 (LNCS , Vol. 1683). Springer, 350\u2013 361 . Julian C. Bradfield. 1999. Fixpoint Alternation and the Game Quantifier. In CSL \u201999 (LNCS, Vol. 1683). Springer, 350\u2013361."},{"key":"e_1_2_1_7_1","volume-title":"VMCAI \u201911 (LNCS","author":"Bradley Aaron R.","unstructured":"Aaron R. Bradley . 2011. SAT-based Model Checking Without Unrolling . In VMCAI \u201911 (LNCS , Vol. 6538). Springer, 70\u2013 87 . Aaron R. Bradley. 2011. SAT-based Model Checking Without Unrolling. In VMCAI \u201911 (LNCS, Vol. 6538). Springer, 70\u201387."},{"key":"e_1_2_1_8_1","volume-title":"TACAS \u201916","author":"Brockschmidt Marc","unstructured":"Marc Brockschmidt , Byron Cook , Samin Ishtiaq , Heidy Khlaaf , and Nir Piterman . 2016. T2: Temporal Property Verification . In TACAS \u201916 . Springer , 387\u2013393. isbn:978-3-662-49674-9 Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, and Nir Piterman. 2016. T2: Temporal Property Verification. In TACAS \u201916. Springer, 387\u2013393. isbn:978-3-662-49674-9"},{"key":"e_1_2_1_9_1","volume-title":"TACAS \u201918 (LNCS","author":"Champion Adrien","unstructured":"Adrien Champion , Tomoya Chiba , Naoki Kobayashi , and Ryosuke Sato . 2018. ICE-Based Refinement Type Discovery for Higher-Order Functional Programs . In TACAS \u201918 (LNCS , Vol. 10805). Springer, 365\u2013 384 . Adrien Champion, Tomoya Chiba, Naoki Kobayashi, and Ryosuke Sato. 2018. ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. In TACAS \u201918 (LNCS, Vol. 10805). Springer, 365\u2013384."},{"key":"e_1_2_1_10_1","volume-title":"LICS \u201998","author":"Charatonik Witold","unstructured":"Witold Charatonik , David A. McAllester , Damian Niwinski , Andreas Podelski , and Igor Walukiewicz . 1998. The Horn Mu-calculus . In LICS \u201998 . IEEE Computer Society , 58\u201369. Witold Charatonik, David A. McAllester, Damian Niwinski, Andreas Podelski, and Igor Walukiewicz. 1998. The Horn Mu-calculus. In LICS \u201998. IEEE Computer Society, 58\u201369."},{"key":"e_1_2_1_11_1","volume-title":"O\u2019Hearn","author":"Chen Hong Yi","year":"2014","unstructured":"Hong Yi Chen , Byron Cook , Carsten Fuhs , Kaustubh Nimkar , and Peter W . O\u2019Hearn . 2014 . Proving Nontermination via Safety. In TACAS \u201914 (LNCS , Vol. 8413). Springer, 156\u2013 171 . Hong Yi Chen, Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O\u2019Hearn. 2014. Proving Nontermination via Safety. In TACAS \u201914 (LNCS, Vol. 8413). Springer, 156\u2013171."},{"key":"e_1_2_1_12_1","volume-title":"CAV \u201900 (LNCS","author":"Clarke Edmund M.","unstructured":"Edmund M. Clarke , Orna Grumberg , Somesh Jha , Yuan Lu , and Helmut Veith . 2000. Counterexample-Guided Abstraction Refinement . In CAV \u201900 (LNCS , Vol. 1855). Springer, 154\u2013 169 . Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. 2000. Counterexample-Guided Abstraction Refinement. In CAV \u201900 (LNCS, Vol. 1855). Springer, 154\u2013169."},{"key":"e_1_2_1_13_1","volume-title":"O\u2019Hearn","author":"Cook Byron","year":"2014","unstructured":"Byron Cook , Carsten Fuhs , Kaustubh Nimkar , and Peter W . O\u2019Hearn . 2014 . Disproving termination with overapproximation. In FMCAD \u201914. IEEE , 67\u201374. Byron Cook, Carsten Fuhs, Kaustubh Nimkar, and Peter W. O\u2019Hearn. 2014. Disproving termination with overapproximation. In FMCAD \u201914. IEEE, 67\u201374."},{"key":"e_1_2_1_14_1","volume-title":"TACAS \u201915","author":"Cook Byron","unstructured":"Byron Cook , Heidy Khlaaf , and Nir Piterman . 2015. Fairness for Infinite-State Systems . In TACAS \u201915 . Springer , 384\u2013398. Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015. Fairness for Infinite-State Systems. In TACAS \u201915. Springer, 384\u2013398."},{"key":"e_1_2_1_15_1","volume-title":"CAV \u201915","author":"Cook Byron","unstructured":"Byron Cook , Heidy Khlaaf , and Nir Piterman . 2015. On Automation of CTL* Verification for Infinite-State Systems . In CAV \u201915 . Springer , 13\u201329. Byron Cook, Heidy Khlaaf, and Nir Piterman. 2015. On Automation of CTL* Verification for Infinite-State Systems. In CAV \u201915. Springer, 13\u201329."},{"key":"e_1_2_1_16_1","article-title":"Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems","volume":"64","author":"Cook Byron","year":"2017","unstructured":"Byron Cook , Heidy Khlaaf , and Nir Piterman . 2017 . Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems . J. ACM , 64 , 2 (2017), Article 15, April, 39 pages. Byron Cook, Heidy Khlaaf, and Nir Piterman. 2017. Verifying Increasingly Expressive Temporal Logics for Infinite-State Systems. J. ACM, 64, 2 (2017), Article 15, April, 39 pages.","journal-title":"J. ACM"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Byron Cook and Eric Koskinen. 2011. Making Prophecies with Decision Predicates. In POPL \u201911. ACM 399\u2013410. Byron Cook and Eric Koskinen. 2011. Making Prophecies with Decision Predicates. In POPL \u201911. ACM 399\u2013410.","DOI":"10.1145\/1925844.1926431"},{"key":"e_1_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Byron Cook and Eric Koskinen. 2013. Reasoning About Nondeterminism in Programs. In PLDI \u201913. ACM 219\u2013230. Byron Cook and Eric Koskinen. 2013. Reasoning About Nondeterminism in Programs. In PLDI \u201913. ACM 219\u2013230.","DOI":"10.1145\/2499370.2491969"},{"key":"e_1_2_1_19_1","volume-title":"CAV \u201911","author":"Cook Byron","unstructured":"Byron Cook , Eric Koskinen , and Moshe Vardi . 2011. Temporal Property Verification As a Program Analysis Task . In CAV \u201911 . Springer , 333\u2013348. Byron Cook, Eric Koskinen, and Moshe Vardi. 2011. Temporal Property Verification As a Program Analysis Task. In CAV \u201911. Springer, 333\u2013348."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Byron Cook Andreas Podelski and Andrey Rybalchenko. 2006. Termination proofs for systems code. In PLDI \u201906. ACM 415\u2013426. Byron Cook Andreas Podelski and Andrey Rybalchenko. 2006. Termination proofs for systems code. In PLDI \u201906. ACM 415\u2013426.","DOI":"10.1145\/1133255.1134029"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100049"},{"key":"e_1_2_1_22_1","volume-title":"CAV \u201915","author":"Dietsch Daniel","unstructured":"Daniel Dietsch , Matthias Heizmann , Vincent Langenfeld , and Andreas Podelski . 2015. Fairness Modulo Theory: A New Approach to LTL Software Model Checking . In CAV \u201915 . Springer , 49\u201366. Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, and Andreas Podelski. 2015. Fairness Modulo Theory: A New Approach to LTL Software Model Checking. In CAV \u201915. Springer, 49\u201366."},{"key":"e_1_2_1_23_1","unstructured":"Stephan Falke Deepak Kapur and Carsten Sinz. 2011. Termination Analysis of C Programs Using Compiler Intermediate Languages. In RTA \u201911. 10 Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik 41\u201350. Stephan Falke Deepak Kapur and Carsten Sinz. 2011. Termination Analysis of C Programs Using Compiler Intermediate Languages. In RTA \u201911. 10 Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik 41\u201350."},{"key":"e_1_2_1_24_1","volume-title":"CAV \u201918 (LNCS","author":"Fedyukovich Grigory","unstructured":"Grigory Fedyukovich , Yueling Zhang , and Aarti Gupta . 2018. Syntax-Guided Termination Analysis . In CAV \u201918 (LNCS , Vol. 10981). Springer, 124\u2013 143 . Grigory Fedyukovich, Yueling Zhang, and Aarti Gupta. 2018. Syntax-Guided Termination Analysis. In CAV \u201918 (LNCS, Vol. 10981). Springer, 124\u2013143."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000627"},{"key":"e_1_2_1_26_1","volume-title":"LOPSTR \u201999","author":"Fribourg Laurent","unstructured":"Laurent Fribourg . 1999. Constraint Logic Programming Applied to Model Checking . In LOPSTR \u201999 . Springer , 30\u201341. Laurent Fribourg. 1999. Constraint Logic Programming Applied to Model Checking. In LOPSTR \u201999. Springer, 30\u201341."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"e_1_2_1_28_1","volume-title":"POPL \u201910, Manuel V","author":"Godefroid Patrice","unstructured":"Patrice Godefroid , Aditya V. Nori , Sriram K. Rajamani , and SaiDeep Tetali . 2010. Compositional may-must program analysis: unleashing the power of alternation . In POPL \u201910, Manuel V . Hermenegildo and Jens Palsberg (Eds.). ACM , 43\u201356. Patrice Godefroid, Aditya V. Nori, Sriram K. Rajamani, and SaiDeep Tetali. 2010. Compositional may-must program analysis: unleashing the power of alternation. In POPL \u201910, Manuel V. Hermenegildo and Jens Palsberg (Eds.). ACM, 43\u201356."},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Sergey Grebenshchikov Nuno P. Lopes Corneliu Popeea and Andrey Rybalchenko. 2012. Synthesizing Software Verifiers from Proof Rules. In PLDI \u201912. ACM 405\u2013416. Sergey Grebenshchikov Nuno P. Lopes Corneliu Popeea and Andrey Rybalchenko. 2012. Synthesizing Software Verifiers from Proof Rules. In PLDI \u201912. ACM 405\u2013416.","DOI":"10.1145\/2345156.2254112"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Ashutosh Gupta Thomas A. Henzinger Rupak Majumdar Andrey Rybalchenko and Ru-Gang Xu. 2008. Proving non-termination. In POPL \u201908. ACM 147\u2013158. Ashutosh Gupta Thomas A. Henzinger Rupak Majumdar Andrey Rybalchenko and Ru-Gang Xu. 2008. Proving non-termination. In POPL \u201908. ACM 147\u2013158.","DOI":"10.1145\/1328897.1328459"},{"key":"e_1_2_1_31_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge A . Navas . 2015 . The SeaHorn Verification Framework. In CAV \u201915. Springer , 343\u2013361. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV \u201915. Springer, 343\u2013361."},{"key":"e_1_2_1_32_1","volume-title":"CAV \u201914","author":"Heizmann Matthias","unstructured":"Matthias Heizmann , Jochen Hoenicke , and Andreas Podelski . 2014. Termination Analysis by Learning Terminating Programs . In CAV \u201914 . Springer , 797\u2013813. Matthias Heizmann, Jochen Hoenicke, and Andreas Podelski. 2014. Termination Analysis by Learning Terminating Programs. In CAV \u201914. Springer, 797\u2013813."},{"key":"e_1_2_1_33_1","volume-title":"McMillan","author":"Henzinger Thomas A.","year":"2004","unstructured":"Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , and Kenneth L . McMillan . 2004 . Abstractions from proofs. In POPL \u201904. ACM , 232\u2013244. Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. 2004. Abstractions from proofs. In POPL \u201904. ACM, 232\u2013244."},{"key":"e_1_2_1_34_1","volume-title":"FMCAD \u201918","author":"Hojjat Hossein","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer . 2018. The Eldarica Horn Solver . In FMCAD \u201918 . IEEE , 1\u20137. Hossein Hojjat and Philipp R\u00fcmmer. 2018. The Eldarica Horn Solver. In FMCAD \u201918. IEEE, 1\u20137."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(94)90033-7"},{"key":"e_1_2_1_36_1","volume-title":"McMillan","author":"Jhala Ranjit","year":"2006","unstructured":"Ranjit Jhala and Kenneth L . McMillan . 2006 . A Practical and Complete Approach to Predicate Refinement. In TACAS \u201906 (LNCS , Vol. 3920). Springer, 459\u2013 473 . Ranjit Jhala and Kenneth L. McMillan. 2006. A Practical and Complete Approach to Predicate Refinement. In TACAS \u201906 (LNCS, Vol. 3920). Springer, 459\u2013473."},{"key":"e_1_2_1_37_1","volume-title":"CAV \u201916. 9779","author":"Kahsai Temesghen","unstructured":"Temesghen Kahsai , Philipp R\u00fcmmer , Huascar Sanchez , and Martin Sch\u00e4f . 2016. JayHorn: A Framework for Verifying Java programs . In CAV \u201916. 9779 , Springer , 352\u2013358. Temesghen Kahsai, Philipp R\u00fcmmer, Huascar Sanchez, and Martin Sch\u00e4f. 2016. JayHorn: A Framework for Verifying Java programs. In CAV \u201916. 9779, Springer, 352\u2013358."},{"key":"e_1_2_1_38_1","volume-title":"SAS \u201919","author":"Kobayashi Naoki","unstructured":"Naoki Kobayashi , Takeshi Nishikawa , Atsushi Igarashi , and Hiroshi Unno . 2019. Temporal Verification of Programs via First-Order Fixpoint Logic . In SAS \u201919 . Springer , 413\u2013436. Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. 2019. Temporal Verification of Programs via First-Order Fixpoint Logic. In SAS \u201919. Springer, 413\u2013436."},{"key":"e_1_2_1_39_1","volume-title":"ESOP \u201918","author":"Kobayashi Naoki","unstructured":"Naoki Kobayashi , Takeshi Tsukada , and Keiichi Watanabe . 2018. Higher-Order Program Verification via HFL Model Checking . In ESOP \u201918 . Springer , 711\u2013738. Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. 2018. Higher-Order Program Verification via HFL Model Checking. In ESOP \u201918. Springer, 711\u2013738."},{"key":"e_1_2_1_40_1","volume-title":"CAV \u201914 (LNCS","author":"Komuravelli Anvesh","unstructured":"Anvesh Komuravelli , Arie Gurfinkel , and Sagar Chaki . 2014. SMT-Based Model Checking for Recursive Programs . In CAV \u201914 (LNCS , Vol. 8559). Springer, 17\u2013 34 . Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. 2014. SMT-Based Model Checking for Recursive Programs. In CAV \u201914 (LNCS, Vol. 8559). Springer, 17\u201334."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_2_1_42_1","volume-title":"ESOP \u201914 (LNCS","author":"Kuwahara Takuya","unstructured":"Takuya Kuwahara , Tachio Terauchi , Hiroshi Unno , and Naoki Kobayashi . 2014. Automatic Termination Verification for Higher-Order Functional Programs . In ESOP \u201914 (LNCS , Vol. 8410). Springer, 392\u2013 411 . Takuya Kuwahara, Tachio Terauchi, Hiroshi Unno, and Naoki Kobayashi. 2014. Automatic Termination Verification for Higher-Order Functional Programs. In ESOP \u201914 (LNCS, Vol. 8410). Springer, 392\u2013411."},{"key":"e_1_2_1_43_1","doi-asserted-by":"crossref","unstructured":"Ton Chanh Le Shengchao Qin and Wei-Ngan Chin. 2015. Termination and Non-termination Specification Inference. In PLDI \u201915. ACM 489\u2013498. Ton Chanh Le Shengchao Qin and Wei-Ngan Chin. 2015. Termination and Non-termination Specification Inference. In PLDI \u201915. ACM 489\u2013498.","DOI":"10.1145\/2813885.2737993"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275338"},{"key":"e_1_2_1_45_1","volume-title":"Armin Biere and Roderick Bloem (Eds.) (Lecture Notes in Computer Science","volume":"259","author":"McMillan Kenneth L.","year":"2014","unstructured":"Kenneth L. McMillan . 2014 . Lazy Annotation Revisited. In CAV \u201914 , Armin Biere and Roderick Bloem (Eds.) (Lecture Notes in Computer Science , Vol. 8559). Springer, 243\u2013 259 . Kenneth L. McMillan. 2014. Lazy Annotation Revisited. In CAV \u201914, Armin Biere and Roderick Bloem (Eds.) (Lecture Notes in Computer Science, Vol. 8559). Springer, 243\u2013259."},{"key":"e_1_2_1_46_1","doi-asserted-by":"crossref","unstructured":"Yoji Nanjo Hiroshi Unno Eric Koskinen and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In LICS \u201918. ACM 759\u2013768. Yoji Nanjo Hiroshi Unno Eric Koskinen and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In LICS \u201918. ACM 759\u2013768.","DOI":"10.1145\/3209108.3209204"},{"key":"e_1_2_1_47_1","volume-title":"CL \u201900","author":"Nilsson Ulf","unstructured":"Ulf Nilsson and Johan L\u00fcbcke . 2000. Constraint Logic Programming for Local and Symbolic Model-Checking . In CL \u201900 . Springer , 384\u2013398. Ulf Nilsson and Johan L\u00fcbcke. 2000. Constraint Logic Programming for Local and Symbolic Model-Checking. In CL \u201900. Springer, 384\u2013398."},{"key":"e_1_2_1_48_1","volume-title":"POPL","author":"Padon Oded","year":"2022","unstructured":"Oded Padon , James R. Wilcox , Jason R. Koenig , Kenneth L. McMillan , and Alex Aiken . 2022. Induction duality: primal-dual search for invariants. 6 , POPL ( 2022 ), 1\u201329. Oded Padon, James R. Wilcox, Jason R. Koenig, Kenneth L. McMillan, and Alex Aiken. 2022. Induction duality: primal-dual search for invariants. 6, POPL (2022), 1\u201329."},{"key":"e_1_2_1_49_1","volume-title":"Probabilistic Inference for Predicate Constraint Satisfaction. AAAI \u201920, 34, 02","author":"Satake Yuki","year":"2020","unstructured":"Yuki Satake , Hiroshi Unno , and Hinata Yanagi . 2020. Probabilistic Inference for Predicate Constraint Satisfaction. AAAI \u201920, 34, 02 ( 2020 ), Apr., 1644\u20131651. Yuki Satake, Hiroshi Unno, and Hinata Yanagi. 2020. Probabilistic Inference for Predicate Constraint Satisfaction. AAAI \u201920, 34, 02 (2020), Apr., 1644\u20131651."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09532-0"},{"key":"e_1_2_1_51_1","volume-title":"Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. In ESOP \u201915 (LNCS","author":"Terauchi Tachio","year":"2015","unstructured":"Tachio Terauchi and Hiroshi Unno . 2015 . Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. In ESOP \u201915 (LNCS , Vol. 9032). Springer, 610\u2013 633 . Tachio Terauchi and Hiroshi Unno. 2015. Relaxed Stratification: A New Approach to Practical Complete Predicate Refinement. In ESOP \u201915 (LNCS, Vol. 9032). Springer, 610\u2013633."},{"key":"e_1_2_1_52_1","doi-asserted-by":"crossref","unstructured":"Takeshi Tsukada. 2020. On Computability of Logical Approaches to Branching-Time Property Verification of Programs. In LICS \u201920. ACM 886\u2013899. Takeshi Tsukada. 2020. On Computability of Logical Approaches to Branching-Time Property Verification of Programs. In LICS \u201920. ACM 886\u2013899.","DOI":"10.1145\/3373718.3394766"},{"key":"e_1_2_1_53_1","unstructured":"Hiroshi Unno and Naoki Kobayashi. 2009. Dependent Type Inference with Interpolants. In PPDP \u201909. ACM 277\u2013288. Hiroshi Unno and Naoki Kobayashi. 2009. Dependent Type Inference with Interpolants. In PPDP \u201909. ACM 277\u2013288."},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of the ACM on Programming Languages, 2, POPL","author":"Unno Hiroshi","year":"2017","unstructured":"Hiroshi Unno , Yuki Satake , and Tachio Terauchi . 2017 . Relatively Complete Refinement Type System for Verification of Higher-order Non-deterministic Programs . Proceedings of the ACM on Programming Languages, 2, POPL (2017), Article 12, Dec., 29 pages. Hiroshi Unno, Yuki Satake, and Tachio Terauchi. 2017. Relatively Complete Refinement Type System for Verification of Higher-order Non-deterministic Programs. Proceedings of the ACM on Programming Languages, 2, POPL (2017), Article 12, Dec., 29 pages."},{"key":"e_1_2_1_55_1","volume-title":"Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR, abs\/2007.03656","author":"Unno Hiroshi","year":"2020","unstructured":"Hiroshi Unno , Yuki Satake , Tachio Terauchi , and Eric Koskinen . 2020. Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR, abs\/2007.03656 ( 2020 ), arXiv:2007.03656. arxiv:2007.03656 Hiroshi Unno, Yuki Satake, Tachio Terauchi, and Eric Koskinen. 2020. Program Verification via Predicate Constraint Satisfiability Modulo Theories. CoRR, abs\/2007.03656 (2020), arXiv:2007.03656. arxiv:2007.03656"},{"key":"e_1_2_1_56_1","volume-title":"CAV \u201921","author":"Unno Hiroshi","unstructured":"Hiroshi Unno , Tachio Terauchi , and Eric Koskinen . 2021. Constraint-Based Relational Verification . In CAV \u201921 . Springer , 742\u2013766. Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. In CAV \u201921. Springer, 742\u2013766."},{"key":"e_1_2_1_57_1","volume-title":"CAV \u201917","author":"Unno Hiroshi","unstructured":"Hiroshi Unno , Sho Torii , and Hiroki Sakamoto . 2017. Automating Induction for Solving Horn Clauses . In CAV \u201917 . Springer , 571\u2013591. Hiroshi Unno, Sho Torii, and Hiroki Sakamoto. 2017. Automating Induction for Solving Horn Clauses. In CAV \u201917. Springer, 571\u2013591."},{"key":"e_1_2_1_58_1","volume-title":"SAS \u201913 (LNCS","author":"Urban Caterina","unstructured":"Caterina Urban . 2013. The Abstract Domain of Segmented Ranking Functions . In SAS \u201913 (LNCS , Vol. 7935). Springer, 43\u2013 62 . Caterina Urban. 2013. The Abstract Domain of Segmented Ranking Functions. In SAS \u201913 (LNCS, Vol. 7935). Springer, 43\u201362."},{"key":"e_1_2_1_59_1","volume-title":"TACAS \u201916","author":"Urban Caterina","unstructured":"Caterina Urban , Arie Gurfinkel , and Temesghen Kahsai . 2016. Synthesizing Ranking Functions from Bits and Pieces . In TACAS \u201916 . Springer , 54\u201370. Caterina Urban, Arie Gurfinkel, and Temesghen Kahsai. 2016. Synthesizing Ranking Functions from Bits and Pieces. In TACAS \u201916. Springer, 54\u201370."},{"key":"e_1_2_1_60_1","volume-title":"ESOP \u201914","author":"Urban Caterina","unstructured":"Caterina Urban and Antoine Min\u00e9 . 2014. An Abstract Domain to Infer Ordinal-Valued Ranking Functions . In ESOP \u201914 . Springer , 412\u2013431. Caterina Urban and Antoine Min\u00e9. 2014. An Abstract Domain to Infer Ordinal-Valued Ranking Functions. In ESOP \u201914. Springer, 412\u2013431."},{"key":"e_1_2_1_61_1","volume-title":"SAS \u201918 (LNCS","author":"Urban Caterina","unstructured":"Caterina Urban , Samuel Ueltschi , and Peter M\u00fcller . 2018. Abstract Interpretation of CTL Properties . In SAS \u201918 (LNCS , Vol. 11002). Springer, 402\u2013 422 . Caterina Urban, Samuel Ueltschi, and Peter M\u00fcller. 2018. Abstract Interpretation of CTL Properties. In SAS \u201918 (LNCS, Vol. 11002). Springer, 402\u2013422."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571265","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571265","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:22Z","timestamp":1750183702000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571265"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":61,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571265"],"URL":"https:\/\/doi.org\/10.1145\/3571265","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,9]]},"assertion":[{"value":"2023-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}