{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:33:56Z","timestamp":1767929636842,"version":"3.49.0"},"reference-count":92,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["759102-SVIS"],"award-info":[{"award-number":["759102-SVIS"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["2117\/23"],"award-info":[{"award-number":["2117\/23"]}],"id":[{"id":"10.13039\/501100003977","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,1,2]]},"abstract":"<jats:p>\n            First-order logic, and quantifiers in particular, are widely used in deductive verification of programs and systems. Quantifiers are essential for describing systems with unbounded domains, but prove difficult for automated solvers. Significant effort has been dedicated to finding quantifier instantiations that establish unsatisfiability of quantified formulas, thus ensuring validity of a system\u2019s verification conditions. However, in many cases the formulas are satisfiable\u2014this is often the case in intermediate steps of the verification process, e.g., when an invariant is not yet inductive. For such cases, existing tools are limited to finding\n            <jats:italic toggle=\"yes\">finite<\/jats:italic>\n            models as counterexamples. Yet, some quantified formulas are satisfiable but only have\n            <jats:italic toggle=\"yes\">infinite<\/jats:italic>\n            models, which current solvers are unable to find. Such infinite counter-models are especially typical when first-order logic is used to approximate the natural numbers, the integers, or other inductive definitions such as linked lists, which is common in deductive verification. The inability of solvers to find infinite models makes them diverge in these cases, providing little feedback to the user as they try to make progress in their verification attempts.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we tackle the problem of finding such infinite models, specifically, finite representations thereof that can be presented to the user of a deductive verification tool. These models give insight into the verification failure, and allow the user to identify and fix bugs in the modeling of the system and its properties. Our approach consists of three parts. First, we introduce\n            <jats:italic toggle=\"yes\">symbolic structures<\/jats:italic>\n            as a way to represent certain infinite models, and show they admit an efficient model checking procedure. Second, we describe an effective model finding procedure that symbolically explores a given (possibly infinite) family of symbolic structures in search of an infinite model for a given formula. Finally, we identify a new decidable fragment of first-order logic that extends and subsumes the many-sorted variant of EPR, where satisfiable formulas always have a model representable by a symbolic structure within a known family, making our model finding procedure a decision procedure for that fragment.\n          <\/jats:p>\n          <jats:p>We evaluate our approach on examples from the domains of distributed consensus protocols and of heapmanipulating programs (specifically, linked lists). Our implementation quickly finds infinite counter-models that demonstrate the source of verification failures in a simple way, while state-of-the-art SMT solvers and theorem provers such as Z3, cvc5, and Vampire diverge or return \u201cunknown\u201d.<\/jats:p>","DOI":"10.1145\/3632875","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"970-1000","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5503-5791","authenticated-orcid":false,"given":"Neta","family":"Elad","sequence":"first","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[{"name":"VMware Research, Palo Alto, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Tel Aviv, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01448869"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/581809"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_6"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511974960.002"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_9_1","volume-title":"The SMT-LIB Standard: Version 2.6","author":"Barrett Clark","year":"2017","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org."},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213006002552"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45085-6_32"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_10"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1133-y"},{"key":"e_1_3_2_14_1","volume-title":"The classical decision problem","author":"B\u00f6rger Egon","year":"2001","unstructured":"Egon B\u00f6rger, Erich Gr\u00e4del, and Yuri Gurevich. 2001. The classical decision problem. Springer Science & Business Media."},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271090"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_5"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2019.17"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3419404"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1066100.1066102"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9352-2"},{"issue":"2","key":"e_1_3_2_26_1","first-page":"1","article-title":"The yices smt solver","volume":"2","author":"Dutertre Bruno","year":"2006","unstructured":"Bruno Dutertre and Leonardo De Moura. 2006. The yices smt solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf 2, 2 (2006), 1\u20132.","journal-title":"Tool paper at"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Neta Elad Oded Padon and Sharon Shoham. [n. d.]. An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification (Artifact). https:\/\/doi.org\/10.5281\/zenodo.8404103 10.5281\/zenodo.8404103","DOI":"10.5281\/zenodo.8404103"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","unstructured":"Neta Elad Oded Padon and Sharon Shoham. 2023a. An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification (Artifact). https:\/\/doi.org\/10.5281\/zenodo.10125136 10.5281\/zenodo.10125136","DOI":"10.5281\/zenodo.10125136"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","unstructured":"Neta Elad Oded Padon and Sharon Shoham. 2023b. An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. https:\/\/doi.org\/10.48550\/arXiv.2310.16762 10.48550\/arXiv.2310.16762 arXiv:2310.16762 [cs.PL]","DOI":"10.48550\/arXiv.2310.16762"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","unstructured":"Yotam M. Y. Feldman Oded Padon Neil Immerman Mooly Sagiv and Sharon Shoham. 2017. Bounded Quantifier Instantiation for Checking Inductive Invariants. In TACAS (1) (Lecture Notes in Computer Science Vol. 10205). 76\u201395. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_510.1007\/978-3-662-54577-5_5","DOI":"10.1007\/978-3-662-54577-5_5"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"e_1_3_2_33_1","first-page":"27","article-title":"Ein Spezialfall des Entscheidungsproblems der theoretischen Logik","volume":"2","author":"G\u00f6del Kurt","year":"1932","unstructured":"Kurt G\u00f6del. 1932. Ein Spezialfall des Entscheidungsproblems der theoretischen Logik. Ergebnisse eines mathematischen Kolloquiums 2 (1932), 27\u201328.","journal-title":"Ergebnisse eines mathematischen Kolloquiums"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_9"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_20"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0022481200051513"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_34"},{"key":"e_1_3_2_39_1","first-page":"115","volume-title":"18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021, James Mickens and Renata Teixeira (Eds.). USENIX Association, 115\u2013131. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40885-4_14"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.OPODIS.2016.25"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_21"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535854"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_29"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3022187"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588534"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60178-3_93"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","unstructured":"Bartek Klin and Michal Szynwelski. 2016. SMT Solving for Functional Programming over Infinite Structures. In MSFP (EPTCS Vol. 207). 57\u201375. https:\/\/doi.org\/10.4204\/EPTCS.207.3 10.4204\/EPTCS.207.3","DOI":"10.4204\/EPTCS.207.3"},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_18"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_53_1","unstructured":"Leslie Lamport. 2019. The Paxos Algorithm - or How to Win a Turing Award. https:\/\/lamport.azurewebsites.net\/tla\/paxos-algorithm.html"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45099-3_15"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"issue":"4","key":"e_1_3_2_57_1","first-page":"563","article-title":"Decidability of the monadic predicate calculus with unary function symbols","volume":"32","author":"L\u00f6b Martin","year":"1967","unstructured":"Martin L\u00f6b. 1967. Decidability of the monadic predicate calculus with unary function symbols. Journal of Symbolic Logic 32, 4 (1967), 563.","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37651-1_12"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2306.09436"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290359"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45237-7_10"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_4"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19750210118"},{"key":"e_1_3_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563354"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89960-2_13"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908118"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498712"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.29007\/slrm"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/11.1.97"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","unstructured":"Mathias Preiner Aina Niemetz and Armin Biere. 2017. Counterexample-Guided Model Synthesis. In TACAS (1) (Lecture Notes in Computer Science Vol. 10205). 264\u2013280. https:\/\/doi.org\/10.1007\/978-3-662-54577-5_15 10.1007\/978-3-662-54577-5_15","DOI":"10.1007\/978-3-662-54577-5_15"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.2307\/1995086"},{"key":"e_1_3_2_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-8176-4842-8_1"},{"key":"e_1_3_2_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40970-2_20"},{"key":"e_1_3_2_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9372-6"},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46081-8_5"},{"key":"e_1_3_2_80_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958040"},{"key":"e_1_3_2_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_26"},{"key":"e_1_3_2_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_26"},{"key":"e_1_3_2_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0140-3"},{"key":"e_1_3_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_3_2_85_1","doi-asserted-by":"publisher","unstructured":"Johannes Schoisswohl and Laura Kov\u00e1cs. 2021. Automating Induction by Reflection. In LFMTP (EPTCS Vol. 337). 39\u201354. https:\/\/doi.org\/10.4204\/EPTCS.337.4 10.4204\/EPTCS.337.4","DOI":"10.4204\/EPTCS.337.4"},{"key":"e_1_3_2_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02759780"},{"key":"e_1_3_2_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_2_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_6"},{"key":"e_1_3_2_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158141"},{"key":"e_1_3_2_90_1","volume-title":"Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates","author":"Voigt Marco","year":"2019","unstructured":"Marco Voigt. 2019. Decidable fragments of first-order logic and of first-order linear arithmetic with uninterpreted predicates. Ph. D. Dissertation. Saarland University, Saarbr\u00fccken, Germany."},{"key":"e_1_3_2_91_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_10"},{"key":"e_1_3_2_92_1","first-page":"485","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022","author":"Yao Jianan","year":"2022","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, and Jason Nieh. 2022. DuoAI: Fast, Automated Inference of Inductive Invariants for Verifying Distributed Protocols. In 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 2022, Marcos K. Aguilera and Hakim Weatherspoon (Eds.). USENIX Association, 485\u2013501. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"e_1_3_2_93_1","first-page":"405","volume-title":"OSDI","author":"Yao Jianan","year":"2021","unstructured":"Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh, Suman Jana, and Gabriel Ryan. 2021. DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols. In OSDI. USENIX Association, 405\u2013421."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632875","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632875","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:35Z","timestamp":1751659655000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632875"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":92,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632875"],"URL":"https:\/\/doi.org\/10.1145\/3632875","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}