DocumentCode
2646332
Title
An application of the m-EVES verification system
Author
Craigen, Dan
Author_Institution
I.P. Sharp Associates Ltd., Ottawa, Ont., Canada
fYear
1988
fDate
19-21 Jul 1988
Firstpage
21
Lastpage
36
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Testing, Verification, and Analysis, 1988., Proceedings of the Second Workshop on
Conference_Location
Banff, Alta.
Print_ISBN
0-8186-0868-4
Type
conf
DOI
10.1109/WST.1988.5351
Filename
5351
Link To Document