{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T00:06:31Z","timestamp":1759190791369,"version":"3.44.0"},"publisher-location":"London","reference-count":20,"publisher":"Springer London","isbn-type":[{"type":"print","value":"9783540197577"},{"type":"electronic","value":"9781447135012"}],"license":[{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1992,1,1]],"date-time":"1992-01-01T00:00:00Z","timestamp":694224000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/978-1-4471-3501-2_11","type":"book-chapter","created":{"date-parts":[[2013,2,1]],"date-time":"2013-02-01T11:32:03Z","timestamp":1359718323000},"page":"193-209","source":"Crossref","is-referenced-by-count":1,"title":["An Approach to Automatic Proof Support for Code Generator Verification"],"prefix":"10.1007","author":[{"given":"Bettina","family":"Buth","sequence":"first","affiliation":[]},{"given":"Karl-Heinz","family":"Buth","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","volume-title":"Prentice-hall","author":"J Bakker","year":"1980","unstructured":"de Bakker J. Mathematical Theory of Program Correctness. Prentice-Hall, 1980"},{"key":"11_CR2","first-page":"61","volume-title":"The Meta-Language. Springer, Lncs","author":"D Bj\u00f8rner","year":"1978","unstructured":"Bj\u00f8rner D., Jones CB. The Vienna Development Method: The Meta-Language. Springer, LNCS 61, 1978"},{"key":"11_CR3","volume-title":"Academic Press","author":"R Boyer","year":"1988","unstructured":"Boyer RS, Moore JS. A Computational Logic Handbook. Academic Press, 1988"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-15976-2_1","volume-title":"Proceedings of the First International Conference on Rewriting Techniques and Applications. Springer, Lncs","author":"B Buchberger","year":"1985","unstructured":"Buchberger B. \u201cBasic Features and Development of the Critical Pairs\/-Completion Procedure\u201d. In: Jouannaud JP (ed.) Proceedings of the First International Conference on Rewriting Techniques and Applications. Springer, LNCS 202, pp. 1\u201345, 1985"},{"key":"11_CR5","volume-title":"Kiel","author":"B Buth","year":"1988","unstructured":"Buth B. PACS - Implementierung einer computergest\u00fctzten Verifikation f\u00fcr die Substitutionsphase von Codegenerator-Spezifikationen im CAT-System. Diplomarbeit, Christian-Albrechts-Universit\u00e4t, Kiel, 1988"},{"key":"11_CR6","volume-title":"Kiel","author":"KH Buth","year":"1988","unstructured":"Buth K-H. Beweis der partiellen Korrektheit von Codegenerator-Spezifikationen mit Hilfe von Termersetzung. Diplomarbeit, Christian-AlbrechtsUniversit\u00e4t, Kiel, 1988"},{"key":"11_CR7","first-page":"406","volume-title":"Vdm 88, Vdm \u2014 The Way Ahead, Proceedings of the 2nd VDM-Europe Symposium. Springer, Lncs","author":"B Buth","year":"1988","unstructured":"Buth B, Buth K-H. \u201cCorrectness Proofs for META IV Written Code Generator Specifications Using Term Rewriting\u201d. In: Bloomfield R et al. (eds.) VDM \u201888, VDM \u2014 The Way Ahead, Proceedings of the 2nd VDM-Europe Symposium. Springer, LNCS 328, pp. 406\u2013433, 1988"},{"key":"11_CR8","volume-title":"Technical Report [Kiel BB 2], ESPRIT BRA 3104 ProCoS, Christian-AlbrechtsUniversit\u00e4t Kiel","author":"B Buth","year":"1989","unstructured":"Buth B et al. Experiments with Program Verification Systems. Technical Report [Kiel BB 2], ESPRIT BRA 3104 ProCoS, Christian-AlbrechtsUniversit\u00e4t Kiel, 1989"},{"key":"11_CR9","volume-title":"Pitman","author":"J Dawes","year":"1991","unstructured":"Dawes J. The VDM-SL Reference Guide. Pitman, 1991"},{"key":"11_CR10","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/3-540-15976-2_9","volume-title":"Proceedings of the First International Conference on Rewriting Techniques and Applications. Springer, Lncs","author":"N Dershowitz","year":"1985","unstructured":"Dershowitz N. \u201cTermination\u201d In: Jouannaud JP (ed.). Proceedings of the First International Conference on Rewriting Techniques and Applications. Springer, LNCS 202, pp. 180\u2013224, 1985"},{"key":"11_CR11","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-51081-8_105","volume-title":"Proceedings of the Third International Conference on Rewriting Techniques and Applications. Springer, Lncs 355","author":"S Garland","year":"1989","unstructured":"Garland SJ, Guttag JV. \u201cAn Overview of LP, The Larch Prover\u201d. In: Dershowitz N (ed.). Proceedings of the Third International Conference on Rewriting Techniques and Applications. Springer, LNCS 355, pp. 137\u2013151, 1989"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Gordon MJ, Milner R, Wadsworth CP. Edinburgh LCF. Springer, LNCS 78, 1979","DOI":"10.1007\/3-540-09724-4"},{"key":"11_CR13","first-page":"349","volume-title":"Formal Languages: Perspectives and Open Problems","author":"G Huet","year":"1980","unstructured":"Huet G, Oppen DC. \u201cEquations and Rewrite Rules: A Survey\u201d. In: Book RV (ed.). Formal Languages: Perspectives and Open Problems. Academic Press, New York, pp. 349\u2013405, 1980"},{"key":"11_CR14","volume-title":"Prentice Hall International","author":"C Jones","year":"1990","unstructured":"Jones CB. Systematic Software Development Using VDM. Prentice Hall International, 1990"},{"key":"11_CR15","volume-title":"Wileyteubner","author":"J Loeckx","year":"1984","unstructured":"Loeckx J, Sieber K. The Foundations of Program Verification. WileyTeubner, 1984"},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-50214-9_23","volume-title":"Vdm 88, Vdm - The Way Ahead, Proceedings of the 2nd VDM-Europe Symposium. Springer, Lncs 328","author":"R Milne","year":"1988","unstructured":"Milne R. \u201cProof Rules for VDM Statements\u201d. In: Bloomfield R et al. (eds.). VDM \u201888, VDM - The Way Ahead, Proceedings of the 2nd VDM-Europe Symposium. Springer, LNCS 328, pp. 318\u2013336, 1988"},{"key":"11_CR17","first-page":"115","volume-title":"Safety of Computer Control Systems 1988. Ifac Proceedings Series, Vol. 16, Pergamon Press","author":"I O\u2019Neill","year":"1988","unstructured":"O\u2019Neill IM et al. \u201cThe Formal Verification of Safety-critical Assembly Code\u201d. In: Ehrenberger WD (ed.). Safety of Computer Control Systems 1988. IFAC Proceedings Series, Vol. 16, Pergamon Press, pp. 115\u2013120, 1988"},{"key":"11_CR18","volume-title":"Dissertation, Christian-Albrechts-Universit\u00e4t, Kiel","author":"U Schmidt","year":"1983","unstructured":"Schmidt U. Ein neuartiger, auf VDM basierender Codegenerator Generator. Dissertation, Christian-Albrechts-Universit\u00e4t, Kiel, 1983"},{"issue":"6","key":"11_CR19","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1145\/502949.502894","volume":"19","author":"U Schmidt","year":"1984","unstructured":"Schmidt U, V\u00f6ller R. \u201cA Multi-Language Compiler System with Automatically Generated Codegenerators\u201d. In: Proceedings of the SIGPLAN \u201884 Symposium on Compiler Construction. ACM SIGPLAN Notices, Vol. 19(6), pp. 202\u2013212, 1984","journal-title":"Acm Sigplan Notices, Vol"},{"key":"11_CR20","volume-title":"Christian-albrechts-universit\u00e4t, Kiel","author":"R V\u00f6ller","year":"1983","unstructured":"V\u00f6ller R. Entwicklung einer maschinenunabh\u00e4ngigen Zwischensprache und zugeh\u00f6riger Ubersetzeroberteile f\u00fcr ein Mehrsprachen\u00fcbersetzersystem mit Hilfe von VDM. Dissertation, Christian-Albrechts-Universit\u00e4t, Kiel, 1983"}],"container-title":["Workshops in Computing","Code Generation \u2014 Concepts, Tools, Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-3501-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T09:07:21Z","timestamp":1759136841000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-1-4471-3501-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540197577","9781447135012"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-3501-2_11","relation":{},"ISSN":["1431-1682"],"issn-type":[{"type":"print","value":"1431-1682"}],"subject":[],"published":{"date-parts":[[1992]]}}}