jenlan@eos (Jennifer S Lanham) (08/04/90)
Thank you to all who responded to my inquiry regarding who is doing
programming correctness proofs. I recevied several requests for a summary
here it is with the sender listed at the beginning of his message.
From Mark Tuttle tuttle@crl.dec.com
Nancy Lynch's research group at MIT has been working on modeling and
verifying distributed algorithms for several years. This work is
based on an automata-theoretic model called the Input-Output Automaton
model. This model was originally developed for asynchronous
distributed algorithms, but there have been recent attempts to extend
the model to shared memory and to real-time systems. I can send you a
copy of my master's thesis, which defined the IOA model, and papers
containing examples of proofs in this model if you can tell me what
kind of things you are interested in.
Some big names in the verification field are
Nancy Lynch
MIT Lab for Computer Science
Leslie Lamport
DEC SRC, Palo Alto
Fred Schneider
Cornell University
Amir Pnueli
Hebrew or Jerusalem University, I can't remember
Zohar Manna
Stanford University
David Harel
Weizmann Institute, Rehovot, Israel
John Guttag (specifications, with Jim below)
MIT Lab for Computer Science
Jim Horning (specifications)
DEC SRC, Palo Alto
From Ian Mason (iam@Gang-of-Four.Stanford.edu)
Carolyn Talcott and myself are actively involved in developing techniques
for proving properties of programs with control abstractions and the
ability to destructively manipulate data. Similarly Matthias Felleisen at Rice
is also engaged in research into reasoning about such Scheme-like languages.
From John Doner (doner@henri.ucsb.edu)
I am doing such proofs as part of my summer work here at Aerospace. I will so
be teaching about them in my logic course at UCSB.
Respond to me at
doner@henri.ucsb.edu
From Jon Jacky (jon@gaffer.rad.washington.edu)
The best-known textbook that teaches how to do program proofs is David Gries,
THE SCIENCE OF PROGRAMMING, Springer-Verlag, 1981. A new book on the same
subject is Edsger W. Dijkstra and W.H.J. Feijen, A METHOD OF PROGRAMMING,
Addison-Wesley, 1988. There are software development systems that assist
with formal development and program proofs, the best-known of these is the
Gypsy system developed at the University of Texas at Austin, and at
Computational Logic Inc. in Austin. I believe it is actually available as
a product from CLI. Gypsy is described in Donald I Good, "Mechanical
proofs about computer programs," in Hoare and Shepherdson, MATHEMATICAL LOGIC
AND PROGRAMMING LANGUAGES, Prentice Hall 1985. This paper is also available
as a tech report direct from CLI. There are a couple of other program-proving
products around, including something called Refine from Reasoning Systems in
Palo Alto, CA.
There is just a huge literature on this subject, however whether or not many
people actually *do* this is another matter. I attended the ACM SIGSOFT
International Conference on Formal Methods in Software Engineering last May,
and many people at that meeting said proofs of correctness of programs were
very rarely used in industrial software production. About the only area where
they are regularly used is in proving the security properties of secure
operating systems and programs for the Department of Defense, and the reason
they are used in that field is that the DoD's contracts *require* it. Even
so, there is some controversy even within DoD regarding whether the effort is
worth it. A paper on one of these projects appears in PROCEEDINGS OF THE
1990 IEEE COMPUTER SOCIETY SYMPOSIUM ON RESEARCH IN SECURITY AND PRIVACY:
Ben Di Vito et al, "The Deductive Theory Manager: A Knowledge Based System for
Formal Verification", which describes a 380,000 - line (7,600 page) proof
of the security kernel of the Army Secure Operating System (they don't say how
much code was proved).
There is a lot of interest and some recent successes in using formal methods
to prove the correctness of computer *hardware* designs, notably the British
VIPER chip, the British Inmos Transputer floating-point chip, and work in
progress on a microprocessor at CLI in Texas.
From David Sims
dsims@uceng.uc.edu
My professor gave me two more interesting papers on program correctness. They're
by C.A.R Hoare et al; isn't he the one who did CSP (communicating sequential
processes)? Anyway, here they are.
1. "The Mathematics of Programming"
C.A.R. Hoare
5th Conference on Foundation of Software Technology and Theoretical
Computer Science
In lecture notes in Computer Science, No. 206, Springer-Verlag, pp. 1-18
2. "Laws of Programming: A Tutorial Paper"
C.A.R. Hoare, He Jifeng, I.J. Hayes, C.C. Morgan, J.W. Sanders,
I.H. Sorensen, J.M. Spivey, B.A. Sufrin, A.W. Roscoe
Technical Monograph PRG-45
May 1985
Oxford University Computing Laboratory
Programming Research Group
8-11 Keble Road
Oxford OX1 3QD
England
From David Keaton dmk@craycos.com
Ray Gumb at the University of Lowell, Massachusetts, is heavily
involved in correctness proofs. He is writing a book on correctness
because he feels the existing material does not adequately cover the
subject. The last I heard, his email address was gumb@ulowell.edu.
From: russ@mcc.com (David Russinoff)
I was asked to send you references to a couple of my papers.
Abstracts follow. They are both available as MCC Technical Reports.
A Verified Prolog Compiler for the Warren Abstract Machine
We extend the theory of Prolog to provide a framework for the study of
Prolog compilation technology. For this purpose, we first demonstrate
the semantic equivalence of two Prolog interpreters: a conventional
SLD-refutation procedure and one that employs Warren's ``last call''
optimization. Next, we formally define the Warren Abstract Machine
(WAM) and its instruction set and present a Prolog compiler for the
WAM. Finally, we prove that the WAM execution of a compiled Prolog
program produces the same result as the interpretation of its source.
A Verification System for Concurrent Programs
Based on the Boyer-Moore Prover
We describe a mechanical proof system for concurrent programs, based
on a formalization of the temporal framework of Manna and Pnueli as an
extension of the computational logic of Boyer and Moore. The system
provides a natural representation of specifications of concurrent
programs as temporal logic formulas, which are automatically
translated into terms that are subject to verification by the
Boyer-Moore prover. Several specialized derived rules of inference
are introduced to the prover in order to facilitate the verification
of invariance (safety) and eventuality (liveness) properties. The
utility of the system is illustrated by a correctness proof (which
could be executed by a naive user) for a two-process program that
computes binomial coefficients.
From: vestal@src.honeywell.com (Steve Vestal)
You might look at the Gypsy language/system (U Texas, Texas A&M??) or the
Cambridge HOL system. I think the commercial product Byron may have something
to do with formal verification of Ada programs (but I'm not sure). David
Gries published a textbook on formal sequential verification a few years ago,
and a lot of articles on the subject have appeared in Transactions on
Programming Languages and Systems over the years (my impression is that more
recent research focuses on things like proving concurrent correctness rather
than slicker ways to do sequential verification, but I may be wrong).
The only place I've ever heard of formal verification being used commercially
is in the secure computing domain. I have not, for example, heard of it being
required for reliable avionics or space software. Being from NASA, I don't
suppose you have any insights into the views of a "regulatory agency" (as
DO178A puts it) on formal verification? [No, I haven't a clue....I work at
NASA for a technical contractor]
From: Jim Caldwell <jlc@air16.larc.nasa.gov>
Here at NASA Langley Research Center we have an active research group
in formal methods. We have 4 civil servants and one in-house
contractor in our group and have contracts with the Computer Science
Lab at SRI, Computational Logic Inc. (CLINK) in Austin Texas, with
Odyssey Research Associates in Ithaca and with a research group at
Boeing Military aircraft.
The group at Odyssey (a number of whom participated in the recent
"digressive discussion") has developed the Penelope verification
system which can handel a subset of Ada. SRI has the EHDM
verification system which we use here at Langley and is quite good for
formalizing system properties and proving correctness of design
properties. The Computational Logic bunch includes the developers of
the Boyer-Moore prover they and have verified what they call the
short-stack. This consists of a formally verified micro-processor
with a formally verified assembler and loader implemented on it's
instruction set. On top of the assembler loader is a verified
compiler for a subset of the Gypsy programming language. (There is an
extensive verification environment also from CLINK for gypsy.) They
have also verified a simple multi-tasking operating system.
Our inhouse group is working on the design and verification of a
reliable computing platform for fly-by-wire contol applications. A
primary property of the system which we are interested in is its
ability to correctly recover from transient faults. A proof that the
design has this property has been given and should be available soon
as a NASA QRTM.
Thank you again to all who took the time to respond. I have to say
this group has been incredibly helpful.This is the second time I have asked
a rather basic question about sources, and the second time I have received
lots of help.
Sincerely, Jennifer S. Lanham
jenlan@eos.arc.nasa.govladkin@icsib12 (Peter Ladkin) (08/15/90)
In article <6996@eos.UUCP>, jenlan@eos (Jennifer S Lanham) writes: >From Jon Jacky (jon@gaffer.rad.washington.edu) > [....] There are a couple of other program-proving >products around, including something called Refine from Reasoning Systems in >Palo Alto, CA. Refine is not a program-proving system. Its main use is in specification and transformation of programs. For example, suppose you want to check if a contractor's code meets your coding standards. Refine may be used to build a checker for this. The inference capabilities in Refine are currently limited to type checking and type inference for a standard collection of data types plus sets and sequences. Peter Ladkin