{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:59Z","timestamp":1780994579061,"version":"3.54.1"},"reference-count":35,"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":["JP20H05703,JP22H03564,JP20H04162,JP22H03570,JP19H04084"],"award-info":[{"award-number":["JP20H05703,JP22H03564,JP20H04162,JP22H03570,JP19H04084"]}],"id":[{"id":"10.13039\/501100001691","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>Motivated by applications to open program reasoning such as maximal specification inference, this paper studies<jats:italic>optimal CHC solving<\/jats:italic>, a problem to compute maximal and\/or minimal solutions of constrained Horn clauses (CHCs). This problem and its subproblems have been studied in the literature, and a major approach is to iteratively improve a solution of CHCs until it becomes optimal. So a key ingredient of optimization methods is the optimality checking of a given solution. We propose a novel optimality checking method, as well as an optimization method using the proposed optimality checker, based on a computational theoretical analysis of the optimality checking problem. The key observation is that the optimality checking problem is closely related to the termination analysis of programs, and this observation is useful both theoretically and practically. From a theoretical perspective, it clarifies a limitation of an existing method and incorrectness of another method in the literature. From a practical perspective, it allows us to apply techniques of termination analysis to the optimality checking of a solution of CHCs. We present an optimality checking method based on constraint-based synthesis of termination arguments, implemented our method, evaluated it on CHCs that encode maximal specification synthesis problems, and obtained promising results.<\/jats:p>","DOI":"10.1145\/3571214","type":"journal-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T21:58:14Z","timestamp":1673474294000},"page":"604-631","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Optimal CHC Solving via Termination Proofs"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0036-8967","authenticated-orcid":false,"given":"Yu","family":"Gu","sequence":"first","affiliation":[{"name":"University of Tsukuba, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"additional","affiliation":[{"name":"Chiba University, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"University of Tsukuba, Japan \/ RIKEN AIP, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Aws Albarghouthi Isil Dillig and Arie Gurfinkel. 2016. Maximal Specification Synthesis. In POPL \u201916. ACM 789\u2013801. Aws Albarghouthi Isil Dillig and Arie Gurfinkel. 2016. Maximal Specification Synthesis. In POPL \u201916. ACM 789\u2013801.","DOI":"10.1145\/2914770.2837628"},{"key":"e_1_2_1_2_1","volume-title":"SAS \u201910","author":"Alias Christophe","unstructured":"Christophe Alias , Alain Darte , Paul Feautrier , and Laure Gonnord . 2010. Multi-dimensional Rankings, Program Termination , and Complexity Bounds of Flowchart Programs . In SAS \u201910 . Springer , 117\u2013133. Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. 2010. Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs. In SAS \u201910. Springer, 117\u2013133."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_2_1_4_1","volume-title":"Ben-Amram and Samir Genaim","author":"Amir","year":"2017","unstructured":"Amir M. Ben-Amram and Samir Genaim . 2017 . On Multiphase-Linear Ranking Functions. In CAV \u201917. Springer , 601\u2013620. Amir M. Ben-Amram and Samir Genaim. 2017. On Multiphase-Linear Ranking Functions. In CAV \u201917. Springer, 601\u2013620."},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","unstructured":"Tewodros Beyene Swarat Chaudhuri Corneliu Popeea and Andrey Rybalchenko. 2014. A Constraint-based Approach to Solving Games on Infinite Graphs. In POPL \u201914. ACM 221\u2013233. Tewodros Beyene Swarat Chaudhuri Corneliu Popeea and Andrey Rybalchenko. 2014. A Constraint-based Approach to Solving Games on Infinite Graphs. In POPL \u201914. ACM 221\u2013233.","DOI":"10.1145\/2578855.2535860"},{"key":"e_1_2_1_6_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_7_1","volume-title":"Lahiri","author":"Blackshear Sam","year":"2013","unstructured":"Sam Blackshear and Shuvendu K . Lahiri . 2013 . Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings. In PLDI \u201913 (PLDI \u201913). ACM , 209\u2013218. Sam Blackshear and Shuvendu K. Lahiri. 2013. Almost-Correct Specifications: A Modular Semantic Framework for Assigning Confidence to Warnings. In PLDI \u201913 (PLDI \u201913). ACM, 209\u2013218."},{"key":"e_1_2_1_8_1","volume-title":"Sipma","author":"Bradley Aaron R.","year":"2005","unstructured":"Aaron R. Bradley , Zohar Manna , and Henny B . Sipma . 2005 . Linear Ranking with Reachability. In CAV \u201905 (LNCS , Vol. 3576). Springer, 491\u2013 504 . Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2005. Linear Ranking with Reachability. In CAV \u201905 (LNCS, Vol. 3576). Springer, 491\u2013504."},{"key":"e_1_2_1_9_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_10_1","volume-title":"VMCAI \u201913","author":"Cousot Patrick","unstructured":"Patrick Cousot , Radhia Cousot , Manuel F\u00e4hndrich , and Francesco Logozzo . 2013. Automatic Inference of Necessary Preconditions . In VMCAI \u201913 . Springer , 128\u2013148. Patrick Cousot, Radhia Cousot, Manuel F\u00e4hndrich, and Francesco Logozzo. 2013. Automatic Inference of Necessary Preconditions. In VMCAI \u201913. Springer, 128\u2013148."},{"key":"e_1_2_1_11_1","volume-title":"Angelic Verification: Precise Verification Modulo Unknowns. In CAV \u201915","author":"Das Ankush","year":"2015","unstructured":"Ankush Das , Shuvendu K. Lahiri , Akash Lal , and Yi Li . 2015 . Angelic Verification: Precise Verification Modulo Unknowns. In CAV \u201915 . Springer , 324\u2013342. Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li. 2015. Angelic Verification: Precise Verification Modulo Unknowns. In CAV \u201915. Springer, 324\u2013342."},{"key":"e_1_2_1_12_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_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9388-y"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Laure Gonnord David Monniaux and Gabriel Radanne. 2015. Synthesis of Ranking Functions Using Extremal Counterexamples. In PLDI \u201915. ACM 608\u2013618. Laure Gonnord David Monniaux and Gabriel Radanne. 2015. Synthesis of Ranking Functions Using Extremal Counterexamples. In PLDI \u201915. ACM 608\u2013618.","DOI":"10.1145\/2813885.2737976"},{"key":"e_1_2_1_15_1","volume-title":"SAS \u201915 (LNCS","author":"Hashimoto Kodai","unstructured":"Kodai Hashimoto and Hiroshi Unno . 2015. Refinement Type Inference via Horn Constraint Optimization . In SAS \u201915 (LNCS , Vol. 9291). Springer, 199\u2013 216 . Kodai Hashimoto and Hiroshi Unno. 2015. Refinement Type Inference via Horn Constraint Optimization. In SAS \u201915 (LNCS, Vol. 9291). Springer, 199\u2013216."},{"key":"e_1_2_1_16_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_17_1","volume-title":"CAV \u201921","author":"Kura Satoshi","unstructured":"Satoshi Kura , Hiroshi Unno , and Ichiro Hasuo . 2021. Decision Tree Learning in CEGIS-Based Termination Analysis . In CAV \u201921 . Springer , 75\u201398. Satoshi Kura, Hiroshi Unno, and Ichiro Hasuo. 2021. Decision Tree Learning in CEGIS-Based Termination Analysis. In CAV \u201921. Springer, 75\u201398."},{"key":"e_1_2_1_18_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_19_1","volume-title":"FMCAD \u201920","author":"Lahiri Shuvendu K.","unstructured":"Shuvendu K. Lahiri , Akash Lal , Sridhar Gopinath , Alexander Nutz , Vladimir Levin , Rahul Kumar , Nate Deisinger , Jakob Lichtenberg , and Chetan Bansal . 2020. Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost . In FMCAD \u201920 . IEEE , 169\u2013178. Shuvendu K. Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, and Chetan Bansal. 2020. Angelic Checking within Static Driver Verifier: Towards high-precision defects without (modeling) cost. In FMCAD \u201920. IEEE, 169\u2013178."},{"key":"e_1_2_1_20_1","volume-title":"Ben-Amram","author":"Lee Chin Soon","year":"2001","unstructured":"Chin Soon Lee , Neil D. Jones , and Amir M . Ben-Amram . 2001 . The size-change principle for program termination. In POPL \u201901. ACM , 81\u201392. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. 2001. The size-change principle for program termination. In POPL \u201901. ACM, 81\u201392."},{"key":"e_1_2_1_21_1","volume-title":"TACAS \u201914 (LNCS","author":"Leike Jan","unstructured":"Jan Leike and Matthias Heizmann . 2014. Ranking Templates for Linear Loops . In TACAS \u201914 (LNCS , Vol. 8413). Springer, 172\u2013 186 . Jan Leike and Matthias Heizmann. 2014. Ranking Templates for Linear Loops. In TACAS \u201914 (LNCS, Vol. 8413). Springer, 172\u2013186."},{"key":"e_1_2_1_22_1","volume-title":"Millstein","author":"Padhi Saswat","year":"2016","unstructured":"Saswat Padhi , Rahul Sharma , and Todd D . Millstein . 2016 . Data-Driven Precondition Inference with Learned Features. In PLDI \u201916. 42\u201356. Saswat Padhi, Rahul Sharma, and Todd D. Millstein. 2016. Data-Driven Precondition Inference with Learned Features. In PLDI \u201916. 42\u201356."},{"key":"e_1_2_1_23_1","volume-title":"VMCAI \u201904 (LNCS","author":"Podelski Andreas","unstructured":"Andreas Podelski and Andrey Rybalchenko . 2004. A Complete Method for the Synthesis of Linear Ranking Functions . In VMCAI \u201904 (LNCS , Vol. 2937). Springer, 239\u2013 251 . Andreas Podelski and Andrey Rybalchenko. 2004. A Complete Method for the Synthesis of Linear Ranking Functions. In VMCAI \u201904 (LNCS, Vol. 2937). Springer, 239\u2013251."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Sumanth Prabhu Grigory Fedyukovich Kumar Madhukar and Deepak D\u2019Souza. 2021. Specification Synthesis with Constrained Horn Clauses. In PLDI \u201921. ACM 1203\u20131217. Sumanth Prabhu Grigory Fedyukovich Kumar Madhukar and Deepak D\u2019Souza. 2021. Specification Synthesis with Constrained Horn Clauses. In PLDI \u201921. ACM 1203\u20131217.","DOI":"10.1145\/3453483.3454104"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Sriram Sankaranarayanan Swarat Chaudhuri Franjo Ivan\u010di\u0107 and Aarti Gupta. 2008. Dynamic Inference of Likely Data Preconditions over Predicates by Tree Learning. In ISSTA \u201908 (ISSTA \u201908). ACM 295\u2013306. Sriram Sankaranarayanan Swarat Chaudhuri Franjo Ivan\u010di\u0107 and Aarti Gupta. 2008. Dynamic Inference of Likely Data Preconditions over Predicates by Tree Learning. In ISSTA \u201908 (ISSTA \u201908). ACM 295\u2013306.","DOI":"10.1145\/1390630.1390666"},{"key":"e_1_2_1_26_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_27_1","volume-title":"ESOP \u201913","author":"Seghir Mohamed Nassim","unstructured":"Mohamed Nassim Seghir and Daniel Kroening . 2013. Counterexample-Guided Precondition Inference . In ESOP \u201913 . Springer , 451\u2013471. Mohamed Nassim Seghir and Daniel Kroening. 2013. Counterexample-Guided Precondition Inference. In ESOP \u201913. Springer, 451\u2013471."},{"key":"e_1_2_1_28_1","volume-title":"First-order logic","author":"Smullyan Raymond M.","unstructured":"Raymond M. Smullyan . 1968. First-order logic . Springer . Raymond M. Smullyan. 1968. First-order logic. Springer."},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In ASPLOS XII. ACM 404\u2013415. Armando Solar-Lezama Liviu Tancau Rastislav Bodik Sanjit Seshia and Vijay Saraswat. 2006. Combinatorial Sketching for Finite Programs. In ASPLOS XII. ACM 404\u2013415.","DOI":"10.1145\/1168918.1168907"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"Saurabh Srivastava and Sumit Gulwani. 2009. Program verification using templates over predicate abstraction. In PLDI \u201909. ACM 223\u2013234. Saurabh Srivastava and Sumit Gulwani. 2009. Program verification using templates over predicate abstraction. In PLDI \u201909. ACM 223\u2013234.","DOI":"10.1145\/1543135.1542501"},{"key":"e_1_2_1_31_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_32_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_33_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_34_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_35_1","volume-title":"Proceedings of the ACM on Programming Languages, 5, OOPSLA","author":"Zhou Zhe","year":"2021","unstructured":"Zhe Zhou , Robert Dickerson , Benjamin Delaware , and Suresh Jagannathan . 2021 . Data-Driven Abductive Inference of Library Specifications . Proceedings of the ACM on Programming Languages, 5, OOPSLA (2021), Article 116, Oct., 29 pages. Zhe Zhou, Robert Dickerson, Benjamin Delaware, and Suresh Jagannathan. 2021. Data-Driven Abductive Inference of Library Specifications. Proceedings of the ACM on Programming Languages, 5, OOPSLA (2021), Article 116, Oct., 29 pages."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571214","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3571214","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:21Z","timestamp":1750183701000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3571214"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,9]]},"references-count":35,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2023,1,9]]}},"alternative-id":["10.1145\/3571214"],"URL":"https:\/\/doi.org\/10.1145\/3571214","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"}}]}}