{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:20:43Z","timestamp":1742617243850,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540635338"},{"type":"electronic","value":"9783540695936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63533-5_15","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:28:40Z","timestamp":1330298920000},"page":"278-297","source":"Crossref","is-referenced-by-count":7,"title":["Towards an Integrated CASE and theorem proving tool for VDM-SL"],"prefix":"10.1007","author":[{"given":"Sten","family":"Agerholm","sequence":"first","affiliation":[]},{"given":"Jacob","family":"Frost","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"15_CR1","unstructured":"S. Agerholm. Mechanizing program verification in HOL. In Proceedings of the 1991 International Workshop on the HOL Theorem Proving System and Its Applications. IEEE Computer Society Press, 1992. A full version is in Technical Report IR-111, University of Aarhus, Department of Computer Science, Denmark."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"S. Agerholm. Translating specifications in VDM-SL to PVS. In J. von Wright, J. Grundy, and J. Harrison, editors, Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96), volume 1125 of Lecture Notes in Computer Science. Springer-Verlag, 1996.","DOI":"10.1007\/BFb0105393"},{"key":"15_CR3","doi-asserted-by":"crossref","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'97), LNCS. Springer-Verlag, August 1997.","DOI":"10.1007\/BFb0028382"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"B. Aichernig and P. G. Larsen. A proof obligation generator for VDM-SL. In FME'97, LNCS. Springer-Verlag, September 1997.","DOI":"10.1007\/3-540-63533-5_18"},{"key":"15_CR5","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H. Barringer","year":"1984","unstructured":"H. Barringer, J. H. Cheng, and C. B. Jones. A logic covering undefinedness in program proofs. Acta Informatica, 21:251\u2013269, 1984.","journal-title":"Acta Informatica"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"J. C. Bicarregui, J. S. Fitzgerald, P. A. Lindsay, R. Moore, and B. Ritchie. Proof in VDM: A Practitioner's Guide. FACIT. Springer-Verlag, 1994.","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"15_CR7","unstructured":"J. H. Cheng. A logic for partial functions. Ph.D. Thesis UMCS-86-7-1, Department of Computer Science, University of Manchester, Manchester M13 9PL, England, 1986."},{"issue":"9","key":"15_CR8","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/185009.185028","volume":"29","author":"R. Elmstr\u00f8m","year":"1994","unstructured":"R. Elmstr\u00f8m, P. G. Larsen, and P. B. Lassen. The IFAD VDM-SL Toolbox: A practical approach to formal specifications. ACM Sigplan Notices, 29(9):77\u201380, September 1994.","journal-title":"ACM Sigplan Notices"},{"key":"15_CR9","unstructured":"John Fitzgerald and Peter Corm Larsen. Software System Design: formal methods into practice. Camdridge University Press, The Edinburgh Building, Cambridge CB2 2RU, UK, 1997. To appear."},{"key":"15_CR10","unstructured":"IFAD World Wide Web page. http:\/\/www.ifad.dk."},{"key":"15_CR11","unstructured":"C. B. Jones. Systematic Software Development using VDM Prentice-Hall International Series in Computer Science. Prentice-Hall, 1986."},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"C. B. Jones, K. D. Jones, P. A. Lindsay, and R. Moore. mural: A Formal Development Support System. Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4471-3180-9"},{"issue":"1","key":"15_CR13","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1007\/BF01211050","volume":"8","author":"P. G. Larsen","year":"1996","unstructured":"P. G. Larsen and B. S. Hansen. Semantics for underdetermined expressions. Formal Aspects of Computing, 8(1):47\u201366, January 1996.","journal-title":"Formal Aspects of Computing"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"P. Mukherjee. Computer-aided validation of formal specifications. Software Engineering Journal, pages 133\u2013140, July 1995.","DOI":"10.1049\/sej.1995.0017"},{"key":"15_CR15","series-title":"Number 828 in Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lecture Notes in Computer Science. Springer-Verlag, Berlin, 1994."},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"F. Henning and C. Elliott. Higher-order abstract syntax. In Proceedings of the SIGPLAN'88 Conference on Programming Language Design and Implementation, pages 199\u2013208, Atlanta, Georgia, June 1998.","DOI":"10.1145\/53990.54010"},{"key":"15_CR17","unstructured":"PVS World Wide Web page. http:\/\/www.csl.sri.com\/pvs\/overview.html."},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"K. J. Ross and P. A. Lindsay. Maintaining consistency under changes to formal specifications. In J.C.P. Woodcock and P.G. Larsen, editors, FME'93: Industrial Strength Formal Methods, pages 558\u2013577. Formal Methods Europe, Springer-Verlag, April 1993. Lecture Notes in Computer Science 670.","DOI":"10.1007\/BFb0024667"}],"container-title":["Lecture Notes in Computer Science","FME '97: Industrial Applications and Strengthened Foundations of Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63533-5_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:43:34Z","timestamp":1742600614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}