An application of the m-EVES verification system
Dan Craigen · 2003
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.>