{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:50Z","timestamp":1780994510407,"version":"3.54.1"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031656293","type":"print"},{"value":"9783031656309","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T00:00:00Z","timestamp":1721865600000},"content-version":"vor","delay-in-days":206,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper lays a practical foundation for using abstract interpretation with an abstract domain that consists of sets of quantified first-order logic formulas. This abstract domain seems infeasible at first sight due to the complexity of the formulas involved and the enormous size of sets of formulas (abstract elements). We introduce an efficient representation of abstract elements, which eliminates redundancies based on a novel syntactic subsumption relation that under-approximates semantic entailment. We develop algorithms and data structures to efficiently compute the join of an abstract element with the abstraction of a concrete state, operating on the representation of abstract elements. To demonstrate feasibility of the domain, we use our data structures and algorithms to implement a symbolic abstraction algorithm that computes the least fixpoint of the best abstract transformer of a transition system, which corresponds to the strongest inductive invariant. We succeed at finding, for example, the least fixpoint for Paxos (which in our representation has 1,438 formulas with <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\forall ^*\\exists ^*\\forall ^*$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:msup>\n                      <mml:mo>\u2200<\/mml:mo>\n                      <mml:mo>\u2217<\/mml:mo>\n                    <\/mml:msup>\n                    <mml:msup>\n                      <mml:mo>\u2203<\/mml:mo>\n                      <mml:mo>\u2217<\/mml:mo>\n                    <\/mml:msup>\n                    <mml:msup>\n                      <mml:mo>\u2200<\/mml:mo>\n                      <mml:mo>\u2217<\/mml:mo>\n                    <\/mml:msup>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> quantification) in time comparable to state-of-the-art property-directed approaches.<\/jats:p>","DOI":"10.1007\/978-3-031-65630-9_5","type":"book-chapter","created":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:01:56Z","timestamp":1721858516000},"page":"86-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Efficient Implementation of\u00a0an\u00a0Abstract Domain of\u00a0Quantified First-Order Formulas"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-4589-2173","authenticated-orcid":false,"given":"Eden","family":"Frenkel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9889-4828","authenticated-orcid":false,"given":"Tej","family":"Chajed","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4209-1635","authenticated-orcid":false,"given":"Oded","family":"Padon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,7,25]]},"reference":[{"key":"5_CR1","doi-asserted-by":"publisher","unstructured":"Ball, T., et al.: Vericon: towards verifying controller programs in software-defined networks. In: O\u2019Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 09\u201311 June 2014, pp. 282\u2013293. ACM (2014). https:\/\/doi.org\/10.1145\/2594291.2594317","DOI":"10.1145\/2594291.2594317"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"5_CR3","unstructured":"Cadar, C., Dunbar, D., Engler, D.R., et\u00a0al.: Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, vol.\u00a08, pp. 209\u2013224 (2008)"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238\u2013252. ACM (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, January 1979, pp. 269\u2013282. ACM Press (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-662-54577-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"YMY Feldman","year":"2017","unstructured":"Feldman, Y.M.Y., Padon, O., Immerman, N., Sagiv, M., Shoham, S.: Bounded quantifier instantiation for checking inductive invariants. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 76\u201395. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_5"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Frenkel, E., Chajed, T., Padon, O., Shoham, S.: Efficient implementation of an abstract domain of quantified first-order formulas (artifact) (2024). https:\/\/doi.org\/10.5281\/zenodo.10938367","DOI":"10.5281\/zenodo.10938367"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Frenkel, E., Chajed, T., Padon, O., Shoham, S.: Efficient implementation of an abstract domain of quantified first-order formulas (extended version) (2024). https:\/\/doi.org\/10.48550\/arXiv.2405.10308","DOI":"10.48550\/arXiv.2405.10308"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-030-76384-8_9","volume-title":"NASA Formal Methods","author":"A Goel","year":"2021","unstructured":"Goel, A., Sakallah, K.: On symmetry and quantification: a new approach to verify distributed protocols. In: Dutle, A., Moscato, M.M., Titolo, L., Mu\u00f1oz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 131\u2013150. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_9"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Goel, A., Sakallah, K.A.: Towards an automatic proof of Lamport\u2019s Paxos. In: FMCAD, pp. 112\u2013122. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_20","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_20"},{"key":"5_CR11","unstructured":"Hance, T., Heule, M., Martins, R., Parno, B.: Finding invariants of distributed systems: It\u2019s a small (enough) world after all. In: Mickens, J., Teixeira, R. (eds.) 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, 12\u201314 April 2021, pp. 115\u2013131. USENIX Association (2021). https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"5_CR12","unstructured":"Hoffmann, J., Koehler, J.: A new method to index and query sets. In: IJCAI, vol.\u00a099, pp. 462\u2013467 (1999)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"756","DOI":"10.1007\/978-3-642-39799-8_53","volume-title":"Computer Aided Verification","author":"S Itzhaky","year":"2013","unstructured":"Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M.: Effectively-propositional reasoning about reachability in linked data structures. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 756\u2013772. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_53"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Karbyshev, A., Bj\u00f8rner, N.S., Itzhaky, S., Rinetzky, N., Shoham, S.: Property-directed inference of universal invariants or proving their absence. J. ACM 64(1), 7:1\u20137:33 (2017). https:\/\/doi.org\/10.1145\/3022187","DOI":"10.1145\/3022187"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-030-99524-9_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"JR Koenig","year":"2022","unstructured":"Koenig, J.R., Padon, O., Shoham, S., Aiken, A.: Inferring Invariants with quantifier alternations: taming the search space explosion. In: TACAS 2022. LNCS, vol. 13243, pp. 338\u2013356. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_18"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"L\u00f6ding, C., Madhusudan, P., Pe\u00f1a, L.: Foundations for natural proofs and quantifier instantiation. Proc. ACM Program. Lang. 2(POPL), 10:1\u201310:30 (2018). https:\/\/doi.org\/10.1145\/3158098","DOI":"10.1145\/3158098"},{"key":"5_CR17","doi-asserted-by":"publisher","unstructured":"Ma, H., Goel, A., Jeannin, J., Kapritsos, M., Kasikci, B., Sakallah, K.A.: I4: incremental inference of inductive invariants for verification of distributed protocols. In: SOSP, pp. 370\u2013384. ACM (2019). https:\/\/doi.org\/10.1145\/3341301.3359651","DOI":"10.1145\/3341301.3359651"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/978-3-030-45237-7_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"U Mathur","year":"2020","unstructured":"Mathur, U., Madhusudan, P., Viswanathan, M.: What\u2019s decidable about program verification modulo axioms? In: TACAS 2020. LNCS, vol. 12079, pp. 158\u2013177. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_10"},{"key":"5_CR19","unstructured":"McMillan, K.: Don\u2019t-care computation using k-clause approximation. In: Proceedings of the IWLS 2005, pp. 153\u2013160 (2005)"},{"key":"5_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-99725-4_4","volume-title":"Static Analysis","author":"KL McMillan","year":"2018","unstructured":"McMillan, K.L., Padon, O.: Deductive verification in decidable fragments with ivy. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 43\u201355. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_4"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Murali, A., Pe\u00f1a, L., Blanchard, E., L\u00f6ding, C., Madhusudan, P.: Model-guided synthesis of inductive lemmas for FOL with least fixpoints. Proc. ACM Program. Lang. 6(OOPSLA2), 1873\u20131902 (2022). https:\/\/doi.org\/10.1145\/3563354","DOI":"10.1145\/3563354"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Padon, O.: Deductive Verification of Distributed Protocols in First-Order Logic. Ph.D. thesis, Tel Aviv University (2019)","DOI":"10.23919\/FMCAD.2018.8603010"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Padon, O., Losa, G., Sagiv, M., Shoham, S.: Paxos made EPR: decidable reasoning about distributed protocols. Proc. ACM Program. Lang. 1(OOPSLA), 108:1\u2013108:31 (2017). https:\/\/doi.org\/10.1145\/3140568","DOI":"10.1145\/3140568"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Padon, O., McMillan, K.L., Panda, A., Sagiv, M., Shoham, S.: Ivy: safety verification by interactive generalization. In: PLDI, pp. 614\u2013630. ACM (2016). https:\/\/doi.org\/10.1145\/2908080.2908118","DOI":"10.1145\/2908080.2908118"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Padon, O., Wilcox, J.R., Koenig, J.R., McMillan, K.L., Aiken, A.: Induction duality: primal-dual search for invariants. Proc. ACM Program. Lang. 6(POPL), 1\u201329 (2022). https:\/\/doi.org\/10.1145\/3498712","DOI":"10.1145\/3498712"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-540-24622-0_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T Reps","year":"2004","unstructured":"Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252\u2013266. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24622-0_21"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Taube, M., et al.: Modularity for decidability of deductive verification with applications to distributed systems. In: PLDI, pp. 662\u2013677. ACM (2018). https:\/\/doi.org\/10.1145\/3192366.3192414","DOI":"10.1145\/3192366.3192414"},{"key":"5_CR29","unstructured":"Thakur, A.V.: Symbolic abstraction: algorithms and applications. Ph.D. thesis, The University of Wisconsin-Madison (2014)"},{"key":"5_CR30","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J.: DuoAI: fast, automated inference of inductive invariants for verifying distributed protocols. In: Aguilera, M.K., Weatherspoon, H. (eds.) 16th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2022, Carlsbad, CA, USA, 11\u201313 July 2022, pp. 485\u2013501. USENIX Association (2022). https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/yao"},{"key":"5_CR31","unstructured":"Yao, J., Tao, R., Gu, R., Nieh, J., Jana, S., Ryan, G.: Distai: data-driven automated invariant learning for distributed protocols. In: OSDI, pp. 405\u2013421. USENIX Association (2021)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65630-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T22:02:42Z","timestamp":1721858562000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65630-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656293","9783031656309"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65630-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"25 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}