{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T22:40:59Z","timestamp":1760049659894,"version":"build-2065373602"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783032071057"},{"type":"electronic","value":"9783032071064"}],"license":[{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,6]],"date-time":"2025-10-06T00:00:00Z","timestamp":1759708800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-07106-4_3","type":"book-chapter","created":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:38:02Z","timestamp":1759847882000},"page":"34-61","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Contextual Equality Saturation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-6171-4492","authenticated-orcid":false,"given":"Alexandre","family":"Drewery","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4064-7170","authenticated-orcid":false,"given":"Thomas P.","family":"Jensen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2504-1760","authenticated-orcid":false,"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,6]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Barthe, G., Blazy, S., Laporte, V., Pichardie, D., Trieu, A.: Verified translation validation of static analyses. In: Proceedings of the CSF\u20192017 IEEE 30th CSF. IEEE Computer Society (2017)","DOI":"10.1109\/CSF.2017.16"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Product programs and relational program logics. J. Log. Algebraic Meth. Program. 85(5) (2016)","DOI":"10.1016\/j.jlamp.2016.05.004"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Proceedings of the POPL\u20192004. ACM (2004)","DOI":"10.1145\/964001.964003"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Benton, N.: Semantic equivalence checking for HHVM bytecode. In: Proceedings of the PPDP\u20192018. ACM (2018)","DOI":"10.1145\/3236950.3236975"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Churchill, B.R., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: Proceedings of the PLDI\u20192019. ACM (2019)","DOI":"10.1145\/3314221.3314596"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"De Moura, L.M., Bj\u00f8rner, N.S.: Efficient e-matching for SMT solvers. In: Proceedings of the CADE\u20192021. LNCS, vol.\u00a04603. Springer (2007)","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3) (2005)","DOI":"10.1145\/1066100.1066102"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4) (1980)","DOI":"10.1145\/322217.322228"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Dutta, S., Sarkar, D., Rawat, A., Singh, K.: Validation of loop parallelization and loop vectorization transformations. In: Proceedings of the ENASE\u20192016. SciTePress (2016)","DOI":"10.5220\/0005869501950202"},{"key":"3_CR11","unstructured":"Hack documentation. https:\/\/hacklang.org. Accessed 01 Apr 2024"},{"key":"3_CR12","unstructured":"Havlak, P.: Construction of thinned gated single-assignment form. In: Proceedings of the LCPC\u20191993. LNCS, vol.\u00a0768. Springer (1993)"},{"key":"3_CR13","unstructured":"HHVM documentation. https:\/\/hhvm.com. Accessed 01 Apr 2024"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Reb\u00ealo, H.: SymDiff: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712\u2013717. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_54","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7) (2009)","DOI":"10.1145\/1538788.1538814"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Nandi, C., et al.: Synthesizing structured CAD models with equality saturation and inverse transformations. In: Proceedings of the PLDI\u20192020, pp. 31\u201344. ACM (2020)","DOI":"10.1145\/3385412.3386012"},{"key":"3_CR17","unstructured":"Paleczny, M., Vick, C.A., Click, C.: The Java hotspot server compiler. In: Proceedings of the Java Virtual Machine Research and Technology Symposium. USENIX (2001)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Premtoon, V., Koppel, J., Solar-Lezama, A.: Semantic code search via equational reasoning. In: Proceedings of the PLDI\u20192020. ACM (2020)","DOI":"10.1145\/3385412.3386001"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-11970-5_13","volume-title":"Compiler Construction","author":"S Rideau","year":"2010","unstructured":"Rideau, S., Leroy, X.: Validating register allocation and spilling. In: Gupta, R. (ed.) CC 2010. LNCS, vol. 6011, pp. 224\u2013243. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11970-5_13"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-based translation validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 737\u2013742. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_59","DOI":"10.1007\/978-3-642-22110-1_59"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2) (1975)","DOI":"10.1145\/321879.321884"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. Log. Methods Comput. Sci. 7(1) (2011)","DOI":"10.2168\/LMCS-7(1:10)2011"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"VanHattum, A., Nigam, R., Lee, V.T., Bornholt, J., Sampson, A.: Vectorization for digital signal processors via equality saturation. In: Proceedings of the ASPLOS\u20192021, pp. 874\u2013886. ACM (2021)","DOI":"10.1145\/3445814.3446707"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Verdoolaege, S., Janssens, G., Bruynooghe, M.: Equivalence checking of static affine programs using widening to handle recurrences. ACM Trans. Program. Lang. Syst. 34(3) (2012)","DOI":"10.1145\/2362389.2362390"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Wang, Y.R., Hutchison, S., Suciu, D., Howe, B., Leang, J.: SPORES: sum-product optimization via relational equality saturation for large scale linear algebra. Proc. VLDB Endow. 13(11) (2020)","DOI":"10.14778\/3407790.3407799"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Willsey, M., Nandi, C., Wang, Y., Flatt, O., Tatlock, Z., Panchekha, P.: EGG: fast and extensible equality saturation. In: Proceedings of the POPL\u20192021. ACM (2021)","DOI":"10.1145\/3434304"},{"key":"3_CR27","unstructured":"Yang, Y., Phothilimthana, P.M., Wang, Y.R., Willsey, M., Roy, S., Pienaar, J.: Equality saturation for tensor graph superoptimization. In: Proceedings of the MLSys 2021 (2021)"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35\u201351. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_5","DOI":"10.1007\/978-3-540-68237-0_5"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07106-4_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T22:03:34Z","timestamp":1760047414000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07106-4_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,6]]},"ISBN":["9783032071057","9783032071064"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07106-4_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025,10,6]]},"assertion":[{"value":"6 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Static Analysis Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 October 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 October 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/2025.splashcon.org\/home\/sas-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}