{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:25:13Z","timestamp":1770297913135,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031377020","type":"print"},{"value":"9783031377037","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,7,18]],"date-time":"2023-07-18T00:00:00Z","timestamp":1689638400000},"content-version":"vor","delay-in-days":198,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Quantifier elimination (qelim) is used in many automated reasoning tasks including program synthesis, exist-forall solving, quantified SMT, Model Checking, and solving Constrained Horn Clauses (CHCs). Exact qelim is computationally expensive. Hence, it is often approximated. For example, Z3 uses \u201clight\u201d pre-processing to reduce the number of quantified variables. CHC-solver Spacer uses model-based projection (MBP) to under-approximate qelim relative to a given model, and over-approximations of qelim can be used as abstractions.<\/jats:p><jats:p>In this paper, we present the QEL framework for fast approximations of qelim. QEL provides a uniform interface for both quantifier reduction and model-based projection. QEL builds on the egraph data structure \u2013 the core of the EUF decision procedure in SMT \u2013 by casting quantifier reduction as a problem of choosing <jats:italic>ground<\/jats:italic> (i.e., variable-free) representatives for equivalence classes. We have used QEL to implement MBP for the theories of Arrays and Algebraic Data Types (ADTs). We integrated QEL and our new MBP in Z3 and evaluated it within several tasks that rely on quantifier approximations, outperforming state-of-the-art.<\/jats:p>","DOI":"10.1007\/978-3-031-37703-7_4","type":"book-chapter","created":{"date-parts":[[2023,7,17]],"date-time":"2023-07-17T17:02:15Z","timestamp":1689613335000},"page":"64-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Fast Approximations of\u00a0Quantifier Elimination"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6098-3895","authenticated-orcid":false,"given":"Isabel","family":"Garcia-Contreras","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2789-5997","authenticated-orcid":false,"given":"V. K. Hari","family":"Govind","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7226-3526","authenticated-orcid":false,"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5964-6792","authenticated-orcid":false,"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,7,18]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","unstructured":"Alt, L., Blicha, M., Hyv\u00e4rinen, A.E.J., Sharygina, N.: SolCMC: Solidity Compiler\u2019s Model Checker. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7\u201310, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13371, pp. 325\u2013338. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_16","DOI":"10.1007\/978-3-031-13185-1_16"},{"key":"4_CR2","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"4_CR3","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"Clark Barrett","year":"2018","unstructured":"Barrett, Clark, Tinelli, Cesare: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner, N.S., Janota, M.: Playing with quantified satisfaction. In: Fehnker, A., McIver, A., Sutcliffe, G., Voronkov, A. (eds.) 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24\u201328, 2015. EPiC Series in Computing, vol. 35, pp. 15\u201327. EasyChair (2015). https:\/\/doi.org\/10.29007\/vv21","DOI":"10.29007\/vv21"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Chang, B.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) Verification, Model Checking, and Abstract Interpretation, 6th International Conference, VMCAI 2005, Paris, France, January 17\u201319, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3385, pp. 147\u2013163. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_11","DOI":"10.1007\/978-3-540-30579-8_11"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. J. ACM 52(3), 365\u2013473 (may 2005). https:\/\/doi.org\/10.1145\/1066100.1066102","DOI":"10.1145\/1066100.1066102"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8559, pp. 737\u2013744. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"4_CR9","unstructured":"Dutertre, B.: Solving Exists\/Forall Problems with Yices. In: Workshop on Satisfiability Modulo Theories (2015). https:\/\/yices.csl.sri.com\/papers\/smt2015.pdf"},{"key":"4_CR10","doi-asserted-by":"publisher","unstructured":"Gange, G., Navas, J.A., Schachte, P., S\u00f8ndergaard, H., Stuckey, P.J.: An abstract domain of uninterpreted functions. In: Jobstmann, B., Leino, K.R.M. (eds.) Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17\u201319, 2016. Proceedings. Lecture Notes in Computer Science, vol. 9583, pp. 85\u2013103. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_4","DOI":"10.1007\/978-3-662-49122-5_4"},{"key":"4_CR11","doi-asserted-by":"publisher","unstructured":"Gasc\u00f3n, A., Subramanyan, P., Dutertre, B., Tiwari, A., Jovanovic, D., Malik, S.: Template-based circuit understanding. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, October 21\u201324, 2014, pp. 83\u201390. IEEE (2014). https:\/\/doi.org\/10.1109\/FMCAD.2014.6987599","DOI":"10.1109\/FMCAD.2014.6987599"},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Tiwari, A., Necula, G.C.: Join algorithms for the theory of uninterpreted functions. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, 24th International Conference, Chennai, India, December 16\u201318, 2004, Proceedings. Lecture Notes in Computer Science, vol. 3328, pp. 311\u2013323. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-30538-5_26","DOI":"10.1007\/978-3-540-30538-5_26"},{"key":"4_CR13","unstructured":"Gurfinkel, A., Ruemmer, P., Fedyukovich, G., Champion, A.: CHC-COMP. https:\/\/chc-comp.github.io\/ (2018)"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Hojjat, H., R\u00fcmmer, P.: The ELDARICA horn solver. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pp. 1\u20137. IEEE (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603013","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Joshi, R., Nelson, G., Randall, K.H.: Denali: A goal-directed superoptimizer. In: Knoop, J., Hendren, L.J. (eds.) Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17\u201319, 2002, pp. 304\u2013314. ACM (2002). https:\/\/doi.org\/10.1145\/512529.512566","DOI":"10.1145\/512529.512566"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Bj\u00f8rner, N.S., Gurfinkel, A., McMillan, K.L.: Compositional verification of procedural programs using horn clauses over integers and arrays. In: Kaivola, R., Wahl, T. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27\u201330, 2015, pp. 89\u201396. IEEE (2015). https:\/\/doi.org\/10.5555\/2893529.2893548","DOI":"10.5555\/2893529.2893548"},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8559, pp. 17\u201334. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: Zorn, B.G., Aiken, A. (eds.) Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5\u201310, 2010, pp. 316\u2013329. ACM (2010). https:\/\/doi.org\/10.1145\/1806596.1806632","DOI":"10.1145\/1806596.1806632"},{"key":"4_CR19","doi-asserted-by":"publisher","unstructured":"de Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"4_CR20","doi-asserted-by":"publisher","unstructured":"Nelson, G., Oppen, D.C.: Fast decision algorithms based on union and find. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pp. 114\u2013119. IEEE Computer Society (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.12","DOI":"10.1109\/SFCS.1977.12"},{"issue":"2","key":"4_CR21","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979). https:\/\/doi.org\/10.1145\/357073.357079","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR22","doi-asserted-by":"publisher","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: A new approach to optimization. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. p. 264\u2013276. POPL \u201909, Association for Computing Machinery, New York, NY, USA (2009). https:\/\/doi.org\/10.1145\/1480881.1480915","DOI":"10.1145\/1480881.1480915"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: A new approach to optimization. Log. Methods Comput. Sci. 7(1) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(1:10)2011","DOI":"10.2168\/LMCS-7(1:10)2011"},{"key":"4_CR24","doi-asserted-by":"publisher","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: egg: Fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL), 1\u201329 (2021). https:\/\/doi.org\/10.1145\/3434304","DOI":"10.1145\/3434304"}],"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-37703-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,26]],"date-time":"2023-08-26T11:02:59Z","timestamp":1693047779000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-37703-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031377020","9783031377037"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-37703-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"18 July 2023","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":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 July 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.i-cav.org\/2023\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"hotcrp","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"261","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"67","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}