Title :
An application of the m-EVES verification system
Author_Institution :
I.P. Sharp Associates Ltd., Ottawa, Ont., Canada
Abstract :
After a brief overview of the m-EVES system, an application of m-EVES to a proof of a nontrivial security property (noninterference) for a pedagogical computer system (the Low Water Mark system) is discussed. An example demonstrates some of the power and novel features of m-EVES. The author concludes with a comparison of the m-EVES solution with similar efforts using the Gypsy verification environment and the Boyer-Moore theorem prover
Keywords :
program verification; software tools; Boyer-Moore theorem prover; Gypsy verification environment; Low Water Mark system; m-EVES verification system; noninterference; pedagogical computer system; security property; Application software; Formal specifications; Formal verification; Logic; Power system security; Prototypes; Software prototyping; Telephony; Water; Writing;
Conference_Titel :
Software Testing, Verification, and Analysis, 1988., Proceedings of the Second Workshop on
Conference_Location :
Banff, Alta.
Print_ISBN :
0-8186-0868-4
DOI :
10.1109/WST.1988.5351
