合成声音与精确摘要变换器，用于非线性双曲偏微分方程求解器

《Proceedings of the ACM on Programming Languages》：Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers

PDE求解器面临非线性、激波形成及数值伪振荡等问题，需程序分析验证不变式。Phocus首次将抽象解释应用于超调和分方程求解器，通过优化流程合成精确变换器，可验证CFL条件和总变差边界，实验显示其能处理数千网格点且精度显著优于传统方法。

　　

摘要

偏微分方程（PDEs）在科学计算和工程领域中起着至关重要的作用。尽管数值方法使得求解PDEs变得可行，但这些数值求解器仍面临诸多问题，尤其是在处理双曲型PDEs时。这些问题源于多个方面：首先是PDE所描述的物理模型本身，它可能导致诸如冲击波形成等现象；其次是PDE求解器自身的近似方法，这些方法可能会引入虚假的数值误差。这些问题可能导致求解器程序崩溃（由于数值溢出），或者返回精度极低的结果（由于虚假振荡或能量耗散）。此外，许多PDE的非线性特性进一步加剧了这些挑战。另外，PDE求解器还必须遵守某些数值不变性，例如CFL条件。因此，迫切需要対PDE求解器进行程序分析，以确保这些问题不会发生，并且所有不变性始终得到满足。

为了解决这些问题，我们开发了Phocus——这是首个针对双曲型PDE求解器的抽象化解释工具。Phocus能够精确评估非线性PDE解的界限，并验证关键不变性，如CFL条件和解的总变差界限。通过Phocus，可以确认冲击波不会形成、求解器的稳定性以及虚假数值效应的幅度。为了实现对双曲型PDE求解器的有效抽象化分析，Phocus采用了一种基于优化的新方法，为多种有限差分格式生成精确的抽象转换器。为了评估Phocus的性能，我们设计了一组新的PDE基准测试程序，并通过大量实验验证了其显著的精度优势和在数千个网格点上的可扩展性。