Collaborative Research: FMitF: Track I: Formally Verified Numerical Methods

当计算机算法计算物理系统的行为时-行星，自动驾驶汽车，火箭，wi-fi天线，药物-有些数学方程无法精确求解。 因此，算法可以根据需要精确地近似答案。 数值分析是计算这些算法的准确性的科学。在某种类型的计算中，需要的精度越高，计算答案所需的时间就越长。 当一个人绝对需要提前知道答案的准确性时，传统的数值方法很难联合收割机组合成一个完整和可信的解决方案。 该项目的创新之处在于：（1）将所有关于数值软件的推理集成到一个系统中;（2）将从数学到软件代码的所有层次的推理连接起来，产生一个端到端的正确性和准确性保证;以及（3）以数学定理的形式产生这种保证，其证明可以完全自动检查。 该项目更广泛的意义和重要性是科学和经济的：开发的新方法和工具可以（1）防止通过传统手段诊断可能非常昂贵的软件错误;（2）允许使用更快的算法（当一个人现在可以证明他们是准确的）;保证控制软件的安全性-关键应用，如飞机和车辆控制。该项目采取分层的方法，以基本验证的正确性和准确性，数值软件-也就是说，关于程序（不仅仅是算法）的正式的机器检查证明，除了解释集架构的规范之外没有任何假设。研究人员在每一层建立、改进和使用适当的工具：离散算法的真实的证明;浮点算法如何逼近实数算法;浮点算法的C程序实现的推理;把所有的证据连接起来该奖项反映了NSF的法定使命，并被认为是值得通过使用基金会的知识价值和更广泛的影响审查标准。

When computer algorithms calculate the behavior of physical systems -- planets, self-driving cars, rockets, wi-fi antennas, medicines – some of the mathematical equations can't be solved exactly. Thus, the algorithms approximate the answers as precisely as needed. Numerical analysis is the science of calculating how accurate these algorithms are. The more precision is needed in a certain type of computation, the more time it takes to compute the answer. When one absolutely needs to know in advance how accurate the answers will be, traditional numerical methods are hard to combine into a complete and trustworthy solution. This project's novelties are (1) to integrate all the reasoning about numerical software into a single system, (2) to connect all the levels of reasoning, from mathematics down to software code, producing an end-to-end guarantee of correctness and accuracy, and (3) to produce that guarantee in the form of a mathematical theorem whose proof can be checked fully automatically. The project's broader significance and importance are both scientific and economic: the novel methods and tools developed can (1) prevent software bugs that can be extremely expensive to diagnose by conventional means; (2) allow faster algorithms to be used (when one can now prove that they are accurate); and (3) assure the safety of control software in safety-critical applications such as aircraft and vehicle control.The project takes a layered approach to foundational verification of correctness and accuracy of numerical software---that is, formal machine-checked proofs about programs (not just algorithms), with no assumptions except specifications of instruction-set architectures. The researchers build, improve, and use appropriate tools at each layer: proving in the real numbers about discrete algorithms; proving how floating-point algorithms approximate real-number algorithms; reasoning about C program implementation of floating-point algorithms; and connecting all proofs end-to-end in the Coq proof assistant.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.