Benedetto L. Di Vito

Education

Ben holds a Ph.D. in computer science from the University of Texas at Austin (1982). His dissertation was titled Verification of Communications Protocols and Abstract Process Models, and was supervised by Donald I. Good and Simon S. Lam. Ben also received an M.S.E. in computer, information and control engineering from the University of Michigan (1975), and a B.S.E. in computer engineering from the University of Michigan (1974).

After completing his education, Ben joined the Institute of Electrical and Electronics Engineers (IEEE) and the Association for Computing Machinery (ACM), and has been a long-standing member of both professional organizations.

Professional Experience

From July 1975 to August 1978, Ben held software development positions at ITT Telecommunications in Des Plaines, Illinois, and then at Texas Instruments in Austin, Texas.

While studying toward his Ph.D. at the University of Texas at Austin, Ben worked as a research assistant with the university's Institute for Computing Science and Computer Applications from June 1979 to August 1982. He participated in the project that developed the Gypsy Verification Environment (GVE) for concurrent program proving, under the direction of Dr. Donald Good. For his Ph.D. thesis, Ben devised a method for protocol specification and verification based on Gypsy-style concurrency proofs carried out with the Boyer-Moore theorem prover (later called “nqthm,” and later still, succeeded by ACL2).

In September 1982, Ben joined Sytek, Inc. of Mountain View, California, where he participated in research activities related to computer security and formal verification of software.

From December 1983 to December 1989, Ben was a senior project engineer with TRW, Inc. in Redondo Beach, California, where he concentrated on applications of computer security and formal methods:

• On a major DoD, A1-secure, system development program concerned with automated message processing, he served as subproject manager for security engineering during the first year, and later supported modeling and verification activities.
• After devising the formal methods approach for the Army Secure Operating System (ASOS) project, a level A1 trusted system written in Ada, he developed its formal security model, wrote formal specifications, and conducted GVE proofs.
• As principal investigator of the Multilevel Applications Security Technology (MAST) IR&D project, he introduced the Deductive Theory Manager concept, a knowledge-based verifier's assistant for the GVE, which TRW later continued under contract to the National Computer Security Center.

From December 1989 to October 1998, Ben worked as a senior research engineer for VíGYAN, Inc. of Hampton, Virginia, where his research conducted for NASA Langley included the following efforts:

• For the Reliable Computing Platform (RCP) project, a formally verified, fault tolerant operating system concept, he developed formal specifications and hierarchical verification schemes, carried out mechanically assisted proofs, and formulated and proved the transient recovery properties.
• He coauthored (with George Finelli of NASA Langley) the formal methods section of RTCA's DO-178B guidelines for avionics software.
• Working with a NASA-wide team to evaluate formal methods for space applications, he formalized key software requirements for the Change Request to add GPS navigation capabilities to the Space Shuttle fleet. With this same team, he coauthored a NASA guidebook on formal methods (published in two volumes).
• He contributed to the Langley research effort to develop strong approaches for partitioning in Avionics Computer Resources (ACRs), including participation in RTCA standards committee SC-182.
• Along with NASA colleagues, he taught a training course on PVS to groups of engineers from industry, which included comprehensive instruction on using the theorem prover.

Since November 1998, Ben has been a senior research engineer in the Safety-Critical Avionics Systems Branch at the NASA Langley Research Center.