{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T11:41:01Z","timestamp":1725536461762},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642032363"},{"type":"electronic","value":"9783642032370"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03237-0_23","type":"book-chapter","created":{"date-parts":[[2009,8,3]],"date-time":"2009-08-03T05:24:37Z","timestamp":1249277077000},"page":"343-359","source":"Crossref","is-referenced-by-count":1,"title":["Inter-program Properties"],"prefix":"10.1007","author":[{"given":"Andrei","family":"Voronkov","sequence":"first","affiliation":[]},{"given":"Iman","family":"Narasamdya","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11823230_20","volume-title":"Static Analysis","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 301\u2013317. Springer, Heidelberg (2006)"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL, pp. 14\u201325 (2004)","DOI":"10.1145\/964001.964003"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Proceedings of Symposium in Applied Mathematics, pp. 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"23_CR4","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. CACM\u00a012(10), 576\u2013580 (1969)","journal-title":"CACM"},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"Lacey, D., Jones, N.D., Van Wyk, E., Frederiksen, C.C.: Proving correctness of compiler optimizations by temporal logic. In: POPL (2002)","DOI":"10.1145\/503272.503299"},{"key":"23_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-96753-4","volume-title":"The Foundations of Program Verification","author":"J. Leockx","year":"1987","unstructured":"Leockx, J., Sieber, K., Stansifer, R.D.: The Foundations of Program Verification, 2nd edn. John Wiley & Sons, Inc., New York (1987)","edition":"2"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: PLDI, pp. 220\u2013231 (2003)","DOI":"10.1145\/781131.781156"},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: POPL (2005)","DOI":"10.1145\/1040305.1040335"},{"issue":"1","key":"23_CR9","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111320.1111042","volume":"41","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. SIGPLAN Not.\u00a041(1), 42\u201354 (2006)","journal-title":"SIGPLAN Not."},{"issue":"2","key":"23_CR10","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1145\/359340.359353","volume":"21","author":"Z. Manna","year":"1978","unstructured":"Manna, Z., Waldinger, R.: Is \u201csometime\u201d sometimes better than \u201calways\u201d?: Intermittent assertions in proving program correctness. CACM\u00a021(2), 159\u2013172 (1978)","journal-title":"CACM"},{"key":"23_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/11547662_18","volume-title":"Static Analysis","author":"I. Narasamdya","year":"2005","unstructured":"Narasamdya, I., Voronkov, A.: Finding basic block and variable correspondence. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 251\u2013267. Springer, Heidelberg (2005)"},{"key":"23_CR12","unstructured":"Narasamdya, I.: Establishing Program Equivalence in Translation Validation for Optimizing Compilers. PhD thesis, The University of Manchester (2007), http:\/\/www-verimag.imag.fr\/~narasamd\/NarasamdyaThesis.ps"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Narasamdya, I., P\u00e9rin, M.: Certification of smart-card applications in common criteria. Technical Report TR-2008-14, Verimag (September 2008)","DOI":"10.1145\/1529282.1529409"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI), June 2000, pp. 83\u201395 (2000)","DOI":"10.1145\/349299.349314"},{"key":"23_CR15","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, p. 151. Springer, Heidelberg (1998)"},{"key":"23_CR16","unstructured":"Pnueli, A., Zaks, A.: Translation validation of interprocedural optimizations. In: Proceedings of 4th International Workshop on Software Verification and Validation (2006)"},{"issue":"1","key":"23_CR17","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/565816.503302","volume":"37","author":"F. Pottier","year":"2002","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ml. SIGPLAN Not.\u00a037(1), 319\u2013330 (2002)","journal-title":"SIGPLAN Not."},{"key":"23_CR18","unstructured":"Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy (July 1999)"},{"key":"23_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/964001.964002","volume-title":"Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Symbolic transfer function-based approaches to certified compilation. In: Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 1\u201313. ACM Press, New York (2004)"},{"key":"23_CR20","unstructured":"Voronkov, A., Narasamdya, I.: Proving inter-program properties. Technical Report TR-2008-13, Verimag (2008)"},{"issue":"1-3","key":"23_CR21","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1016\/j.tcs.2006.12.036","volume":"375","author":"H. Yang","year":"2007","unstructured":"Yang, H.: Relational separation logic. Theor. Comput. Sci.\u00a0375(1-3), 308\u2013334 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR22","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: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 35\u201351. Springer, Heidelberg (2008)"},{"issue":"3","key":"23_CR23","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":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03237-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T06:18:20Z","timestamp":1685081900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03237-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032363","9783642032370"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03237-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}