{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:07:04Z","timestamp":1790075224306,"version":"4.0.1"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T00:00:00Z","timestamp":1780876800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-23-1-2134"],"award-info":[{"award-number":["N00014-23-1-2134"]}],"id":[{"id":"10.13039\/100000006","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":[[2026,6,8]]},"abstract":"<jats:p>\n                    Backward stability is a desirable property for a well-designed numerical algorithm: given an input, a backward stable floating-point program produces the exact output for a nearby input. While automated tools for bounding the forward error of a numerical program are well-established, few existing tools target backward error analysis. We present a formal framework that enables sound, automated backward error analysis for a broad class of numerical programs. First, we propose a novel generalization of the definition of backward stability that is both compositional and flexible, satisfied by a wide range of floating-point operations. Second, based on this generalization, we develop the category\n                    <jats:bold>Shel<\/jats:bold>\n                    where morphisms model stable numerical programs, and show that structures in\n                    <jats:bold>Shel<\/jats:bold>\n                    support a rich variety of backward error analyses. Third, we implement a tool,\n                    <jats:bold>eggshel<\/jats:bold>\n                    , that automatically searches within a syntactic subcategory of\n                    <jats:bold>Shel<\/jats:bold>\n                    to prove backward stability for a given program. Our algorithm handles many programs with variable reuse, a known challenge in backward error analysis. We prove soundness of our algorithm and use our tool to synthesize backward error bounds for a suite of programs that were previously beyond the reach of automated analysis.\n                  <\/jats:p>","DOI":"10.1145\/3808333","type":"journal-article","created":{"date-parts":[[2026,6,8]],"date-time":"2026-06-08T18:04:09Z","timestamp":1780941849000},"page":"2157-2180","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Synthesizing Backward Error Bounds, Backward"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-6516-1392","authenticated-orcid":false,"given":"Laura","family":"Zielinski","sequence":"first","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8953-7060","authenticated-orcid":false,"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,6,8]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636953"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1137\/20M1334796"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-8453-0"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2010.128"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Valeria Correa Vaz de Paiva. 1989. The Dialectica categories. Ph. D. Dissertation. University of Cambridge Computer Laboratory. doi:10.48456\/tr-213","DOI":"10.48456\/tr-213"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.432.6"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232424"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814317"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/11823230_3"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1137\/0613014"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898718027"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103715"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656456"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/3729324"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/356502.356497"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1137\/0715024"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737959"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/100816"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3230733"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-71177-0_2"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"James Hardy Wilkinson. 2023. Rounding Errors in Algebraic Processes. Society for Industrial and Applied Mathematics Philadelphia PA. doi:10.1137\/1.9781611977523 Originally published 1963.","DOI":"10.1137\/1.9781611977523"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Laura Zielinski and Justin Hsu. 2026. eggshel: A Floating-Point Backward Error Analysis Tool. doi:10.5281\/zenodo.19391349","DOI":"10.5281\/zenodo.19391349"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Laura Zielinski and Justin Hsu. 2026. Supplemental Material for Article \u2018Synthesizing Backward Error Bounds Backward\u2019. doi:10.1145\/3808333","DOI":"10.1145\/3808333"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808333","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3808333","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T10:38:46Z","timestamp":1790073526000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3808333"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6,8]]},"references-count":24,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2026,6,8]]}},"alternative-id":["10.1145\/3808333"],"URL":"https:\/\/doi.org\/10.1145\/3808333","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,6,8]]},"assertion":[{"value":"2025-11-13","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-04-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-06-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}