Designing programs that check their work

ABSTRACT

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

REFERENCES

• 1: Leonard M. Adleman , Ming-Deh Huang , Kireeti Kompella, Efficient checkers for number-theoretic computations, Information and Computation, v.121 n.1, p.93-102, Aug. 15, 1995 [doi>10.1006/inco.1995.1125]
• 2: László Babai , Shlomo Moran, Arthur-Merlin games: a randomized proof system, and a hierarchy of complexity class, Journal of Computer and System Sciences, v.36 n.2, p.254-276, April 1988 [doi>10.1016/0022-0000(88)90028-1]
• 3: ~BARW~SE, J. 1989. Mathematical proofs of computer system correctness. Notices AMS 36, 7.
• 4: Donald Beaver , J. Feigenbaum, Hiding instances in multioracle queries, Proceedings of the seventh annual symposium on Theoretical aspects of computer science, p.37-48, February 1990, Rouen, France
• 5: Richard Beigel , Joan Feigenbaum, On being incoherent without being very hard, Computational Complexity, v.2 n.1, p.1-17, 1992 [doi>10.1007/BF01276436]
• 6: Manuel Blum , Will Evans , Peter Gemmell , Sampath Kannan , Moni Naor, Checking the correctness of memories, Proceedings of the 32nd annual symposium on Foundations of computer science, p.90-99, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185352]
• 7: M. Blum , S. Kanna, Designing programs that check their work, Proceedings of the twenty-first annual ACM symposium on Theory of computing, p.86-97, May 14-17, 1989, Seattle, Washington, United States [doi>10.1145/73007.73015]
• 8: M. Blum , M. Luby , R. Rubinfeld, Self-testing/correcting with applications to numerical problems, Proceedings of the twenty-second annual ACM symposium on Theory of computing, p.73-83, May 13-17, 1990, Baltimore, Maryland, United States [doi>10.1145/100216.100225]
• 9: Robert S. Boyer , J. Strother Moore, The Correctness Problem in Computer Science, Academic Press, Inc., Orlando, FL, 1982
• 10: ~BUDD, T. m., AND ANGLUIN, D. 1982. Two notions of correctness and their relation to testing. ~Acta Inf. 18, 31-45.
• 11: Stephen A. Cook, A taxonomy of problems with fast parallel algorithms, Information and Control, v.64 n.1-3, p.2-22, Jan./Feb./March 1985 [doi>10.1016/S0019-9958(85)80041-3]
• 12: Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
• 13: Richard A. DeMillo , W. Michael McCracken , R. J. Martin , John F. Passafiume, Software testing and evaluation, Benjamin-Cummings Publishing Co., Inc., Redwood City, CA, 1987
• 14: ~FEIGENBAUM, J. 1993. Locally random reductions in interactive complexity theory. In Ad- ~vances in Computational Complexity, DIMACS Series ill Discrete Mathemattcs and Theoretical ~Computer Science, vol. 13. AMS, Providence, R.I., pp. 73-98.
• 15: Joan Feigenbaum , Lance Fortnow, Random-self-reducibility of complete sets, SIAM Journal on Computing, v.22 n.5, p.994-1005, Oct. 1993 [doi>10.1137/0222061]
• 16: ~FREIVALDS, R. 1979. Fast probabilistic algorithms. In Mathemaucal Formulations of CS. Lec- ~ture Notes in Computer Science, vol. 74. Springer-Verlag, New York, pp. 57-69.
• 17: ~FURST, M., HOPCROFT, J. E., AND LUKS, E. 1980. Polynomial-time algorithms for permutation ~groups. In Proceedings of the 21st IEEE Symposium on Foundations of Computer Science. IEEE ~Computer Society, Los Alamitos, Calif., pp. 36-41.
• 18: Oded Goldreich , Silvio Micali , Avi Wigderson, Proofs that yield nothing but their validity or all languages in NP have zero-knowledge proof systems, Journal of the ACM (JACM), v.38 n.3, p.690-728, July 1991 [doi>10.1145/116825.116852]
• 19: S. Goldwasser , S. Micali , C. Rackoff, The knowledge complexity of interactive proof systems, SIAM Journal on Computing, v.18 n.1, p.186-208, Feb. 1989 [doi>10.1137/0218012]
• 20: ~GOLDWASSER, S., AND SIPSER, M. 1989. Public coins vs. private coins in interactive proof ~systems. In Advances m Computing Research--Vol. 5.' Randomness and Computation. JAI Press, ~Greenwich, Conn., pp. 73-90.
• 21: ~GORENSTEIN, D. 1982. Finite Simple Groups--An Introduction to Their Classification. Plenum ~Press, New York.
• 22: ~HOFFMANN, C.M. 1982. Group-Theorettc Algorithms and Graph Isomorphism. In Lecture Notes ~in Computer Science. G. Goos and J. Hartmanis, eds. vol. 136. Springer-Verlag, Berlin, ~Germany.
• 23: Sampath Kannan , Andrew Yao, Program checkers for probability generation, Proceedings of the 18th international colloquium on Automata, languages and programming, p.163-173, June 1991, Madrid, Spain
• 24: Richard M. Karp , Michael O. Rabin, Efficient randomized pattern-matching algorithms, IBM Journal of Research and Development, v.31 n.2, p.249-260, March 1987
• 25: Richard M. Karp , Vijaya Ramachandran, Parallel algorithms for shared-memory machines, Handbook of theoretical computer science (vol. A): algorithms and complexity, MIT Press, Cambridge, MA, 1991
• 26: Ker-I Ko, On helping by robust oracle machines, Theoretical Computer Science, v.52 n.1-2, p.15-36, May 1987 [doi>10.1016/0304-3975(87)90078-8]
• 27: LEON, J.S. 1984. Computing automorphism groups of combinatorial objects. In Computational ~Group Theory M. D. Atkinson, Ed. Academic Press, London, England, pp. 321-335.
• 28: ~LIPTON, R. 1991. New directions in testing. In Distributed Computing and Cryptography, DI- ~MACS series in Discrete Mathematics and Theoretical Computer Science, vol. 2. AMS, Providence, ~R.I., pp. 191-202.
• 29: Carsten Lund , Lance Fortnow , Howard Karloff, Algebraic methods for interactive proof systems, Journal of the ACM (JACM), v.39 n.4, p.859-868, Oct. 1992 [doi>10.1145/146585.146605]
• 30: ~MATHON, R.A. 1979. A note on the graph isomorphism counting problem. Inf. Proc. Lett. 8, ~131-t32.
• 31: George Pólya , R. C. H Read, Combinatorial enumeration of groups, graphs, and chemical compounds, Springer-Verlag New York, Inc., New York, NY, 1987
• 32: ~RABIN, M.O. 1976. Probabilistic algorithms. In Algorithms and Complexity, Recent Results and ~New Directions, J. F. Traub, ed. Academic Press, Orlando, Fla., pp. 21-40.
• 33: ~RUBINFELD, R. 1990. Designing checkers for programs that run in parallel. Tech. Rep. TR-090- ~040. International Computer Science Institute, Berkeley, Calif., August.
• 34: ~SCHONING, U. 1985. Robust algorithms: A different approach to oracles. Theoret. Comput. Sci. ~40, 57-66.
• 35: Adi Shamir, IP = PSPACE, Journal of the ACM (JACM), v.39 n.4, p.869-877, Oct. 1992 [doi>10.1145/146585.146609]
• 36: ~TOMPA, M., AND WOL{, H. 1987. Random self-reducibility and zero knowledge interactive ~proofs of possession of information. In Proceedings of the 28th IEEE Symposium on Foundations ~of Computer Science. IEEE Computer Society, Los Alamitos, Calif., pp. 472-482.
• 37: E. J. Weyuker, The evaluation of program-based software test data adequacy criteria, Communications of the ACM, v.31 n.6, p.668-675, June 1988 [doi>10.1145/62959.62963]
• 38: ~WEGMAN, M. N. AND CARTER, J.L. 1981. New hash functions and their use in authentication ~and set equality. J. Comput. Syst. Sci. 22 3, 265-279.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Reliability

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
  F.3 LOGICS AND MEANINGS OF PROGRAMS

  G. Mathematics of Computing
  G.3 PROBABILITY AND STATISTICS
      Subjects: Probabilistic algorithms (including Monte Carlo)

General Terms:
Algorithms, Design, Reliability, Theory, Verification

Keywords:
interactive proofs, probabilistic algorithms, program checking, program verification, testing