The deductive theory manager: a knowledge based system for formal verification

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