New Directions in Program Checking

这个项目将研究程序检查的概念，这是一种获得对程序输出的信心的技术。程序检查的传统替代方法是很难做到的程序验证和不能提供数学保证的程序测试。程序检查是一种健康的折衷——为问题设计检查器的难度与为问题设计算法的难度一样大，但检查提供了对输出正确性的精确保证。其中一个主要目标将是为目前通过未经证实的启发式方法解决的问题设计检查器。此外，有效和实用的检查程序将实现在科学计算问题，特别强调检查软件包线性规划，线性代数问题，常微分方程和偏微分方程。本研究的另一个主要推力将是探索交互证明和随机自约性相关概念对程序检查新结果的影响。这里考虑的问题之一是可满足性问题是否可检查。在不久的将来，编写检查程序作为软件设计的一部分可能会成为标准做法，本研究旨在了解程序检查的基础。//

This project will investigate the concept of program checking, which is a technique for gaining confidence in the output of a program. The traditional alternatives to program checking are program verification, which is hard to do, and program testing, which does not provide mathematical guarantees. Program checking strikes a healthy compromise--designing a checker for a problem is only as difficult as designing an algorithm for it, but checking provides precise guarantees about output correctness. One of the major goals will be to design checkers for problems which are currently solved by unproven heuristics. Also, efficient and practical checkers will be implemented for problems in scientific computing, with special emphasis on checking software packages for linear programming, problems in linear algebra, and ordinary and partial differential equations. The other major thrust of this research will be to explore the implications to program checking of new results on the related concepts of interactive proofs and random self reducibility. Among the questions considered here will be whether the satisfiability problem is checkable. Writing a checker as part of designing software may become standard practice in the near future, and this research aims to understand the foundations of program checking.//