Formal verification tools and techniques are difficult and expensive to apply. To make verification of large, complex systems more practical, TRW is developing the deductive theory manager (DTM). A knowledge-based tool that integrates with the Gypsy verification environment (GVE), the DTM supports the construction of deductive theories and applies them to proofs. Knowledge bases applicable to a variety of projects, and one specific to the army secure operating system (ASOS) proofs, are simultaneously under development. The authors describe the underlying philosophy of the verification strategy on which the DTM is based, present the DTM architecture, and illustrate DTM knowledge engineering and proof processing with a case study.>

System Development Corporation (SDC) has developed an informal approach for establishing correspondence (or lack thereof) between the formal specifications of a system and lower levels of specification, including implementation code. Establishing correspondence means showing that one level meets the intent of a higher lever. This paper presents the motivation, technique, and current SDC experience with the method, contains an example of the hypothetical correlation analysis, and evaluates the limits and the usefulness of this approach. This paper results from recent applications of the method.