Title :
m-EVES: a tool for verifying software
Author :
Craigen, Dan ; Kromodimoeljo, Sentot ; Meisels, Irwin ; Neilson, Andy ; Pase, Bill ; Saaltink, Mark
Author_Institution :
I.P. Sharp Associates Ltd., Ottawa, Ont., Canada
Abstract :
A description is given of the development of a tool for formally verifying software. The tool is called m-EVES and consists of a language, called m-Verdi, for implementing and specifying software; a logic that has been proved sound; and theorem prover, called m-NEVER, which integrates many state-of-the-art techniques drawn from the theorem proving literature. Two simple examples are used to present the fundamental ideas embodied within the system
Keywords :
program verification; software engineering; software tools; specification languages; theorem proving; m-EVES; m-NEVER; m-Verdi; specifying software; theorem prover; verifying software; Application software; Formal specifications; Formal verification; Logic; Programming; Prototypes; Software prototyping; Software quality; Software tools; Telephony;
Conference_Titel :
Software Engineering, 1988., Proceedings of the 10th International Conference on
Print_ISBN :
0-89791-258-6
DOI :
10.1109/ICSE.1988.93713
