such as embedded safety-critical software programs and trusted operating
system kernels. Only recently have formal methods started to be discussed as
a means for assuring the required security properties of software-intensive
systems. Also emerging are several “semi-formal” methods (e.g., Praxis High