A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called "predicate subtyping" that uses this capability and illustrate its utility as mechanized in PVS.

PVS is the most recent in a series of verification systems developed at SRI. Its design was strongly influenced, and later refined, by our experiences in developing formal specifications and mechanically checked verifications for the fault-tolerant architecture, algorithms, and implementations of a model "reliable computing platform" (RCP) for life-critical digital flight-control applications, and by a collaborative project to formally verify the design of a commercial avionics processor called AAMP5. Several of the formal specifications and verifications performed in support of RCP and AAMP5 are individually of considerable complexity and difficulty. But in order to contribute to the overall goal, it has often been necessary to modify completed verifications to accommodate changed assumptions or requirements, and people other than the original developer have often needed to understand, review, build on, modify, or extract part of an intricate verification. We outline the verifications performed, present the lessons learned, and describe some of the design decisions taken in PVS to better support these large, difficult, iterative, and collaborative verifications.>

Muse is a verification system which extends the collection of tools developed by SRI International for their Hierarchical Development Methodology (HDM). It enhances the SRI system by providing a capability for proving invariants and constraints for the state machine described by a specification written in SPECIAL (the specification language of HDM). In particular, it enables one to use the HDM system to meet the requirements for formal verification in a National Computer Security Center A1 evaluation of a secure operating system. In addition to the tools provided by SRI, Muse has a parser, a facility to handle multiple modules, a formula generator, and a theorem prover. The theorem prover has a number of interesting features designed to facilitate human direction of the proving process. In concept, it is open-ended. We introduce the notion of a theorem prover kernel as a device for ensuring the logical soundness of the prover in the face of continual improvements to its functionality.

Muse is a verification system which extends the collection of tools developed by SRI for their Hierarchical Development Methodology (HDM). It enhances the SRI system by providing a capability for proving invariants and constraints for the state machine described by a SPECIAL specification. In particular, it enables one to use the HDM system to meet the requirements for formal verification in a National Computer Security Center Al evaluation of a secure operating system. In addition to the tools provided by SRI, Muse has a parser, a facility to handle multiple modules, a formula generator and a theorem prover. The theorem prover has a number of interesting features designed to facilitate human direction of the proving process.