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