{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:11Z","timestamp":1725475811906},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540669302"},{"type":"electronic","value":"9783540466246"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/10703260_4","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T20:34:34Z","timestamp":1167510874000},"page":"62-73","source":"Crossref","is-referenced-by-count":2,"title":["Towards Rigorous Compiler Implementation Verification"],"prefix":"10.1007","author":[{"given":"Wolfgang","family":"Goerigk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Friedemann","family":"Simon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"4_CR1","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1145\/5397.30847","volume":"8","author":"L.M. Chirica","year":"1986","unstructured":"Chirica, L.M., Martin, D.F.: Toward Compiler Implementation Correctness Proofs. ACM Transactions on Programming Languages and Systems\u00a08(2), 185\u2013214 (1986)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_CR2","unstructured":"Curzon, P.: The Veried Compilation of Vista Programs. Internal Report, Computer Laboratory. University of Cambridge (January 1994)"},{"key":"4_CR3","unstructured":"Goerigk, W.: An Exercise in Program Verication: The ACL2 Correctness Proof of a Simple Theorem Prover Executable. Technical Report Verifix\/CAU\/2.4, CAU Kiel (1996)"},{"key":"4_CR4","unstructured":"Goerigk, W.: A Denotational Semantics for ComLisp and SIL. Technical Report Verifix\/CAU\/2.8, CAU Kiel (December 1997)"},{"key":"4_CR5","unstructured":"Goerigk, W., Dold, A., Gaul, T., Goos, G., Heberle, A., von Henke, F.W., Homann, U., Langmaack, H., Pfeifer, H., Ruess, H., Zimmermann, W.: Compiler Correctness and Implementation Verication: The Verix Approach. In: Fritzson, P. (ed.) Proceedings of the Poster Session of CC 1996 International Conference on Compiler Construction, IDA Technical Report LiTH-IDA-R-96-12, Link\u00f8ping, Sweden (1996)"},{"key":"4_CR6","volume-title":"Proceedings ATOOLS 1998 Workshop on \u201dTool Support for System Specication, Development, and Verification\u201d, Advances in Computing Science","author":"W. Goerigk","year":"1998","unstructured":"Goerigk, W., Gaul, T., Zimmermann, W.: Correct Programs without Proof? On Checker-Based Program Verication. In: Proceedings ATOOLS 1998 Workshop on \u201dTool Support for System Specication, Development, and Verification\u201d, Advances in Computing Science, Malente. Springer, Heidelberg (1998)"},{"key":"4_CR7","unstructured":"Goerigk, W., Homann, U.: The Compiler Implementation Language ComLisp. Technical Report Verifix\/CAU\/1.7, CAU Kiel (June 1996)"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","first-page":"71","volume-title":"Applied Formal Methods - FM-Trends 98","author":"W. Goerigk","year":"1998","unstructured":"Goerigk, W., Homann, U.: Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, p. 71. Springer, Heidelberg (1998) (to appear)"},{"key":"4_CR9","unstructured":"Goerigk, W., Homann, U.: The Compiling Specication from Com- Lisp to Executable Machine Code. Technical Report Nr. 9713, Institut f\u00fcr Informatik, CAU, Kiel (December 1998)"},{"key":"4_CR10","unstructured":"Goerigk, W., M\u00fcller-Olm, M.: Erhaltung partieller Korrektheit bei beschr\u00e4nkten Maschinenressourcen. Eine Beweisskizze. Technical Report Verifix\/CAU\/2.5, CAU Kiel (1996)"},{"key":"4_CR11","unstructured":"Guttman, J.D., Monk, L.G., Ramsdell, J.D., Farmer, W.M., Swarup, V.: A Guide to VLisp, A Veried Programming Language Implementation. Technical Report M92B091, The MITRE Corporation, Bedford, MA (September 1992)"},{"key":"4_CR12","first-page":"33","volume-title":"3rd Renement Workshop","author":"C.A.R. Hoare","year":"1991","unstructured":"Hoare, C.A.R.: Renement algebra proves correctness of compiling specifications. In: Morgan, C.C., Woodcock, J.C.P. (eds.) 3rd Renement Workshop, pp. 33\u201348. Springer, Heidelberg (1991)"},{"key":"4_CR13","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"C.A.R. Hoare","year":"1993","unstructured":"Hoare, C.A.R., Jifeng, H., Sampaio, A.: Normal Form Approach to Compiler Design. Acta Informatica\u00a030, 701\u2013739 (1993)","journal-title":"Acta Informatica"},{"key":"4_CR14","unstructured":"Homann, U.: \u00dcber die korrekte Implementierung von Compilern. InWorkshop Alternative Konzepte f\u00fcr Sprachen und Rechner, pp. 94\u2013105, Bad Honnef, Also available as Technical Report Verifix\/CAU\/3.1 (1996)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Hardware Specification, Verification and Synthesis: Mathematical Aspects","author":"J.J. Joyce","year":"1990","unstructured":"Joyce, J.J.: Totally Veried Systems: Linking Veried Software to Verified Hardware. In: Leeser, M., Brown, G. (eds.) Hardware Specification, Verification and Synthesis: Mathematical Aspects. LNCS, vol.\u00a0408. Springer, Heidelberg (1990)"},{"key":"4_CR16","unstructured":"Kaufmann, M., Moore, J.S.: Design Goals of ACL2. Technical Report 101, Computational Logic, Inc. (August 1994)"},{"key":"4_CR17","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1524\/itit.1997.39.3.41","volume":"97","author":"H. Langmaack","year":"1997","unstructured":"Langmaack, H.: Softwareengineering zur Zertizierung von Systemen: Spezikations-, Implementierungs-, \u00dcbersetzerkorrektheit. Informationstechnik und Technische Informatik it-ti\u00a097, 41\u201347 (1997)","journal-title":"Informationstechnik und Technische Informatik it-ti"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"McCarthy, J., Painter, J.A.: Correctness of a compiler for arithmetical expressions. In: Schwartz, J.T. (ed.) Proceedings of a Symposium in Applied Mathematics. Mathematical Aspects of Computer Science, vol.\u00a019. American Mathematical Society, Providence (1967)","DOI":"10.1090\/psapm\/019\/0242403"},{"key":"4_CR19","unstructured":"Moore, J.S.: Piton: A verified assembly level language. Technical Report 22, Comp. Logic Inc., Austin, Texas (1988)"},{"key":"4_CR20","volume-title":"Piton, A Mechanically Verified Assembly-Level Language","author":"J.S. Moore","year":"1996","unstructured":"Moore, J.S.: Piton, A Mechanically Verified Assembly-Level Language. Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"4_CR21","unstructured":"Moore, J.S., Kaufmann, M.: ACL2: An industrial strength version of Nqthm. In: Proceedings of COMPASS 1996 (June 1996)"},{"key":"4_CR22","unstructured":"M\u00fcller-Olm, M.: Three Views on Preservation of Partial Correctness. Technical Report Verifix\/CAU\/5.1, CAU Kiel (October 1996)"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification","author":"M. M\u00fcller-Olm","year":"1997","unstructured":"M\u00fcller-Olm, M.: Modular Compiler Verification. LNCS, vol.\u00a01283. Springer, Heidelberg (1997)"},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Conference Record of POPL 1997: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January 15\u201317, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17-19, vol.\u00a019, pp. 333\u2013344 (1998)","DOI":"10.1145\/277650.277752"},{"key":"4_CR26","unstructured":"Oliva, D.P., Wand, M.: A Veried Compiler for Pure PreScheme. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, Northeastern University (February 1992)"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verication System. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"4_CR28","unstructured":"Pfeifer, H., Dold, A., von Henke, F.W., Rue, B.H.: Mechanized Semantics of Simple Imperative Programming Constructs. Ulmer Informatik-Berichte 96-11, Universit\u00e4t Ulm (December 1996)"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-10886-6","volume-title":"Compiler Specification and Verification","author":"W. Polak","year":"1981","unstructured":"Polak, W.: Compiler specication and verication. In: Hartmanis, J., Goos, G. (eds.) Compiler Specification and Verification. LNCS, vol.\u00a0124. Springer, Heidelberg (1981)"},{"issue":"8","key":"4_CR30","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1145\/358198.358210","volume":"27","author":"K. Thompson","year":"1990","unstructured":"Thompson, K.: Reflections on Trusting Trust. Communications of the ACM\u00a027(8), 761\u2013763 (1990); Also in ACM Turing Award Lectures: The First Twenty Years 1965-1985. ACM Press, 1987, and in Computers Under Attack: Intruders, Worms, and Viruses Copyright. ACM Press (1990)","journal-title":"Communications of the ACM"},{"key":"4_CR31","volume-title":"Fourth International Conference on the World-Wide Web","author":"F. Yellin","year":"1995","unstructured":"Yellin, F.: Low level security in java. In: Fourth International Conference on the World-Wide Web, December 1995. MIT, Boston (1995)"}],"container-title":["Lecture Notes in Computer Science","Collaboration between Human and Artificial Societies"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10703260_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,7]],"date-time":"2021-08-07T04:56:18Z","timestamp":1628312178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10703260_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540669302","9783540466246"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/10703260_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}