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 formal methods.

Title: Formal Methods Fact vs. Fiction

Panel Chair: Michael Holloway, NASA Langley Research Center

Panelists:

Ben Di Vito, ViGYAN, Inc.: Position Statement
David Guaspari, Odyssey Research Associates: Position Statement
Michael Smith, Computational Logic, Inc.: Position Statement

Summary

Few people seem to be ambivalent about formal methods. Proponents are ardent in their support; opponents are equally ardent in their disdain. 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 fact from fiction 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 opening presentation 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.

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 on applications of formal methods to fault-tolerant computin 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 space applications as part of a multi-center effort involving Langley Research Center, Johnson Space 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 address: b.l.divito@larc.nasa.gov.

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 Ada. 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 Ada 9X Language 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 davidg@oracorp.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 Ada 9X 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 mksmith@cli.com.

Michael Holloway is a research engineer at the World Wide Web homepage for formal methods (URL: http://shemesh.larc.nasa.gov/fm/). 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 c.m.holloway@larc.nasa.gov.