{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:24:57Z","timestamp":1787592297670,"version":"build-2736575974"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1755880"],"award-info":[{"award-number":["CCF-1755880"]}],"id":[{"id":"10.13039\/100000001","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,4,9]]},"abstract":"<jats:p>\n                    Many interesting program properties involve the execution of\n                    <jats:italic toggle=\"yes\">multiple<\/jats:italic>\n                    programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency. One strategy for verifying such\n                    <jats:italic toggle=\"yes\">relational properties<\/jats:italic>\n                    is to construct and reason about an intermediate program whose correctness implies that the individual programs exhibit those properties. A key challenge in building an intermediate program is finding a good\n                    <jats:italic toggle=\"yes\">alignment<\/jats:italic>\n                    of the original programs. An alignment puts subparts of the original programs into correspondence so that their similarities can be exploited in order to simplify verification. We propose an approach to intermediate program construction that uses e-graphs, equality saturation, and algebraic realignment rules to efficiently represent and build programs amenable to automated verification. A key ingredient of our solution is a novel data-driven extraction technique that uses execution traces of candidate intermediate programs to identify solutions that are semantically well-aligned. We have implemented a relational verification engine based on our proposed approach, called\n                    <jats:sc>KestRel<\/jats:sc>\n                    , and use it to evaluate our approach over a suite of benchmarks taken from the relational verification literature.\n                  <\/jats:p>","DOI":"10.1145\/3720474","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1073-1100","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["KestRel: Relational Verification using E-Graphs for Program Alignment"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2697-2145","authenticated-orcid":false,"given":"Robert","family":"Dickerson","sequence":"first","affiliation":[{"name":"Purdue University, Computer Science, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-4833-1496","authenticated-orcid":false,"given":"Prasita","family":"Mukherjee","sequence":"additional","affiliation":[{"name":"Purdue University, Computer Science, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1016-6261","authenticated-orcid":false,"given":"Benjamin","family":"Delaware","sequence":"additional","affiliation":[{"name":"Purdue University, Computer Science, West Lafayette, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571213"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2016.11"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_3"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3470569"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9457-5"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360567"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.7"},{"key":"e_1_3_1_17_1","volume-title":"Introduction to algorithms","author":"Cormen Thomas H.","year":"2009","unstructured":"Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. 2009. Introduction to algorithms, third edition (3rd ed.). The MIT Press."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689756"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53413-7_8"},{"key":"e_1_3_1_21_1","unstructured":"Robert Dickerson Prasita Mukherjee and Benjamin Delaware. 2025a. KestRel. https:\/\/github.com\/rcdickerson\/kestrel\/tree\/oopsla-2025"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Robert Dickerson Prasita Mukherjee and Benjamin Delaware. 2025b. KestRel: Relational verification using e-graphs for program alignment. https:\/\/doi.org\/10.5281\/zenodo.14942558 10.5281\/zenodo.14942558","DOI":"10.5281\/zenodo.14942558"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371081"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-011-1793-7_4"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264278"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656403"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"W Keith Hastings. 1970. Monte Carlo sampling methods using Markov chains and their applications. (1970). https:\/\/doi.org\/10.1093\/biomet\/57.1.97 10.1093\/biomet\/57.1.97","DOI":"10.1093\/biomet\/57.1.97"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_9"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_13"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/909447"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509509"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837655"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/321879.321884"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480915"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.14778\/3407790.3407799"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908125"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720474","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720474","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720474","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:31:01Z","timestamp":1787589061000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720474"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":53,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720474"],"URL":"https:\/\/doi.org\/10.1145\/3720474","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}