一句话：提出 Phocus，首个双曲 PDE 求解器的抽象解释，通过合成抽象变换器验证不变式与稳定性。
双曲偏微分方程（PDE）数值求解器会因物理模型中的激波形成以及数值近似引入的伪振荡或耗散而崩溃或失真，非线性使问题更复杂，且求解器必须满足 CFL 等数值不变式。本文提出 Phocus，首个面向双曲 PDE 求解器的抽象解释方法。它采用基于优化的新过程，为多种有限差分格式合成可靠且精确的抽象变换器，从而证明非线性 PDE 解的精确界、CFL 条件与全变差界等关键不变式，验证无激波形成、求解器稳定性及伪数值效应界限。作者构建新的 PDE 基准程序并开展广泛实验，表明 Phocus 在精度上显著提升，并可扩展到数千网格点。
Partial Differential Equations (PDEs) play a ubiquitous role in scientific computing and engineering. While numerical methods make solving PDEs tractable, these numerical solvers encounter several issues, particularly for hyperbolic PDEs. These issues arise from multiple sources including the PDE’s physical model, which can lead to effects like shock wave formation, and the PDE solver’s inherent approximations, which can introduce spurious numerical artifacts. These issues can cause the solver’s program execution to crash (due to overflow) or return results with unacceptable levels of inaccuracy (due to spurious oscillations or dissipation). Moreover, these challenges are compounded by the nonlinear nature of many of these PDEs. In addition, PDE solvers must obey numerical invariants like the CFL condition. Hence there exists a critical need to apply program analysis to PDE solvers to certify such problems do not arise and that invariants are always satisfied. As a solution, we develop Phocus, which is the first abstract interpretation of hyperbolic PDE solvers. Phocus can certify precise bounds on nonlinear PDE solutions and certify key invariants such as the CFL condition and a solution’s total variation bound. Hence Phocus can verify the absence of shock formation, the stability of the solver, and bounds on the amount of spurious numerical effects. To enable effective abstract interpretation of hyperbolic PDE solvers, Phocus uses a novel optimization-based procedure to synthesize precise abstract transformers for multiple finite difference schemes. To evaluate Phocus, we develop a new set of PDE benchmark programs and use them to perform an extensive experimental evaluation which demonstrates Phocus’s significant precision benefits and scalability to several thousand mesh points.
@article{paperbot2912,
title = {Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers},
author = {Jacob Laurel and Ignacio Laguna and Jan Hückelheim},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763088}
}