%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "blumk95.ltx",
%%%     date      = "20 November 1995",
%%%     time      = "21:41:31 EST",
%%%     author    = "David M. Jones",
%%%     email     = "jacm@theory.lcs.mit.edu",
%%%     url       = "http://theory.lcs.mit.edu/~jacm/",
%%%     address   = "Journal of the ACM
%%%                  MIT Laboratory for Computer Science
%%%                  Room NE43-316
%%%                  545 Technology Square
%%%                  Cambridge, MA 02139
%%%                  USA",
%%%     telephone = "(617) 253-5936",
%%%     FAX       = "(617) 253-3480",
%%%     checksum  = "18866 107 463 3832",
%%%     codetable = "ISO/ASCII",
%%%     supported = "yes",
%%%     docstring = "Copyright (c) 1995 by ACM, Inc.
%%%                  Permission to make digital or hard copies of part
%%%                  or all of this work for personal or classroom use
%%%                  is granted without fee provided that copies are
%%%                  not made or distributed for profit or direct
%%%                  commercial advantage and that copies bear this
%%%                  notice and the full citation on the first page.
%%%                  Copyrights for components of this work owned by
%%%                  others than ACM must be honored. Abstracting with
%%%                  credit is permitted. To copy otherwise, to
%%%                  republish, to post on servers, or to redistribute
%%%                  to lists, requires prior specific permission
%%%                  and/or a fee. Request permissions from
%%%                  Publications Dept, ACM Inc., fax +1 (212)
%%%                  869-0481, or permissions@acm.org.
%%%                  
%%%                  This is a LaTeX2e file.  To process it, you will
%%%                  need a copy of the acmabs document class, which is
%%%                  available via the following URL:
%%%
%%%                  http://theory.lcs.mit.edu/~jacm/acmart/acmabs.cls
%%%                  ",
%%%  }
%%% ====================================================================

\documentclass{acmabs}

\begin{document}

\Journal{Journal of the ACM}

\refkey{BlumK95}

\title{Designing Programs that Check Their Work}

\author{Manuel Blum \and Sampath Kannan}

\Pages{269--291}

\Month{January}

\Year{1995}

\Volume{42}

\Number{1}

\maketitle

\begin{abstract}

A \emph{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. \par 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.

\end{abstract}

\begin{categories}

D.2.4[correctness proofs; reliability]; F.2.0; F.3.1; G.3[probabilistic
  algorithms (including Monte Carlo)]

\end{categories}

\begin{terms}

Algorithms, Design, Reliability, Theory, Verification

\end{terms}

\begin{keywords}

Interactive proofs, probabilistic algorithms, program checking, program
  verification, testing

\end{keywords}

\end{document}
