{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:21:38Z","timestamp":1770283298370,"version":"3.49.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"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":["KAKENHI JP20H05703, JP22H03654, JP20H04162, JP19H04084"],"award-info":[{"award-number":["KAKENHI JP20H05703, JP22H03654, JP20H04162, 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":[[2024,6,20]]},"abstract":"<jats:p>\n            The constrained Horn clause satisfiability problem is at the core of many automated verification methods, and S\n            <jats:sc>pacer<\/jats:sc>\n            is one of the most efficient solvers of this problem. The standard description of S\n            <jats:sc>pacer<\/jats:sc>\n            is based on an abstract transition system, dividing the whole procedure into small rules. This division makes individual rules easier to understand but, conversely, makes it difficult to discuss the procedure as a whole. As evidence of the difficulty in understanding the whole procedure, we point out that the claimed refutational completeness actually fails for several reasons, some of which were not present in the original version and subsequently added. It is also difficult to grasp the differences between S\n            <jats:sc>pacer<\/jats:sc>\n            and another procedure, such as GPDR.\n          <\/jats:p>\n          <jats:p>\n            This paper aims to provide a better understanding of S\n            <jats:sc>pacer<\/jats:sc>\n            by developing a S\n            <jats:sc>pacer<\/jats:sc>\n            -like procedure defined by structural induction. We first formulate the problem to be solved inductively, then give its naive solver and transform it to obtain a S\n            <jats:sc>pacer<\/jats:sc>\n            -like procedure. Interestingly, our inductive approach almost unifies S\n            <jats:sc>pacer<\/jats:sc>\n            and GPDR, which differ in only one respect in our understanding. To demonstrate the usefulness of our inductive approach in understanding S\n            <jats:sc>pacer<\/jats:sc>\n            , we examine S\n            <jats:sc>pacer<\/jats:sc>\n            variants in the literature in terms of inductive procedures and discuss why they are not refutationally complete and how to fix them. We also implemented the proposed procedure and evaluated it experimentally.\n          <\/jats:p>","DOI":"10.1145\/3656457","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1979-2002","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Inductive Approach to Spacer"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2824-8708","authenticated-orcid":false,"given":"Takeshi","family":"Tsukada","sequence":"first","affiliation":[{"name":"Chiba University, Chiba, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4225-8195","authenticated-orcid":false,"given":"Hiroshi","family":"Unno","sequence":"additional","affiliation":[{"name":"Tohoku University, Sendai, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_27"},{"key":"e_1_3_1_3_1","first-page":"869","article-title":"Solving Existentially Quantified Horn Clauses","author":"Beyene Tewodros A.","year":"2013","unstructured":"Tewodros A. Beyene, Corneliu Popeea, and Andrey Rybalchenko. 2013. Solving Existentially Quantified Horn Clauses. In CAV \u201813 (LNCS), Vol. 8044. Springer, 869-882.","journal-title":"In CAV \u201813 (LNCS), Vol. 8044. Springer"},{"key":"e_1_3_1_4_1","first-page":"15","article-title":"Playing with Quantified Satisfaction","author":"Bjorner Nikolaj","year":"2015","unstructured":"Nikolaj Bjorner and Mikolas Janota. 2015. Playing with Quantified Satisfaction. In LPAR \u201815 (EPiC Series in Computing), Vol. 35. EasyChair, 15-27.","journal-title":"In LPAR \u201815 (EPiC Series in Computing), Vol. 35. EasyChair"},{"key":"e_1_3_1_5_1","first-page":"105","article-title":"On Solving Universally Quantified Horn Clauses","author":"Bjorner Nikolaj","year":"2013","unstructured":"Nikolaj Bjorner, Ken McMillan, and Andrey Rybalchenko. 2013. On Solving Universally Quantified Horn Clauses. In SAS \u201813 (LNCS), Vol. 7935. Springer, 105-125.","journal-title":"In SAS \u201813 (LNCS), Vol. 7935. Springer"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_29"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_3_1_8_1","article-title":"Higher-order constrained horn clauses for verification","author":"Burn Toby Cathcart","year":"2018","unstructured":"Toby Cathcart Burn, C.-H. Luke Ong, and Steven J. Ramsay. 2018. Higher-order constrained horn clauses for verification. Proceedings ofthe ACM on Programming Languages 2, POPL (2018), 11:1-11:28.","journal-title":"Proceedings ofthe ACM on Programming Languages 2, POPL (2018), 11:1-11:28"},{"key":"e_1_3_1_9_1","doi-asserted-by":"crossref","unstructured":"Leonardo de Moura and Nikolaj Bjorner. 2008. Z3: An Efficient SMT Solver. In TACAS \u201808 (Budapest Hungary March29 - April 6) (LNCS) Vol. 4963. Springer 337-340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_10_1","first-page":"125","article-title":"Efficient implementation of property directed reachability","author":"Een Niklas","year":"2011","unstructured":"Niklas Een, Alan Mishchenko, and Robert Brayton. 2011. Efficient implementation of property directed reachability. In 2011 Formal Methods in Computer-AidedDesign (FMCAD). 125-134.","journal-title":"In 2011 Formal Methods in Computer-AidedDesign (FMCAD)"},{"key":"e_1_3_1_11_1","first-page":"735","article-title":"Linear Arithmetic Satisfiability via Strategy Improvement","author":"Farzan Azadeh","year":"2016","unstructured":"Azadeh Farzan and Zachary Kincaid. 2016. Linear Arithmetic Satisfiability via Strategy Improvement. In IJCAI \u201816. AAAI Press, 735-743.","journal-title":"In IJCAI \u201816. AAAI Press"},{"key":"e_1_3_1_12_1","doi-asserted-by":"crossref","unstructured":"Yotam M. Y. Feldman Neil Immerman Mooly Sagiv and Sharon Shoham. 2019. Complexity and Information in Invariant Inference. 4 POPL Article 5 (dec 2019) 29 pages.","DOI":"10.1145\/3371073"},{"key":"e_1_3_1_13_1","doi-asserted-by":"crossref","unstructured":"Yotam M. Y. Feldman Mooly Sagiv Sharon Shoham and James R. Wilcox. 2022. Property-Directed Reachability as Abstract Interpretation in the Monotone Theory. 6 POPL Article 15 (jan 2022) 31 pages.","DOI":"10.1145\/3498676"},{"key":"e_1_3_1_14_1","first-page":"201","author":"Feldman Yotam M. Y.","year":"2022","unstructured":"Yotam M. Y. Feldman and Sharon Shoham. 2022. Invariant Inference with Provable Complexity from the Monotone Theory. Springer, Cham, 201-226.","journal-title":"Invariant Inference with Provable Complexity from the Monotone Theory"},{"key":"e_1_3_1_15_1","first-page":"131","article-title":"On Symmetry and Quantification: A New Approach to Verify Distributed Protocols","author":"Goel Aman","year":"2021","unstructured":"Aman Goel and Karem A. Sakallah. 2021. On Symmetry and Quantification: A New Approach to Verify Distributed Protocols. In NFM \u201821. 131-150.","journal-title":"In NFM \u201821"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706353"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31612-8_13"},{"key":"e_1_3_1_18_1","first-page":"457","article-title":"^Z: An Efficient Engine for Fixed Points with Constraints","author":"Hoder Krystof","year":"2011","unstructured":"Krystof Hoder, Nikolaj Bjorner, and Leonardo de Moura. 2011. ^Z: An Efficient Engine for Fixed Points with Constraints. In CAV \u201811 (Snowbird, UT) (LNCS), Vol. 6806. Springer, 457-462.","journal-title":"In CAV \u201811 (Snowbird, UT) (LNCS), Vol. 6806. Springer"},{"key":"e_1_3_1_19_1","first-page":"1","author":"Hojjat Hossein","year":"2018","unstructured":"Hossein Hojjat and Philipp R\u00fcmmer. 2018. The Eldarica Horn Solver. In FMCAD \u201818. IEEE, 1-7.","journal-title":"The Eldarica Horn Solver. In FMCAD \u201818. IEEE"},{"key":"e_1_3_1_20_1","doi-asserted-by":"crossref","unstructured":"Aleksandr Karbyshev Nikolaj Bjorner Shachar Itzhaky Noam Rinetzky and Sharon Shoham. 2017. Property-Directed Inference of Universal Invariants or Proving Their Absence. J. ACM 64 1 Article 7 (mar 2017) 33 pages.","DOI":"10.1145\/3022187"},{"key":"e_1_3_1_21_1","first-page":"413","article-title":"Temporal Verification ofPrograms via First-Order Fixpoint Logic","author":"Kobayashi Naoki","year":"2019","unstructured":"Naoki Kobayashi, Takeshi Nishikawa, Atsushi Igarashi, and Hiroshi Unno. 2019. Temporal Verification ofPrograms via First-Order Fixpoint Logic. In SAS \u201819. Springer, 413-436.","journal-title":"In SAS \u201819. Springer"},{"key":"e_1_3_1_22_1","first-page":"711","article-title":"Higher-Order Program Verification via HFL Model Checking","author":"Kobayashi Naoki","year":"2018","unstructured":"Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe. 2018. Higher-Order Program Verification via HFL Model Checking. In ESOP \u201818. Springer, 711-738.","journal-title":"In ESOP \u201818. Springer"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/fmcad.2015.7542257"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0249-4"},{"key":"e_1_3_1_26_1","first-page":"101","article-title":"Global Guidance for Local Generalization in Model Checking","author":"Krishnan Hari Govind Vediramana","year":"2020","unstructured":"Hari Govind Vediramana Krishnan, Yuting Chen, Sharon Shoham, and Arie Gurfinkel. 2020. Global Guidance for Local Generalization in Model Checking. In CAV \u201820 (LNCS), Vol. 12225. Springer, 101-125.","journal-title":"In CAV \u201820 (LNCS), Vol. 12225. Springer"},{"key":"e_1_3_1_27_1","first-page":"83","article-title":"Redundant argument filtering of logic programs","author":"Leuschel Michael","year":"1997","unstructured":"Michael Leuschel and Morten Heine Sorensen. 1997. Redundant argument filtering of logic programs. In LOPSTR \u201897. Springer, 83-103.","journal-title":"In LOPSTR \u201897. Springer"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_1_30_1","doi-asserted-by":"crossref","unstructured":"Patrick Rondon Ming Kawaguchi and Ranjit Jhala. 2008. Liquid Types. In PLDI \u201808. ACM 159-169.","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54108-7_1"},{"key":"e_1_3_1_32_1","first-page":"1644","article-title":"Probabilistic Inference for Predicate Constraint Satisfaction","author":"Satake Yuki","year":"2020","unstructured":"Yuki Satake, Hiroshi Unno, and Hinata Yanagi. 2020. Probabilistic Inference for Predicate Constraint Satisfaction. AAAI \u201820 34, 02 (Apr. 2020), 1644-1651.","journal-title":"AAAI \u201820 34, 02 (Apr. 2020)"},{"key":"e_1_3_1_33_1","first-page":"161","article-title":"Property Directed Self Composition","author":"Shemer Ron","year":"2019","unstructured":"Ron Shemer, Arie Gurfinkel, Sharon Shoham, and Yakir Vizel. 2019. Property Directed Self Composition. In CAV \u201819 (LNCS), Vol. 11561. Springer, 161-179.","journal-title":"In CAV \u201819 (LNCS), Vol. 11561. Springer"},{"key":"e_1_3_1_34_1","first-page":"206","article-title":"Retrofitting Effect Handlers onto OCaml","author":"Sivaramakrishnan KC","year":"2021","unstructured":"KC Sivaramakrishnan, Stephen Dolan, Leo White, Tom Kelly, Sadiq Jaffer, and Anil Madhavapeddy. 2021. Retrofitting Effect Handlers onto OCaml. In PLDI \u201821 (Virtual, Canada) (PLDI 2021). ACM, 206-221.","journal-title":"In PLDI \u201821 (Virtual, Canada) (PLDI 2021). ACM"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Takeshi Tsukada and Hiroshi Unno. 2021. Software Model-Checking as Cyclic-ProofSearch. https:\/\/doi.org\/10.48550\/ARXIV.2111.05617 10.48550\/ARXIV.2111.05617","DOI":"10.48550\/ARXIV.2111.05617"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498725"},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","unstructured":"Hiroshi Unno and Naoki Kobayashi. 2009. Dependent Type Inference with Interpolants. In PPDP\u201909. ACM 277-288.","DOI":"10.1145\/1599410.1599445"},{"key":"e_1_3_1_38_1","doi-asserted-by":"crossref","unstructured":"Hiroshi Unno Tachio Terauchi Yu Gu and Eric Koskinen. 2023. Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. 7 POPL Article 72 (jan 2023) 30 pages.","DOI":"10.1145\/3571265"},{"key":"e_1_3_1_39_1","first-page":"742","article-title":"Constraint-Based Relational Verification","author":"Unno Hiroshi","year":"2021","unstructured":"Hiroshi Unno, Tachio Terauchi, and Eric Koskinen. 2021. Constraint-Based Relational Verification. In CAV \u201821. Springer, 742-766.","journal-title":"In CAV \u201821. Springer"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656457","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656457","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:42:44Z","timestamp":1751661764000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656457"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":38,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656457"],"URL":"https:\/\/doi.org\/10.1145\/3656457","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}