m-EVES: a tool for verifying software
- 6 January 2003
- proceedings article
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 324-333
- https://doi.org/10.1109/icse.1988.93713
Abstract
This paper describes the development of a new tool for formally verifying software. The tool is called m-EVES and consists of a new language, called m-Verdi, for implementing and specifying software; a new logic, which has been proven sound; and a new 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
This publication has 8 references indexed in Scilit:
- Strengths and weaknesses of Program Verification SystemsPublished by Springer Nature ,2005
- Automatic Generation of the C# Code for Security Protocols Verified with Casper/FDRPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Testing Formal Specifications to Detect Design ErrorsIEEE Transactions on Software Engineering, 1985
- A note on a standard strategy for developing loop invariants and loopsScience of Computer Programming, 1982
- The Science of ProgrammingPublished by Springer Nature ,1981
- Simplification by Cooperating Decision ProceduresACM Transactions on Programming Languages and Systems, 1979
- Abstract data types and software validationCommunications of the ACM, 1978
- Proof of correctness of data representationsActa Informatica, 1972