LEVITT@SRI-AI.ARPA (07/05/83)
From: Karl N. Levitt <LEVITT@SRI-AI.ARPA>
[Reprinted from the UTexas-20 BBoard.]
ROBERT S. BOYER AND J STROTHER MOORE: RECIPIENTS OF
THE 1983 JOHN MCCARTHY PRIZE FOR WORK IN PROGRAM
VERIFICATION
An anonymous donor has established the John McCarthy Prize, to be
awarded every two years for outstanding work in Program Verification.
The prize, is intended to recognize outstanding current work -- not
necessarily work of a milestone value. This first award is for work
carried out and published during the past 5 years.
Our committee has decided to give the initial award to Robert S. Boyer
and J Strother Moore for work carried out at the following
institutions: University of Edinburgh, SRI International and,
currently, the University of Texas. Their main achievement is the
development of an elegant logic implemented in a very powerful theorem
prover. Particularly noteworthy about the logic is the use of
induction to express properties about the objects common to programs.
Their theorem prover is among the most powerful of the current
mechanical provers, combining heuristics in support of automatic
theorem proving with a user interface that allows a human to drive
proofs that cannot be accomplished automatically. They have extended
their theorem prover with a Verification Condition Generator for
Fortran that handles most of the features -- even those thought to be
too "dirty" for verification -- of a "real" programming language. They
have used their system to prove numerous applications, including
programs subtle enough to tax human verifiers, and such real
applications as crytographic algorithms and simple flight control
systems; their proofs are always very "honest", using "believable"
specifications and assuming little more than a core set of axioms.
Their work has led to a constant stream of high quality publications,
including the book "A Computational Logic", Academic Press, 1979, and
a comprehensive User's Manual to the theorem prover.
The other individuals nominated by the committee are the following:
Donald Good: for the language Gypsy which enhances the possibility for
verifying concurrent and real-time systems, for the verification
system based on Gypsy, and for carrying out the verification of
numerous "real" systems; Robin Milner: for the Logic of Computable
Functions which has led to elegant formal definitions of programming
languages, to elegant specifications of varied applications, and to a
powerful mechanical theorem prover; Susan Owicki and David Gries: for
a practical method for the verification of concurrent programs; and to
Wolfgang Polak: for the verification of a "real" Pascal compiler,
perhaps the largest and most comlicated program verified to date.
The committee would also like to call attention to interesting and
important work in a number of areas related to program verification.
Included herein are the following: the formal definition of large and
complex programming languages; numerous mechanical verification
systems for a variety of programming languages; the verification of
systems covering such applications as computer security, compilers,
operating systems, fault-tolerant computers, and digital logic;
program testing; and program transformation. This work indicates that
program verification (and its extensions) besides being a rich area
for research gives promise of being usable to achieve reliability when
needed for critical applications.
Robert Constable -- Cornell
Susan Gerhart -- Wang Institute
Karl Levitt (Chairman) -- SRI International
David Luckham -- Stanford
Richard Platek -- Cornell and Odyssey Research Associates
Vaughan Pratt -- Stanford
Charles Rich -- MIT