{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T13:46:34Z","timestamp":1725630394610},"publisher-location":"London","reference-count":18,"publisher":"Springer London","isbn-type":[{"type":"print","value":"9783540761860"},{"type":"electronic","value":"9781447115328"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/978-1-4471-1532-8_6","type":"book-chapter","created":{"date-parts":[[2011,11,4]],"date-time":"2011-11-04T15:28:04Z","timestamp":1320420484000},"page":"157-189","source":"Crossref","is-referenced-by-count":1,"title":["On the Verification of VDM Specification and Refinement with PVS"],"prefix":"10.1007","author":[{"given":"Sten","family":"Agerholm","sequence":"first","affiliation":[]},{"given":"Juan","family":"Bicarregui","sequence":"additional","affiliation":[]},{"given":"Savi","family":"Maharaj","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"S. Agerholm. A HOL Basis for Reasoning about Functional Programs PhD thesis, BRICS, Department of Computer Science, University of Aarhus, 1994. Available as Technical Report RS-94\u201344.","DOI":"10.7146\/brics.v1i44.21598"},{"key":"6_CR2","volume-title":"The Computer Journal, 38(2)","author":"S Agerholm","year":"1995","unstructured":"S. Agerholm. LCF examples in HOL. In The Computer Journal, 38(2), 1995."},{"key":"6_CR3","first-page":"1125","volume-title":"Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOL 96), Springer-Verlag LNCS","author":"S Agerholm","year":"1996","unstructured":"S. Agerholm. Translating Specifications in VDM-SL to PVS. In Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOL \u201986), Springer-Verlag LNCS 1125, 1996."},{"key":"6_CR4","volume-title":"Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs97), Springer-Verlag LNCS","author":"S Agerholm","year":"1997","unstructured":"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\u201997), Springer-Verlag LNCS, 1997."},{"key":"6_CR5","volume-title":"FME97, Springer-Verlag LNCS","author":"S Agerholm","year":"1997","unstructured":"S. Agerholm and J. Frost. Towards an Integrated CASE and Theorem Proving Tool for VDM-SL. In FME\u201997, Springer-Verlag LNCS, 1997."},{"key":"6_CR6","volume-title":"FME97, Springer-Verlag LNCS","author":"B Aichernig","year":"1997","unstructured":"B. Aichernig and P. G. Larsen. A Proof Obligation Generator for VDM-SL. In FME\u201997, Springer-Verlag LNCS, 1997."},{"key":"6_CR7","unstructured":"D.J. Andrews and M. Bruun et al. Information Technology \u2014 Programming Languages, their environments and system software interfaces \u2014 Vienna Development Method-Specification Language Part 1: Base language. ISO Draft International Standard: 13817\u20131, 1995."},{"key":"6_CR8","volume-title":"Rutherford Appleton Laboratory","author":"JC Bicarregui","year":"1993","unstructured":"J.C. Bicarregui. A Model-Oriented Analysis of a Communications Protocol. Technical report RAL-93\u2013099, Rutherford Appleton Laboratory, 1993."},{"key":"6_CR9","volume-title":"Proceeding of Formal Methods Europe 93, Springer-Verlag LNCS 670, 1993. Also in IEEE Transaction on Software Engineering, 21(2)","author":"JC Bicarreui","year":"1995","unstructured":"J.C. Bicarregui and B. Ritchie. Invariants, Frames and Postconditions: a comparison of the VDM and B notations. In Proceeding of Formal Methods Europe \u201983, Springer-Verlag LNCS 670, 1993. Also in IEEE Transaction on Software Engineering, 21(2), 1995."},{"key":"6_CR10","volume-title":"Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10\/WG 10.2 International Conference, North-Holland, IFIP Transactions A-10","author":"RJ Boulton","year":"1992","unstructured":"R. J. Boulton and A. D. Gordon et al Experience with Embedding Hardware Description Languages in HOL. In Theorem Provers in Circuit Design: Theory, Practice and Experience: Proceedings of the IFIP TC10\/WG 10.2 International Conference, North-Holland, IFIP Transactions A-10, 1992."},{"key":"6_CR11","volume-title":"Formal Aspects of Computing, 6(1), Springer","author":"G Bruns","year":"1994","unstructured":"G. Bruns and S. Anderson. The Formalization and Analysis of a Communications Protocol. In Formal Aspects of Computing, 6(1), Springer, 1994."},{"key":"6_CR12","first-page":"971","volume-title":"Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Springer-Verlag LNCS","author":"G Collins","year":"1995","unstructured":"G. Collins and D. Syme. A theory of finite maps. In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, Springer-Verlag LNCS 971, September 1995."},{"key":"6_CR13","volume-title":"A Tutorial Introduction to PVS. Computer Science Laboratory","author":"J Crow","year":"1993","unstructured":"J. Crow, S. Owre et al A Tutorial Introduction to PVS. Computer Science Laboratory, SRI International, Menlo Park, CA, February 1993."},{"key":"6_CR14","volume-title":"ACM Sigplan Notices 29(9)","author":"R Elmstrom","year":"1994","unstructured":"R. Elmstrom, P.G. Larsen, and P.B. Lassen. The IFAD VDM-SL Toolbox: A practical approach to formal specifications. In ACM Sigplan Notices 29(9), 1994"},{"key":"6_CR15","unstructured":"P.G. Larsen. Towards Proof Rules for VDM-SL PhD thesis, Technical University of Denmark, Department of Computer Science, March 1995. ID-TR:1995160."},{"key":"6_CR16","volume-title":"Formal Aspects of Computing, 8(1)","author":"G Peter","year":"1996","unstructured":"Peter G. Larsen and Bo S. Hansen. Semantics of Underdetermined Expressions. In Formal Aspects of Computing, 8(1), 1996."},{"key":"6_CR17","volume-title":"IEEE Transactions on Nuclear Science, 36(1)","author":"LL Santoline","year":"1989","unstructured":"L.L. Santoline et al. Multiprocessor Shared-Memory Information Exchange. In IEEE Transactions on Nuclear Science, 36(1), 1989."},{"key":"6_CR18","volume-title":"The Computer Journal 35(5)","author":"H Sondergaard","year":"1992","unstructured":"H. Sondergaard and P. Sestoft. Non-determinism in functional languages. In The Computer Journal, 35(5), 1992."}],"container-title":["Proof in VDM: Case Studies"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-1532-8_6.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T05:47:37Z","timestamp":1605678457000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-1532-8_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540761860","9781447115328"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-1532-8_6","relation":{},"subject":[],"published":{"date-parts":[[1998]]}}}