Designing programs that check their work

ABSTRACT

A program correctness checker is an algorithm for checking the output of a computation. This paper defines the concept of a program checker. It designs program checkers for a few specific and carefully chosen problems in the class P of problems solvable in polynomial time. 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. Finally it characterizes the problems that can be checked.

REFERENCES

• A: D. Angluin, "Lecture Notes on the Complexity of Some Problems in Number Tl~eory," Yale Technical Report #243 (1982).
• B1: R. Beigel, personal communication.
• B2: M. Blum, "Designing Programs to Check Their Work", submitted for publication in CACM.
• BA: T.A. Budd and D. Angluin, "Two Notions of Correcmess and Their Relation to Testing," Acta Informaflea, v. 18, 31-45 (1982).
• BCG: E.R. Berlekamp, J.H. Conway, and R.K. Guy, "Winning Ways," Academic Press, (1982).
• BR: M. Blum and P. Raghavan, "Program Correctness: Can One Test for It?," IBM T.J. Watson Research Center Technical Report (1988).
• CFGMW: Larry Carter , Robert Floyd , John Gill , George Markowsky , Mark Wegman, Exact and approximate membership testers, Proceedings of the tenth annual ACM symposium on Theory of computing, p.59-65, May 01-03, 1978, San Diego, California, United States [doi>10.1145/800133.804332]
• F: R. Freivalds, "Fast Probabilistic Algorithms," Springer Vefiag Lecture Notes in CS #74, Mathematical Foundations of CS, 57-69 (1979).
• FHL: M. Furst, J.E. Hopcroft, E. Luks, "Polynomial-Time Algorithms for Permutation Groups," Proc. 21st IEEE Symposium on Foundations of Computer Science, 36-41 (1980).
• GJ: M.R. Garey and D.S. johnson, "Computers and Intractability," Freeman, San Francisco, CA (1979).
• GMR: S Goldwasser , S Micali , C Rackoff, The knowledge complexity of interactive proof-systems, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.291-304, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22178]
• GMW: O. Goldreich, S. Micali and A. Wigderson, "Proofs that Yield Nothing but their Validity and a Methodology of Cryptographic Design," Proc. 27th IEEE Symposium on Foundations of Computer Science, 174-187 (1986).
• GS: S Goldwasser , M Sipser, Private coins versus public coins in interactive proof systems, Proceedings of the eighteenth annual ACM symposium on Theory of computing, p.59-68, May 28-30, 1986, Berkeley, California, United States [doi>10.1145/12130.12137]
• H: C.M. Hoffmann, "Group-Theoretic Algorithms and Graph Isomorphism,'' V. 136 of the series "Lecture Notes in Computer Science," ed. by G. Goos and J. Hartmanis, Springer-Verlag, 311 pp. (1982).
• K1: R. Kannan, personal communication through S. Rudich.
• K2: S. Kannan, Ph.D. thesis to be submitred to the Computer Science Division of the University of Califomia at Berkeley.
• KR: 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
• L1: J. Leech, "Computer Proof of Relations in Groups," in "Topics in Group Theory and Computation," edited by M.P.J. Curran, Academic Press, 38-61 (1977).
• L2: J.S. Leon, "Computing Automorphism Groups of Combinatorial Objects," in "Computational Group Theory," edited by M.D. Atkinson, Academic Press, 321-335 (1984).
• L3: R. Lipton, personal communication.
• PR: George Pólya , R. C. H Read, Combinatorial enumeration of groups, graphs, and chemical compounds, Springer-Verlag New York, Inc., New York, NY, 1987
• R: M.O. Rabin, "Probabilistic Algorithms,'' in "Algorithms and Complexity, Recent Results and New Directions," edited by J.F. Traub, Academic Press, 21-40 (1976).
• TW: M. Tompa and H. Woll, "Random Self-Reducibility and Zero Knowledge Interactive Proofs of Possession of Information," Proc. 28th IEEE Symposium on Foundations of Computer Science, 472-482 (1987).
• W: 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]
• WC: M.N. Wegman and J.L. Caner, "New Hash Functions and Their Use in Authentication and Set Equality," J. of Computer and System Science, v. 22, no. 3, 265-279 (1981).

INDEX TERMS

Primary Classification:
  E. Data
  E.3 DATA ENCRYPTION

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

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

  G. Mathematics of Computing

General Terms:
Algorithms, Security, Verification