Abstract :
I.P. Sharp Associates, under the sponsorship of the United States Navy and the Canadian Department of National Defence, is developing a formal program verification and evaluation system based on the Euclid programming language. The central application of the system is to be the development of security related software. This paper reports the status of the project, as of early 1984, and discusses some of the research and development directions being followed.
