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 Shel where morphisms model stable numerical programs, and show that structures in Shel support a rich variety of backward error analyses. Third, we implement a tool, eggshel, that automatically searches within a syntactic subcategory of Shel 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.

翻译：后向稳定性是设计良好的数值算法的一个理想特性：给定输入，一个后向稳定的浮点程序对于邻近的输入会产生精确的输出。尽管用于界定数值程序前向误差的自动化工具已相当成熟，但现有工具很少针对后向误差分析。我们提出了一个形式化框架，能够对一大类数值程序进行可靠、自动的后向误差分析。首先，我们提出了后向稳定性定义的一个新颖推广，该定义既具有组合性又具有灵活性，适用于广泛的浮点运算。其次，基于这一推广，我们构建了Shel范畴，其中的态射模拟稳定的数值程序，并展示了Shel中的结构支持多种丰富的后向误差分析。第三，我们实现了一个工具eggshel，它能在Shel的语法子范畴内自动搜索，以证明给定程序的后向稳定性。我们的算法能处理许多涉及变量复用的程序，这是后向误差分析中的一个已知难题。我们证明了算法的可靠性，并利用该工具为一系列此前超出自动分析能力的程序合成了后向误差界。