{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T06:26:17Z","timestamp":1770445577313,"version":"3.49.0"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/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":[[2025,1,7]]},"abstract":"<jats:p>First-order logic has proved to be a versatile and expressive tool as the basis of abstract modeling languages. Used to verify complex systems with unbounded domains, such as heap-manipulating programs and distributed protocols, first-order logic, and specifically uninterpreted functions and quantifiers, strike a balance between expressiveness and amenity to automation. However, first-order logic semantics may differ in important ways from the intended semantics of the modeled system, due to the inability to distinguish between finite and infinite first-order structures, for example, or the undefinability of well-founded relations in first-order logic. This semantic gap may give rise to spurious states and unreal behaviors, which only exist as an artifact of the first-order abstraction and impede the verification process.<\/jats:p>\n                  <jats:p>In this paper we take a step towards bridging this semantic gap. We present an approach for soundly refining the first-order abstraction according to either well-founded semantics or finite-domain semantics, utilizing induction axioms for an abstract order relation, a common primitive in verification. We first formalize sound axiom schemata for each of the aforementioned semantics, based on well-founded induction. Second, we show how to use spurious counter-models, which are necessarily infinite, to guide the instantiation of these axiom schemata. Finally, we present a sound and complete reduction of well-founded semantics and finite-domain semantics to standard semantics in the recently discovered Ordered Self-Cycle (OSC) fragment of first-order logic, and prove that satisfiability under these semantics is decidable in OSC.<\/jats:p>\n                  <jats:p>We implement a prototype tool to evaluate our approach, and test it on various examples where spurious models arise, from the domains of distributed protocols and heap-manipulating programs. Our tool quickly finds the necessary axioms to refine the semantics, and successfully completes the verification process, eliminating the spurious system states that blocked progress.<\/jats:p>","DOI":"10.1145\/3704853","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"479-508","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Axe \u2019Em: Eliminating Spurious States with Induction Axioms"],"prefix":"10.1145","volume":"9","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\/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":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594317"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_4_2","volume-title":"The SMT-LIB Standard: Version 2.6. Technical Report","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_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603091"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-8928-6_23"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.2307\/2271090"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3428229"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_27"},{"issue":"91","key":"e_1_3_2_10_2","first-page":"300","article-title":"Theorem proving in arithmetic without multiplication","volume":"7","author":"Cooper David C","year":"1972","unstructured":"David C Cooper. 1972. Theorem proving in arithmetic without multiplication. Machine intelligence 7, 91-99 (1972), 300. https:\/\/doi.org\/10.1007\/10930755_5 10.1007\/10930755_5.","journal-title":"Machine intelligence"},{"key":"e_1_3_2_11_2","first-page":"17:1","volume-title":"MFCS (LIPIcs","author":"Danielski Daniel","year":"2019","unstructured":"Daniel Danielski and Emanuel Kieronski. 2019. Finite Satisfiability of Unary Negation Fragment with Transitivity. In MFCS (LIPIcs, Vol. 138). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 17:1\u201317:15. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2019.17 10.4230\/LIPIcs.MFCS.2019.17."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/361179.361202"},{"key":"e_1_3_2_14_2","first-page":"1","volume-title":"Studies in Logic and the Foundations of Mathematics","author":"Doner John E","year":"1978","unstructured":"John E Doner, Andrzej Mostowski, and Alfred Tarski. 1978. The Elementary Theory of Well-Ordering\u2014A Metamathematical Study\u2014. In Studies in Logic and the Foundations of Mathematics. Vol. 96. Elsevier, 1\u201354."},{"key":"e_1_3_2_15_2","article-title":"An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification","author":"Elad Neta","year":"2023","unstructured":"Neta Elad, Oded Padon, and Sharon Shoham. 2023. An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. CoRR abs\/2310.16762 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2310.16762 10.48550\/ARXIV.2310.16762 https:\/\/arxiv.org\/abs\/2310.16762.","journal-title":"CoRR"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632875"},{"key":"e_1_3_2_17_2","unstructured":"Neta Elad and Sharon Shoham. [n. d.]. Axe \u2019Em: Eliminating Spurious States with Induction Axioms (Artifact). https:\/\/doi.org\/10.5281\/zenodo.13912208 10.5281\/zenodo.13912208."},{"key":"e_1_3_2_18_2","unstructured":"Neta Elad and Sharon Shoham. 2024. Axe \u2019Em: Eliminating Spurious States with Induction Axioms. (2024). https:\/\/doi.org\/10.48550\/ARXIV.2410.18671 10.48550\/ARXIV.2410.18671 https:\/\/arxiv.org\/abs\/2410.18671."},{"key":"e_1_3_2_19_2","unstructured":"Neta Elad and Sharon Shoham. 2024. Axe \u2019Em: Eliminating Spurious States with Induction Axioms (Artifact). https:\/\/doi.org\/10.5281\/zenodo.13912279 10.5281\/zenodo.13912279."},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","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_5 10.1007\/978-3-662-54577-5_5.","DOI":"10.1007\/978-3-662-54577-5_5"},{"key":"e_1_3_2_21_2","first-page":"112","volume-title":"FMCAD","author":"Goel Aman","year":"2021","unstructured":"Aman Goel and Karem A. Sakallah. 2021. Towards an Automatic Proof of Lamport\u2019s Paxos. In FMCAD. IEEE, 112\u2013122. https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_20 10.34727\/2021\/isbn.978-3-85448-046-4_20."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_8"},{"key":"e_1_3_2_23_2","first-page":"1","volume-title":"FMCAD","author":"Hajd\u00fa M\u00e1rton","year":"2021","unstructured":"M\u00e1rton Hajd\u00fa, Petra Hozzov\u00e1, Laura Kov\u00e1cs, and Andrei Voronkov. 2021. Induction with Recursive Definitions in Superposition. In FMCAD. IEEE, 1\u201310. https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_34 10.34727\/2021\/isbn.978-3-85448-046-4_34."},{"key":"e_1_3_2_24_2","article-title":"Incremental Proof Development in Dafny with Module-Based Induction","author":"Ho Son","year":"2024","unstructured":"Son Ho and Cl\u00e9ment Pit-Claudel. 2024. Incremental Proof Development in Dafny with Module-Based Induction. CoRR abs\/2401.16233 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2401.16233 10.48550\/ARXIV.2401.16233 https:\/\/arxiv.org\/abs\/2401.16233.","journal-title":"CoRR"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40885-4_14"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_21"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66263-3_22"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535854"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_53"},{"key":"e_1_3_2_30_2","article-title":"A note on the theory of well orders","author":"Jer\u00e1bek Emil","year":"2024","unstructured":"Emil Jer\u00e1bek. 2024. A note on the theory of well orders. CoRR abs\/2405.05779 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2405.05779 10.48550\/ARXIV.2405.05779 https:\/\/arxiv.org\/abs\/2405.05779.","journal-title":"CoRR"},{"key":"e_1_3_2_31_2","first-page":"1","volume-title":"Proc. ACM Program. Lang","author":"Hari Govind V. K.","year":"2022","unstructured":"Hari Govind V. K., Sharon Shoham, and Arie Gurfinkel. 2022. Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. ACM Program. Lang. 6, POPL (2022), 1\u201329. https:\/\/doi.org\/10.1145\/3498722 10.1145\/3498722."},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_18"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111048"},{"key":"e_1_3_2_36_2","volume-title":"A decision procedure for well-founded reachability. Technical Report. Technical Report MSR-TR-2007-43","author":"Lahiri Shuvendu K","year":"2007","unstructured":"Shuvendu K Lahiri and Shaz Qadeer. 2007. A decision procedure for well-founded reachability. Technical Report. Technical Report MSR-TR-2007-43, Microsoft Research."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328461"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/279227.279229"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27940-9_21"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90027-6"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158098"},{"key":"e_1_3_2_43_2","article-title":"Proving Cutoff Bounds for Safety Properties in First-Order Logic","author":"Lotan Raz","year":"2024","unstructured":"Raz Lotan, Eden Frenkel, and Sharon Shoham. 2024. Proving Cutoff Bounds for Safety Properties in First-Order Logic. CoRR abs\/2408.10685 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2408.10685 10.48550\/ARXIV.2408.10685 https:\/\/arxiv.org\/abs\/2408.10685.","journal-title":"CoRR"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_4"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563354"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3140568"},{"key":"e_1_3_2_47_2","volume-title":"Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow). Lecture Notes in Computer Science, Vol. 828","author":"Paulson Lawrence C.","year":"1994","unstructured":"Lawrence C. Paulson. 1994. Isabelle - A Generic Theorem Prover (with a contribution by T. Nipkow). Lecture Notes in Computer Science, Vol. 828. Springer. https:\/\/doi.org\/10.1007\/BFB0030541 10.1007\/BFB0030541."},{"key":"e_1_3_2_48_2","first-page":"1","article-title":"Decidability of second-order theories and automata on infinite trees","volume":"141","author":"Rabin Michael O","year":"1969","unstructured":"Michael O Rabin. 1969. Decidability of second-order theories and automata on infinite trees. Transactions of the american Mathematical Society 141 (1969), 1\u201335. https:\/\/doi.org\/10.2307\/1995086 10.2307\/1995086.","journal-title":"Transactions of the american Mathematical Society"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_26"},{"key":"e_1_3_2_51_2","doi-asserted-by":"crossref","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_52_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056620"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02759780"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-10769-6_9"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_2_56_2","unstructured":"The Coq Development Team. 2024. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.11551307 10.5281\/zenodo.11551307."},{"key":"e_1_3_2_57_2","unstructured":"The Open Logic Project. [n. d.]. Frame Definability. https:\/\/builds.openlogicproject.org\/content\/normal-modal-logic\/frame-definability\/frame-definability.pdf"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.5555\/1593511"},{"key":"e_1_3_2_59_2","first-page":"485","volume-title":"16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, July 11-13, 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_60_2","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."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-24950-1_16"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704853","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704853","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:00Z","timestamp":1770200160000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704853"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704853"],"URL":"https:\/\/doi.org\/10.1145\/3704853","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-08","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}