The EVES system

  • Sentot Kromodimoeljo
  • Bill Pase
  • Mark Saaltink
  • Dan Craigen
  • Irwin Meisels
Part of the Lecture Notes in Computer Science book series (LNCS, volume 693)


After a brief introduction, we discuss two applications of EVES. The first application is a proof of Jacobson's Theorem. The second application is a proof of an interpreter for a small programming language; portions of the interpreter proof are described in this paper. We conclude by discussing some of the issues raised by the international lecture series on “Functional Programming, Concurrency, Simulation and Automated Reasoning” (FPCSAR).


Automated deduction EVES Formal Methods Logic of programs NEVER Verdi 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BB74]
    W.W. Bledsoe and P. Bruell. A man-machine theorem proving system. Artificial Intelligence, 5(1):51–72, 1974.Google Scholar
  2. [BHK89]
    J.A. Bergstra, J. Heering, and P. Klint. Algebraic Specification. ACM Press, New York, New York, 1989.Google Scholar
  3. [BM79]
    Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, NY, 1979.Google Scholar
  4. [CKM+91]
    [CKM+91] Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, and Mark Saaltink. EVES: An Overview. In Proceedings of VDM '91, Noordwijkerhout, The Netherlands (October 1991). Springer-Verlag, 1991.Google Scholar
  5. [Cra91]
    Dan Craigen. Reference manual for the language Verdi. Technical Report TR-91-5429-09a, ORA Canada, Ottawa, September 1991.Google Scholar
  6. [CS90]
    Dan Craigen and Mark Saaltink. Simple Type Theory in EVES. In Graham Birtwistle, editor, Proceedings of the Fourth Banff Higher Order Workshop (9–15 September 1990), New York, 1990. Springer-Verlag.Google Scholar
  7. [Fra68]
    Abraham Fraenkel. Abstract Set Theory. North-Holland, 1968.Google Scholar
  8. [Her90]
    Ted Herman. On a theorem of Jacobson. In W.H.J. Feigen, et al., editor, Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra. Springer-Verlag, New York, 1990.Google Scholar
  9. [KP90]
    Sentot Kromodimoeljo and Bill Pase. Using the EVES Library Facility: A PICO Interpreter. Final Report FR-90-5444-02, ORA Canada, Ottawa, February 1990.Google Scholar
  10. [LJZ92]
    P.E. Lauer, R. Janicki, and J. Zucker. Functional Programming, Concurrency, Simulation and Automated Reasoning (FPCSAR). Memo FPCSAR.1, Department of Computer Science and Systems, McMaster University, February 1992.Google Scholar
  11. [Luc79]
    D.C. Luckham, et al. Stanford Pascal Verifier User Manual. Technical Report STAN-CS-79-731, Stanford University, Computer Science Department, March 1979.Google Scholar
  12. [Saa90a]
    Mark Saaltink. Alternative Semantics for Verdi. Technical Report TR-90-5446-02, ORA Canada, Ottawa, November 1990.Google Scholar
  13. [Saa90b]
    Mark Saaltink. A formal description of Verdi. Technical Report TR-90-5429-10a, ORA Canada, Ottawa, November 1990.Google Scholar
  14. [Saa91a]
    Mark Saaltink. Using make to maintain EVES libraries. Working Paper WP-91-5449-206, ORA Canada, Ottawa, July 1991.Google Scholar
  15. [Saa91b]
    Mark Saaltink. Z and EVES. Technical Report TR-91-5449-02, ORA Canada, Ottawa, October 1991.Google Scholar
  16. [Saa92]
    Mark Saaltink. Z and EVES: A summary. In Proceedings of the 6th Annual Z User Meeeting (16–17 December 1991), Berlin, 1992. Workshops in Computing, Springer-Verlag.Google Scholar
  17. [Spi89]
    J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1989.Google Scholar
  18. [TE81]
    D.H. Thompson and R.W. Erickson, editors. AFFIRM Reference Manual. USC Information Sciences Institute, Marina Dey Ray, CA, 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Sentot Kromodimoeljo
    • 1
  • Bill Pase
    • 1
  • Mark Saaltink
    • 1
  • Dan Craigen
    • 1
  • Irwin Meisels
    • 1
  1. 1.ORA CanadaOttawaCanada

Personalised recommendations