{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:50:56Z","timestamp":1725511856484},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540797067"},{"type":"electronic","value":"9783540797074"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-79707-4_8","type":"book-chapter","created":{"date-parts":[[2008,5,7]],"date-time":"2008-05-07T06:37:44Z","timestamp":1210142264000},"page":"85-100","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification with Isabelle\/HOL in Practice: Finding a Bug in the GCC Scheduler"],"prefix":"10.1007","author":[{"given":"Lars","family":"Gesellensetter","sequence":"first","affiliation":[]},{"given":"Sabine","family":"Glesner","sequence":"additional","affiliation":[]},{"given":"Elke","family":"Salecker","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Elsevier ENTCS","first-page":"1","volume-title":"Compiler Optimization meets Compiler Verification (COCV 2005)","author":"J.O. Blech","year":"2005","unstructured":"Blech, J.O., Glesner, S., Leitner, J., M\u00fclling, S.: Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle\/HOL. In: Compiler Optimization meets Compiler Verification (COCV 2005). Elsevier ENTCS, pp. 1\u201318. Elsevier, Amsterdam (2005)"},{"issue":"1","key":"8_CR2","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/200836.200880","volume":"42","author":"M. Blum","year":"1995","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. J. ACM\u00a042(1), 269\u2013291 (1995)","journal-title":"J. ACM"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans.\u00a0on Prog.\u00a0Lang.\u00a0and Systems\u00a013(4) (1991)","DOI":"10.1145\/115372.115320"},{"issue":"4","key":"8_CR5","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1142\/S0129054103001947","volume":"14","author":"A. Dold","year":"2003","unstructured":"Dold, A., von Henke, F.W., Goerigk, W.: A Completely Verified Realistic Bootstrap Compiler. Int.\u00a0Journal of Foundations of Computer Science\u00a014(4), 659\u2013680 (2003)","journal-title":"Int.\u00a0Journal of Foundations of Computer Science"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/513829.513844","volume-title":"Languages, Compilers and Tools for Embedded Systems (LCTES\/SCOPES 2002)","author":"X. Feng","year":"2002","unstructured":"Feng, X., Hu, A.J.: Automatic formal verification for scheduled VLIW code. In: Languages, Compilers and Tools for Embedded Systems (LCTES\/SCOPES 2002), pp. 85\u201392. ACM Press, New York (2002)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Compiler Construction","author":"W. Goerigk","year":"1996","unstructured":"Goerigk, W., Dold, A., Gaul, T., Goos, G., Heberle, A., von Henke, F.W., Hoffmann, U., Langmaack, H., Pfeifer, H., Ruess, H., Zimmermann, W.: Compiler Correctness and Implementation Verification: The Verifix Approach. In: Gyim\u00f3thy, T. (ed.) CC 1996. LNCS, vol.\u00a01060, Springer, Heidelberg (1996)"},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1524\/itit.46.5.265.44799","volume":"46","author":"S. Glesner","year":"2004","unstructured":"Glesner, S., Goos, G., Zimmermann, W.: Verifix: Konstruktion und Architektur verifizierender \u00dcbersetzer (Verifix: Construction and Architecture of Verifying Compilers). it - Information Technology\u00a046, 265\u2013276 (2004)","journal-title":"it - Information Technology"},{"issue":"3","key":"8_CR9","first-page":"191","volume":"9","author":"S. Glesner","year":"2003","unstructured":"Glesner, S.: Using Program Checking to Ensure the Correctness of Compiler Implementations. Journal of Universal Comp.\u00a0Science\u00a09(3), 191\u2013222 (2003)","journal-title":"Journal of Universal Comp.\u00a0Science"},{"key":"8_CR10","unstructured":"The GNU Project. GNU binutils version 2.17 (2006), http:\/\/www.gnu.org\/software\/binutils\/"},{"key":"8_CR11","series-title":"Elsevier ENTCS","volume-title":"Compiler Optimization meets Compiler Verification (COCV 2004)","author":"B. Goldberg","year":"2004","unstructured":"Goldberg, B., Zuck, L., Barrett, C.: Into the Loops: Practical Issues in Translation Validation for Optimizing Compilers. In: Compiler Optimization meets Compiler Verification (COCV 2004). Elsevier ENTCS. Elsevier, Amsterdam (2004)"},{"key":"8_CR12","unstructured":"Intel Corporation. Intel Itanium architecture software developer\u2019s manual: Volume 3: Instruction set reference. Revision 2.2 (January 2006)"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1109\/ISQED.2006.10","volume-title":"7th Int.\u00a0Symposium on Quality Electronic Design (ISQED 2006)","author":"C. Karfa","year":"2006","unstructured":"Karfa, C., Mandal, C., Sarkar, D., Pentakota, S.R., Reade, C.: A formal verification method of scheduling in high-level synthesis. In: 7th Int.\u00a0Symposium on Quality Electronic Design (ISQED 2006), pp. 71\u201378. IEEE, Los Alamitos (2006)"},{"key":"8_CR14","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1016\/S0304-3975(02)00869-1","volume":"298","author":"G. Klein","year":"2003","unstructured":"Klein, G., Nipkow, T.: Verified Bytecode Verifiers. Theoretical Computer Science\u00a0298, 583\u2013626 (2003)","journal-title":"Theoretical Computer Science"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"POPL 2006: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Mehlhorn, K., N\u00e4her, S.: From algorithms to working programs: On the use of program checking in leda. In: MFCS, pp. 84\u201393 (1998)","DOI":"10.1007\/BFb0055759"},{"issue":"4","key":"8_CR17","first-page":"461","volume":"5","author":"J.S. Moore","year":"1989","unstructured":"Moore, J.S.: A Mechanically Verified Language Implementation. Journal of Automated Reasoning\u00a05(4), 461\u2013492 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-Carrying Code. In: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997) (1997)","DOI":"10.1145\/263699.263712"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation Validation for an Optimizing Compiler. In: Programming Language Design and Implementation (PLDI 2000) (2000)","DOI":"10.1145\/349299.349314"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055126","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Verified Lexical Analysis. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 1\u201315. Springer, Heidelberg (1998)"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"8_CR22","volume-title":"25th ACM Symposium on the Principles of Programming Languages","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T., von Oheimb, D.: Java light is Type-Safe \u2013 Definitely. In: 25th ACM Symposium on the Principles of Programming Languages. ACM Press, New York (1998)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/3-540-45732-1_29","volume-title":"Computer Safety, Reliability and Security","author":"F. Ortmeier","year":"2002","unstructured":"Ortmeier, F., Schellhorn, G., Thums, A., Reif, W., Hering, B., Trappschuh, H.: Safety Analysis of the Height Control System of the Elbtunnel. In: Anderson, S., Bologna, S., Felici, M. (eds.) SAFECOMP 2002. LNCS, vol.\u00a02434, pp. 296\u2013308. Springer, Heidelberg (2002)"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"8_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Automated Deduction - CADE-18","author":"M. Strecker","year":"2002","unstructured":"Strecker, M.: Formal Verification of a Java Compiler in Isabelle. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, pp. 63\u201377. Springer, Heidelberg (2002)"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Wasserrab, D., Nipkow, T., Snelting, G., Tip, F.: An operational semantics and type safety proof for multiple inheritance in C++. In: OOPSLA, pp. 345\u2013362 (2006)","DOI":"10.1145\/1167515.1167503"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-79707-4_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:28:40Z","timestamp":1619522920000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-79707-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540797067","9783540797074"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-79707-4_8","relation":{},"subject":[]}}