Taking the hol out of HOL

We describe a systematic approach to building tools for the analysis of specifications expressed in higher-order logic (hol) outside the framework of a conventional, interactive theorem proving environment. Tools such as HOL and PVS integrate the tasks of parsing and typechecking a hol specification with substantial and complex theorem-proving functionality. In contrast, we have taken ``the hol out of HOL'''' by building automated tools on top of just a parser and typechecker to eliminate the burden of the skilled interaction required in a conventional theorem prover. Our lightweight approach allows a hol specification to be used for diverse purposes such as refutation-based analysis and the algorithmic generation of test cases. Our toolset contains a variety of general-purpose utilities for the manipulation of higher-order logic specifications. For example, one utility allows a hol specification to be ``evaluated'''' in a manner similar to the evaluation of a functional program. These utilities are combined to implement analysis techniques such as symbolic model checking. After five years of experience with this approach, we conclude that by decoupling hol from its conventional environment, we retain the benefits of an expressive specification notation, and can generate many useful analysis results automatically.