{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,26]],"date-time":"2025-02-26T05:32:55Z","timestamp":1740547975337,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642157684"},{"type":"electronic","value":"9783642157691"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_3","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T06:09:40Z","timestamp":1284358180000},"page":"6-21","source":"Crossref","is-referenced-by-count":1,"title":["Translation Validation of Loop Optimizations and Software Pipelining in the TVOC Framework"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Goldberg","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/11513988_29","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2005","unstructured":"Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L.D.: TVOC: A translation validator for optimizing compilers. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 291\u2013295. Springer, Heidelberg (2005)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. Symp. Appl. Math., vol.\u00a019, pp. 19\u201331 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Goldberg, B., Crutcher, E., Huneycutt, C., Palem, K.: Software bubbles: Using predication to compensate for aliasing in software pipelines. In: International Conference on Parallel Architectures and Compilation Techniques, p. 211 (2002)","DOI":"10.1109\/PACT.2002.1106019"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Lam, M.: Software pipelining: an effective scheduling technique for vliw machines. In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI 1988), pp. 318\u2013328 (July 1988)","DOI":"10.1145\/960116.54022"},{"key":"3_CR6","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/581630.581676","volume-title":"CASES 2002: Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems","author":"R. Leviathan","year":"2002","unstructured":"Leviathan, R., Pnueli, A.: Validating software pipelining optimizations. In: CASES 2002: Proceedings of the 2002 International Conference on Compilers, Architecture, and Synthesis for Embedded Systems, pp. 280\u2013287. ACM Press, New York (2002)"},{"key":"3_CR7","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/349299.349314","volume-title":"PLDI 2000: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI 2000: Proceedings of the ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation, pp. 83\u201394. ACM Press, New York (2000)"},{"issue":"1","key":"3_CR8","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/s100090050027","volume":"2","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Shtrichman, O., Siegel, M.: The code validation tool CVT: Automatic verification of a compilation process. International Journal on Software Tools for Technology Transfer (STTT)\u00a02(1), 192\u2013201 (1998)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/BFb0055057","volume-title":"Automata, Languages and Programming","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Shtrichman, O., Siegel, M.: Translation validation for synchronous languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 235\u2013246. Springer, Heidelberg (1998)"},{"key":"3_CR10","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.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/3-540-48257-1_8","volume-title":"Applied Formal Methods - FM-Trends 98","author":"A. Pnueli","year":"1999","unstructured":"Pnueli, A., Shtrichman, O., Siegel, M.: Translation validation: From DC+ to C*. In: Hutter, D., Traverso, P. (eds.) FM-Trends 1998. LNCS, vol.\u00a01641, pp. 137\u2013150. Springer, Heidelberg (1999)"},{"key":"3_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-48092-7_11","volume-title":"Correct System Design","author":"A. Pnueli","year":"1999","unstructured":"Pnueli, A., Strichman, O., Siegel, M.: Translation validation: From SIGNAL to C. In: Olderog, E.-R., Steffen, B. (eds.) Correct System Design. LNCS, vol.\u00a01710, pp. 231\u2013255. Springer, Heidelberg (1999)"},{"key":"3_CR13","first-page":"183","volume-title":"MICRO 14: Proceedings of the 14th Annual Workshop on Microprogramming","author":"B.R. Rau","year":"1981","unstructured":"Rau, B.R., Glaeser, C.D.: Some scheduling techniques and an easily schedulable horizontal architecture for high performance scientific computing. In: MICRO 14: Proceedings of the 14th Annual Workshop on Microprogramming, Piscataway, NJ, USA, pp. 183\u2013198. IEEE Press, Los Alamitos (1981)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 500\u2013504. Springer, Heidelberg (2002)"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/1542476.1542512","volume-title":"PLDI 2009: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"J.-B. Tristan","year":"2009","unstructured":"Tristan, J.-B., Leroy, X.: Verified validation of lazy code motion. In: PLDI 2009: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 316\u2013326. ACM Press, New York (2009)"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/1706299.1706311","volume-title":"POPL 2010: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"J.-B. Tristan","year":"2010","unstructured":"Tristan, J.-B., Leroy, X.: A simple, verified validator for software pipelining. In: POPL 2010: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 83\u201392. ACM, New York (2010)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-540-68237-0_5","volume-title":"FM 2008: Formal Methods","author":"A. Zaks","year":"2008","unstructured":"Zaks, A., Pnueli, A.: CovaC: Compiler validation by program analysis of the cross-product. In: Cu\u00e9llar, J., Maibaum, T.S.E., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 35\u201351. Springer, Heidelberg (2008)"},{"issue":"3","key":"3_CR18","first-page":"223","volume":"9","author":"L.D. Zuck","year":"2003","unstructured":"Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: A methodology for the translation validation of optimizing compilers. J. UCS\u00a09(3), 223\u2013247 (2003)","journal-title":"J. UCS"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T18:44:49Z","timestamp":1740509089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_3"}},"subtitle":["In Memory of Amir Pnueli"],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}