An Isabelle-Based Theorem Prover for VDM-SL

9 years 4 months ago
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...
Sten Agerholm, Jacob Frost
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1997
Authors Sten Agerholm, Jacob Frost
Comments (0)