Paper Info
Title
Muse A Computer Assisted Verification System
Abstract
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.
Year
DOI
Venue
1986
10.1109/TSE.1987.226477
IEEE Transactions on Software Engineering
Keywords
DocType
Volume
sri system,verification system,muse a computer assisted,specification language,secure operating system,sri international,a1 evaluation,hdm system,theorem prover kernel,theorem prover,formal verification,generators,operating systems,computer security
Conference
13
Issue
ISSN
ISBN
2
1540-7993
0-8186-0716-5
Citations 
PageRank 
References 
3
0.49
0
Authors
4
Name
Order
Citations
PageRank
J. Daniel Halpern130.49
Sam Owre21323104.39
Proctor, Norman341.60
Wilson, William F.430.49