TRI-Ada '94 Formal Methods Panel Summary
Note: this page is no longer maintained.
At TRI-Ada '94 (Baltimore, November 7-11, 1994),
there was a panel session on
Title: Formal Methods Fact vs. Fiction
Few people seem to be ambivalent about formal methods. Proponents
are ardent in their support; opponents are equally ardent in their
Over-zealous supporters make unsupportable claims about the potential of
formal methods, while over-zealous detractors make unsupportable claims about
its shortcomings. A primary cause of this polarization is that it is often
difficult to separate
in formal methods. This panel plans
to make that separation.
In particular, the panel will address each of the following
fictitious statements about formal methods:
Each panelist will make a 15-minute
in which he will address several of the above statements.
The remainder of the session will
be used for interaction between the audience and the panelists.
Formal methods requires lots of education and training
Formal methods is equivalent to theorem proving
Formal methods is too expensive to use in practice
Formal methods does not scale to real problems
Formal methods guarantees perfection
Formal methods is a straight jacket
Formal methods is an all-or-nothing approach
Formal methods is simply code-level proofs
Ada is too complex and ambiguous semantically to be
compatible with formal methods.
Brief Professional Biographies of the Participants
Ben Di Vito
is a Senior Research Scientist for ViGYAN, Inc. He
currently conducts research at
NASA Langley Research Center
of formal methods to
and flight control system
reliability. He is also contributing to the analysis and design of Langley's
Reliable Computing Platform (RCP),
and is participating in a
pilot project to evaluate formal methods for NASA
as part of a multi-center
Langley Research Center,
Center, and the
Jet Propulsion Lab.
Prior to joining ViGYAN, he worked for TRW Inc., in a
variety of roles involving computer security and formal methods technologies,
including a key role in the Army Secure Operating System (ASOS), an Ada-based
operating system designed to meet A1 security criteria. He has a Ph.D. in
Computer Science from the University of Texas at Austin, and M.S.E. and
B.S.E. degrees in Computer Engineering from the University of Michigan.
Mr. Di Vito may be contacted through electronic mail at the following
David Guaspari is employed by
Odyssey Research Associates (ORA) in
Ithaca, New York. His areas of expertise include: mathematical logic, formal
specification and verification of software, and
He has been involved in
the design and implementation of the
Penelope programming environment
for specification and formal verification of Ada programs and of the Larch/Ada
specification language, and he was the original leader of the
Precision Project (sponsored by the Ada 9X Project Office), providing advice
to the Mapping/Revision Team based on mathematical analysis of proposed
language changes. He has a Ph.D. in Mathematics from the University of
Cambridge, and a B.S. in Mathematics from Rensselaer Polytechnic Institute.
Mr. Guaspari's electronic mail address is email@example.com.
Michael Smith is the Executive Vice-President of
Computational Logic, Inc.
in Austin, Texas. He was one of the five founders of CLI. He directed
CLI's efforts as part of the
Language Precision Team (ORA was prime),
which analyzed selected Ada 9X mapping proposals and attempted to provide a
basis for future mathematical work on the semantics of Ada. He is currently
engaged in an effort to prove properties of Ada programs by direct
application of an operational semantic definition of a subset called AVA (A
Verifiable Ada) that has been specified in the ACL2 Logic. The result of
this work should be a library of theorems and an assortment of tools to
assist in the proof process. He holds a Ph.D. in Computer Science from the
University of Texas at Austin, and a B.S.E. in Electrical Engineering from
Princeton University. Mr. Smith's electronic mail address is
is a research engineer at the
World Wide Web homepage for formal methods (URL:
He has a B.S. in computer
science from the University of Virginia, and did graduate computer
science work at the University of Illinois at Urbana-Champaign.
His electronic mail address is
LaRC Formal Methods Home Page
WWW Virtual Library: Formal Methods
Last modified: 16 December 1994 (15:28:53)