%%% ====================================================================
%%%  @LaTeX-file{
%%%     filename  = "boyery96.ltx",
%%%     date      = "16 May 1996",
%%%     time      = "14:58:8 EDT",
%%%     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  = "21660 111 458 3913",
%%%     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{BoyerY96}

\title{Automated Proofs of Object Code for a Widely Used Microprocessor}

\author{Robert~S. Boyer \and Yuan Yu}

\Pages{166--192}

\Month{January}

\Year{1996}

\Volume{43}

\Number{1}

\maketitle

\begin{abstract}

We have formally described a substantial subset of the MC68020, a widely used
  microprocessor built by Motorola, within the mathematical logic of the
  automated reasoning system Nqthm, a.k.a.\ the Boyer-Moore Theorem Prover.
  Using this formal description, we have mechanically checked the correctness
  of MC68020 object code programs for binary search, Hoare's Quick Sort,
  twenty-one functions from the Berkeley Unix C string library, and other
  well-known algorithms. The object code for these examples was generated using
  the Gnu~C, the Verdix Ada, and the Gnu Common Lisp compilers. We have
  mechanized a mathematical theory to facilitate automated reasoning about
  object code programs. We describe a two-stage methodology we use to do our
  proofs.

\end{abstract}

\begin{categories}

D.2.1 [\textbf{Software Engineering}]: Requirements\slash
Specifications; D.2.4 [\textbf{Software Engineering}]: Program
Verification; D.3.1 [\textbf{Programming Languages}]: Formal
Definitions and Theory; F.3.1 [\textbf{Logics and Meanings of
Programs}]: Specifying and Verifying and Reasoning about Programs;
I.2.3 [\textbf{Artificial Intelligence}]: Deduction and Theorem
Proving

\end{categories}

\begin{terms}

Theory

\end{terms}

\begin{keywords}

Ada, automated reasoning, Boyer-Moore logic, C, Common Lisp, formal methods,
  machine code, mechanical theorem proving, MC68xxx, Nqthm, object code,
  program proving, program verification

\end{keywords}

\end{document}
