Abstract
The Trusted Systems Group at I.P. Sharp Associates Limited has developed a prototype system, called m-EVES, for formally verifying software. Programs are written in a new language, called m-Verdi, and proved with the help of a theorem prover called m-NEVER. The logic for proving programs has been proved sound.
This paper describes the logic and the theorem prover, and presents two transcripts of the application of the system to simple problems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
W. Bledsoe and P. Bruell. A Man-Machine Theorem Proving System. InProceedings 3rd IJCAI, Stanford University, 1973.
Bob Boyer and J Strother Moore.A Computational Logic. Academic Press, 1979.
M. Cheheyl,et alVerifying Security.Computing Surveys13(4), September
Dan Craigen.A Description of m-Verdi. TR-87-5420-02, I.P. Sharp Associates Limited, November 1987.
Dan Craigen and Mark Saaltink.An m-Verdi User’s Guide. TR-87-5420- 12, LP. Sharp Associates Limited, November 1987.
Don Good.Proving Network Security. Internal Note #125-B, Institute for Computing Science, University of Texas at Austin, 1985.
Mike Gordon. Why Higher-Order Logic is a Good Formalism for Specifying and Verifying Hardware. In G.J. Milne and P.A. Subrahmanyam (Eds.),Formal Aspects of VLSI Design, North-Holland, 1986.
David Gries. A Note on a Standard Strategy for Developing Loop Invariants and Loops. InScience of Computer Programming2(3), December
John Guttag,et alAbstract Data Types and Software Validation.CACM21(12), December 1978.
Dick Kemmerer. Testing Formal Specifications to Detect Design Errors.IEEE Transactions on Software Engineering21(1), January 1985.
Dick Kemmerer,et al. Verification Assessment Study Final ReportTechnical Report C3-CR01-86, National Computer Security Center, Maryland.
D.C. Luckham,et al. Stanford Pascal Verifier User Manual.STAN-CS-79-731, Stanford University Computer Science Department, March 1979.
Irwin Meisels.VAX/VMS m-Verdi Compiler User’s ManualTR-87-5420-10 I.P. Sharp Associates Limited, October 1987
Irwin Meisels.VAX/Unix m-Verdi Compiler User’s ManualTR-87-5420-11 I.P. Sharp Associates Limited, October 1987.
Greg Nelson.Techniques for Program Verification. CSL-81-10, Xerox PARC, June 1981.
Bill Pase and Sentot Kromodimoeljo.NEVER: An Interactive Theorem Prover. CP-87-5402-20, LP. Sharp Associates Limited, January 1987.
Mark Saaltink.The Mathematics of m-Verdi. FR-87-5420-03, LP. Sharp Associates Limited, November 1987.
D. Thompsonet al.AFFIRM Reference Manual USC Information Sciences Institute, Marina Del Rey, California, 1981
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1989 Springer-Verlag New York Inc.
About this chapter
Cite this chapter
Pase, B., Saaltink, M. (1989). Formal Verification in m-EVES. In: Birtwistle, G., Subrahmanyam, P.A. (eds) Current Trends in Hardware Verification and Automated Theorem Proving. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-3658-0_6
Download citation
DOI: https://doi.org/10.1007/978-1-4612-3658-0_6
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4612-8195-5
Online ISBN: 978-1-4612-3658-0
eBook Packages: Springer Book Archive