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.//