This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Muse?A Computer Assisted Verification System
February 1987 (vol. 13 no. 2)
pp. 151-156
J.D. Halpern, Department of Government Research and Development, Sytek, Inc.
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.
Index Terms:
theorem prover, Formal specification, formal verification, HDM, interactive theorem proving, Muse, National Computer Security Center, software verification, SPECIAL
Citation:
J.D. Halpern, S. Owre, N. Proctor, W.F. Wilson, "Muse?A Computer Assisted Verification System," IEEE Transactions on Software Engineering, vol. 13, no. 2, pp. 151-156, Feb. 1987, doi:10.1109/TSE.1987.226477
Usage of this product signifies your acceptance of the Terms of Use.