{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:52Z","timestamp":1775873632707,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540682356","type":"print"},{"value":"9783540682370","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-68237-0_5","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T01:36:00Z","timestamp":1212543360000},"page":"35-51","source":"Crossref","is-referenced-by-count":80,"title":["CoVaC: Compiler Validation by Program Analysis of the Cross-Product"],"prefix":"10.1007","author":[{"given":"Anna","family":"Zaks","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","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)"},{"issue":"3","key":"5_CR2","first-page":"223","volume":"9","author":"L. Zuck","year":"2003","unstructured":"Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: VOC: A methodology for the translation validation of optimizing compilers. Journal of Universal Computer Science\u00a09(3), 223\u2013247 (2003)","journal-title":"Journal of Universal Computer Science"},{"key":"5_CR3","first-page":"83","volume-title":"Programming Language Design and Implementation","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation, pp. 83\u201395. ACM Press, New York (2000)"},{"key":"5_CR4","first-page":"1","volume-title":"POPL","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Symbolic transfer function-based approaches to certified compilation. In: POPL, pp. 1\u201313. ACM Press, New York (2004)"},{"key":"5_CR5","first-page":"100","volume-title":"Computer Security Foundations Workshop","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Computer Security Foundations Workshop, p. 100. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"5_CR6","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: The LLVM Compiler Infrastructure Project, \n                    \n                      http:\/\/llvm.org\/\n                    \n                    \n                  , \n                    \n                      http:\/\/llvm.org\/\n                    \n                    \n                  , \n                    \n                      http:\/\/llvm.org"},{"key":"5_CR7","unstructured":"Zaks, A., Pnueli, A.: CoVaC: Compiler validation by program analysis of the cross-product. Technical report, NYU (2007), \n                    \n                      http:\/\/cs.nyu.edu\/acsys\/publications.html"},{"key":"5_CR8","unstructured":"Pnueli, A.: Verification of procedural programs. In: We Will Show Them! Essays in Honour of Dov Gabbay, vol.\u00a02, pp. 543\u2013590. College Publications (2005)"},{"issue":"3","key":"5_CR9","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/s10703-005-3402-z","volume":"27","author":"L. Zuck","year":"2005","unstructured":"Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y.: Translation and run-time validation of loop tranformations. Formal Methods in System Design\u00a027(3), 335\u2013360 (2005)","journal-title":"Formal Methods in System Design"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Symposia in Applied Mathematics, vol.\u00a019, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"5_CR11","first-page":"342","volume-title":"POPL","author":"S. Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.: Global value numbering using random interpretation. In: POPL, pp. 342\u2013352. ACM Press, New York (2004)"},{"key":"5_CR12","unstructured":"The YICES SMT Solver, \n                    \n                      http:\/\/yices.csl.sri.com\n                    \n                    \n                  , \n                    \n                      http:\/\/yices.csl.sri.com"},{"key":"5_CR13","unstructured":"CVC3: An Automatic Theorem Prover for Satisfiability Modulo Theories (SMT), \n                    \n                      http:\/\/www.cs.nyu.edu\/acsys\/cvc3\/"},{"key":"5_CR14","unstructured":"Simpson, L.T.: Value-Driven Redundancy Elimination. PhD thesis, Rice University (1996)"},{"key":"5_CR15","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"5_CR16","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"5th GI-Conference on Theoretical Computer Science","author":"D. Park","year":"1981","unstructured":"Park, D.: Concurrency and automata on infinite sequences. In: 5th GI-Conference on Theoretical Computer Science, pp. 167\u2013183. Springer, Heidelberg (1981)"},{"key":"5_CR17","unstructured":"Fang, Y.: Translation Validation of Optimizing Compilers. PhD thesis, New York University (2005)"},{"key":"5_CR18","unstructured":"Pnueli, A., Zaks, A.: Validation of interprocedural optimizations. In: 7\n                    th\n                   International Workshop on Compiler Optimization Meets Compiler Verificaiton (2008)"},{"key":"5_CR19","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11823230_19","volume-title":"Static Analysis Symposium","author":"Y. Huang","year":"2006","unstructured":"Huang, Y., Childer, B.R., Soffa, M.L.: Catching and identifying bugs in register allocation. In: Static Analysis Symposium, pp. 281\u2013300. Springer, Heidelberg (2006)"},{"issue":"6","key":"5_CR20","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"M.A. Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes\u00a028(6), 2\u20132 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:43:46Z","timestamp":1620002626000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540682356","9783540682370"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_5","relation":{},"subject":[]}}