AbstractA program correctness checker is an algorithm for checking the output of a computation. That is, given a program and an instance on which the program is run, the checker certifies whether the output of the program on that instance is correct. This paper defines the concept of a program checker. It designs program checkers for a few specific and carefully chosen problems in the class FP of functions computable in polynomial time. Problems in FP for which checkers are presented in this paper include Sorting, Matrix Rank and GCD. It also applies methods of modern cryptography, especially the idea of a probabilistic interactive proof, to the design of program checkers for group theoretic computations.
Two structural theorems are proven here. One is a characterization of problems that can be checked. The other theorem establishes equivalence classes of problems such that whenever one problem in a class is checkable, all problems in the class are checkable. Copyright: Copyright 1995 by ACM, Inc. CR91: D.2.4 [correctness proofs \and reliability]; F.2.0; F.3.1; G.3 [probabilistic algorithms (including Monte Carlo)] Terms: Algorithms, Design, Reliability, Theory, Verification Keywords: Interactive proofs, probabilistic algorithms, program checking, program verification, testing
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
Categories and Subject Descriptors: D.2.4 [Software Engineering]: Program Verification -- correctness proofs; reliability; F.2.0 [Analysis of Algorithms and Problem Complexity]; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; G.3 [Probability and Statistics] -- probabilistic algorithms (including Monte Carlo)
General Terms: Algorithms, Design, Reliability, Theory, Verification
Additional Key Words and Phrases: Interactive proofs, probabilistic algorithms, program checking, program verification, testing
Selected papers that cite this one
- M. Agrawal and V. Arvind. A note on decision versus search for graph automorphism. Information and Computation, 131(2):179-189, 15 December 1996.
- V. Arvind, R. Beigel, and A. Lozano. The complexity of modular graph automorphism. In 15th Annual Symposium on Theoretical Aspects of Computer Science, volume 1373 of Lecture Notes in Computer Science, pages 172-182, Paris France, 25-27 February 1998. Springer.
- Zhi-Zhong Chen and Ming-Yang Kao. Reducing randomness via irrational numbers. In Proceedings of the Twenty-Ninth Annual ACM Symposium on Theory of Computing, pages 200-209, El Paso, Texas, 4-6 May 1997.
- Edith Hemaspaandra, Ashish V. Naik, Mitsunori Ogihara, and Alan L. Selman. P-selective sets and reducing search to decision vs self-reducibility. Journal of Computer and System Sciences, 53(2):194-209, October 1996.
- Izabela Wierzbowska. Checker for data structures which sort elements. Information Processing Letters, 64(5):245-249, 15 December 1997.
Selected references
- Leonard M. Adleman, Ming-Deh Huang, and Kireeti Kompella. Efficient checkers for number-theoretic computations. Information and Computation, 121(1):93-102, 15 August 1995.
- Manuel Blum, Will Evans, Peter Gemmell, Sampath Kannan, and Moni Naor. Checking the correctness of memories. In 32nd Annual Symposium on Foundations of Computer Science, pages 90-99, San Juan, Puerto Rico, 1-4 October 1991. IEEE.
- Manuel Blum and Sampath Kannan. Designing programs that check their work. In Proceedings of the Twenty First Annual ACM Symposium on Theory of Computing, pages 86-97, Seattle, Washington, 15-17 May 1989.
- Manuel Blum, Michael Luby, and Ronitt Rubinfeld. Self-testing/correcting with applications to numerical problems. In Proceedings of the Twenty Second Annual ACM Symposium on Theory of Computing, pages 73-83, Baltimore, Maryland, 14-16 May 1990.
- Stephen A. Cook. A taxonomy of problems with fast parallel algorithms. Information and Control, 64(1-3):2-21, January/February/March 1985.
- Merrick Furst, John Hopcroft, and Eugene Luks. Polynomial-time algorithms for permutation groups. In 21st Annual Symposium on Foundations of Computer Science, pages 36-41, Syracuse, New York, 13-15 October 1980. IEEE.
- Oded Goldreich, Silvio Micali, and Avi Wigderson. Proofs that yield nothing but their validity or all languages in NP have zero-knowledge proof systems. Journal of the ACM, 38(3):691-729, July 1991.
- Carsten Lund, Lance Fortnow, Howard Karloff, and Noam Nisan. Algebraic methods for interactive proof systems. Journal of the ACM, 39(4):859-868, October 1992.
- Adi Shamir. IP = PSPACE. Journal of the ACM, 39(4):869-877, October 1992.
- Martin Tompa and Heather Woll. Random self-reducibility and zero knowledge interactive proofs of possession of information. In 28th Annual Symposium on Foundations of Computer Science, pages 472-482, Los Angeles, California, 12-14 October 1987. IEEE.