An Isabelle-Based Theorem Prover for VDM-SL

This note lists references which address –in some way or another– the problems relating to formal manipulation of logical expressions where terms can fail to denote. References [ABM98] S. Angerholm, J. Bicarregui, and S. Maharaj. On the Verification of VDM Specifications and Refinement with PVS. In J.C. Bicarregui, editor, Proof in VDM: Case Studies, FACIT. Springer, 1998. [Abr84a] J-R. Abrial. The mathematical construction of a program and its application to the construction of mathematics. Science of Computer Programming, 4:45–86, 1984. [Abr84b] J-R. Abrial. Programming as a Mathematical Exercise, pages 113–137. Prentice-Hall International, 1984. [AF97a] S. Agerholm and J. Frost. An Isabelle-based theorem prover for VDM-SL. In Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs’97), Lecture Notes in Computer Science. SpringerVerlag, August 1997. [AF97b] Sten Agerholm and Jacob Frost. Towards an Integrated CASE and Theorem P...

• Type: Conference
• Year: 1997
• Where: TPHOL
• Authors: Sten Agerholm, Jacob Frost
• Keywords: Automated Reasoning, Computer Science, Lecture Notes, Theorem Proving, TPHOL 1997