{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T13:26:45Z","timestamp":1726406805337},"publisher-location":"Berlin, Heidelberg","reference-count":31,"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_18","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:28:36Z","timestamp":1330298916000},"page":"338-357","source":"Crossref","is-referenced-by-count":17,"title":["A proof obligation generator for VDM-SL"],"prefix":"10.1007","author":[{"given":"Bernhard K.","family":"Aichernig","sequence":"first","affiliation":[]},{"given":"Peter Gorm","family":"Larsenz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"J.-R. Abrial. The B Book-Assigning Programs to Meanings. Cambridge University Press, August 1996.","DOI":"10.1017\/CBO9780511624162"},{"key":"18_CR2","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":"18_CR3","doi-asserted-by":"crossref","unstructured":"S. Agerholm and J. Frost. Towards an integrated CASE and theorem proving tool for VDM-SL. FME'97, September 1997.","DOI":"10.1007\/3-540-63533-5_15"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Bernhard K. Aichernig. A Proof Obligation Generator for the IFAD VDM-SL Toolbox. Master's thesis, Technical University Graz, Austria, March 1997.","DOI":"10.1007\/3-540-63533-5_18"},{"issue":"4","key":"18_CR5","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. Apt","year":"1981","unstructured":"K. Apt. Ten Years of Hoare's Logic: A survey \u2014 Part I. ACM-TOPLAS, 3(4):431\u2013483, Oct 1981.","journal-title":"ACM-TOPLAS"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Juan Bicarregui, John Fitzgerald, Peter Lindsay, Richard Moore, and Brian Ritchie. Proof in VDM: A Practitioner's Guide. FACIT. Springer-Verlag, 1994. ISBN 3-540-19813-X.","DOI":"10.1007\/978-1-4471-2033-9"},{"key":"18_CR7","doi-asserted-by":"crossref","unstructured":"Hans Bruun, Flemming Damm, and Bo Stig Hansen. An Approach to the Static Semantics of VDM-SL. In VDM '91: Formal Software Development Methods, pages 220-253. VDM Europe, Springer-Verlag, October 1991.","DOI":"10.1007\/3-540-54834-3_15"},{"key":"18_CR8","unstructured":"Bernard Carre, William Marsh, and Jon Garnsworthy. SPARK: A Safety-Related Ada Subset. In Ada UK Conference, pages 1\u201319, August 22 1992."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Dan Craigen, Sentot Kromodimoeljo, Irwin Meisels, Bill Pase, and Mark Saaltink. Eves: An overview. In S. Prehn and W.J. Toetenel, editors, VDM'91-Formal Software Development Methods, pages 389\u2013405. Springer-Verlag, October 1991.","DOI":"10.1007\/3-540-54834-3_24"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"Flemming Damm, Hans Bruun, and Bo Stig Hansen. On Type Checking in VDM and Related Consistency Issues. In VDM '91: Formal Software Development Methods, pages 45\u201362. VDM Europe, Springer-Verlag, October 1991.","DOI":"10.1007\/3-540-54834-3_6"},{"key":"18_CR11","unstructured":"Flemming M. Damm and Bo Stig Hansen. Generation of Proof Obligations for Type Consistency. Technical Report 1993-123, Department of Computer Science, Technical University of Denmark, December 1993."},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"John Dawes. The VDM-SL Reference Guide. Pitman, 1991. ISBN 0-273-03151-1.","DOI":"10.1201\/9781482267419"},{"issue":"9","key":"18_CR13","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1145\/185009.185028","volume":"29","author":"R. Elmstrom","year":"1994","unstructured":"Ren\u00e8 Elmstrom, Peter Gorm Larsen, and Poul B\u00f8gh 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":"18_CR14","unstructured":"Jon Garnsworthy, Ian O'Neill, and Bernhard Carr\u00e8. Automatic Proof of Absence of Run-time Errors. In Ada UK Conference. London Docklands, October 1993."},{"key":"18_CR15","unstructured":"The RAISE Language Group. The RAISE Specification Language. The BCSPractitioners Series. Prentice-Hall, 1992."},{"key":"18_CR16","unstructured":"The VDM Tool Group. User Manual for the IFAD VDM-SL Toolbox. Technical report, IFAD, May 1996. IFAD-VDM-4."},{"key":"18_CR17","unstructured":"Howard Haughton. Specification in B: An Introduction Using the B Toolkit. World Scientific Publishing, 1996."},{"key":"18_CR18","unstructured":"I.J. Hayes, C.B. Jones, and J.E. Nicholls. Understanding the Differences Between VDM and Z. FRCS Europe, pages 7\u201330, Autumn 1993."},{"issue":"10","key":"18_CR19","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An Axiomatic Basis for Computer Programming. Communications of teh ACM, 12(10):576\u2013581, October 1969.","journal-title":"Communications of teh ACM"},{"key":"18_CR20","doi-asserted-by":"crossref","unstructured":"Cliff Jones, Kevin Jones, Peter Linsay, and Richard Moore, editors. mural: A Formal Development Support System. Springer-Verlag, 1991. ISBN 3-540-19651-X.","DOI":"10.1007\/978-1-4471-3180-9"},{"key":"18_CR21","unstructured":"Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, Englewood Cliffs, New Jersey, second edition, 1990. ISBN 0-13-880733-7."},{"key":"18_CR22","unstructured":"Peter Corm Larsen. Towards Proof Rules for VDM-SL. PhD thesis, Technical University of Denmark, Department of Computer Science, March 1995. ID-TR:1995-160."},{"key":"18_CR23","unstructured":"P.G. Larsen, B. S. Hansen, H. Brunn, N. Plat, H. Toetenel, D. J. Andrews, J. Dawes, G. Parkin, and et. al. Information Technology-Programming languages, their environments and system software interfaces-Vienna Development Method-Specification Language-Part 1: Base language, ISO\/IEC 13817-1, December 1996."},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Paul Mukherjee. Computer-aided Validation of Formal Specifications. Software Engineering Journal, pages 133\u2013140, July 1995.","DOI":"10.1049\/sej.1995.0017"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal Verification for Fault-Tolerant Architectures: Some Lessons Learned. In J.C.P. Woodcock and P.G. Larsen, editors, FME'93: Industrial-Strength Formal Methods, pages 482\u2013501. Formal Methods Europe, Springer-Verlag, April 1993. Lecture Notes in Computer Science 670.","DOI":"10.1007\/BFb0024663"},{"issue":"8","key":"18_CR26","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/142137.142153","volume":"27","author":"N. Plat","year":"1992","unstructured":"Nico Plat and Peter Gorm Larsen. An Overview of the ISO\/VDM-SL Standard. Sigplan Notices, 27(8):76\u201382, August 1992.","journal-title":"Sigplan Notices"},{"key":"18_CR27","unstructured":"The RAISE Method Group. The RAISE Development Method. The BCS Practitioners Series. Prentice-Hall International, 1995."},{"key":"18_CR28","doi-asserted-by":"crossref","unstructured":"Mark Saaltink. Z and EVES. In J.E. Nicholls, editor, Z User Workshop, York 1991, pages 223\u2013242. Springer-Verlag, 1992. Workshops in Computing.","DOI":"10.1007\/978-1-4471-3203-5_11"},{"key":"18_CR29","unstructured":"Mark Saaltink. The Z\/EVES system. Technical report, ORA Canada, September 1995."},{"key":"18_CR30","unstructured":"R.D. Tennent. Principles of Programming Languages. Prentice-Hall International, Englewood Cliffs, New Jersey 07632, 1981."},{"key":"18_CR31","unstructured":"The VDM Tool Group. The IFAD VDM-SL Language. Technical report, IFAD, May 1996. IFAD-VDM-1."}],"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_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T11:49:51Z","timestamp":1640951391000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63533-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540635338","9783540695936"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-63533-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}