DocumentCode
3292371
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
fYear
1988
fDate
11-15 Apr 1988
Firstpage
324
Lastpage
333
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Software Engineering, 1988., Proceedings of the 10th International Conference on
Print_ISBN
0-89791-258-6
Type
conf
DOI
10.1109/ICSE.1988.93713
Filename
93713
Link To Document