{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T13:37:17Z","timestamp":1771940237616,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642214363","type":"print"},{"value":"9783642214370","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_17","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T03:33:16Z","timestamp":1308367996000},"page":"200-214","source":"Crossref","is-referenced-by-count":123,"title":["Relational Verification Using Product Programs"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Juan Manuel","family":"Crespo","sequence":"additional","affiliation":[]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","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":"17_CR2","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: Foccardi, R. (ed.) Computer Security Foundations Workshop, pp. 100\u2013114. IEEE Press, Los Alamitos (2004)"},{"key":"17_CR3","first-page":"90","volume-title":"Principles of Programming Languages","author":"G. Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Zanella B\u00e9guelin, S.: Formal certification of code-based cryptographic proofs. In: Shao, Z., Pierce, B.C. (eds.) Principles of Programming Languages, pp. 90\u2013101. ACM Press, New York (2009)"},{"key":"17_CR4","first-page":"14","volume-title":"Principles of Programming Languages","author":"N. Benton","year":"2004","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) Principles of Programming Languages, pp. 14\u201325. ACM Press, New York (2004)"},{"issue":"6","key":"17_CR5","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1145\/1743546.1743572","volume":"53","author":"J. Burnim","year":"2010","unstructured":"Burnim, J., Sen, K.: Asserting and checking determinism for multithreaded programs. Communications of the ACM\u00a053(6), 97\u2013105 (2010)","journal-title":"Communications of the ACM"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity analysis of programs. In: Principles of Programming Languages, pp. 57\u201370 (2010)","DOI":"10.1145\/1706299.1706308"},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Computer Security Foundations Symposium, pp. 51\u201365 (2008)","DOI":"10.1109\/CSF.2008.7"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"A. Darvas","year":"2005","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol.\u00a03450, pp. 193\u2013209. Springer, Heidelberg (2005)"},{"key":"17_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/11532231_9","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Dufay","year":"2005","unstructured":"Dufay, G., Felty, A.P., Matwin, S.: Privacy-sensitive information flow with JML. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 116\u2013130. Springer, Heidelberg (2005)"},{"key":"17_CR10","first-page":"466","volume-title":"Design Meets Automation","author":"B. Godlin","year":"2009","unstructured":"Godlin, B., Strichman, O.: Regression verification. In: Design Meets Automation, pp. 466\u2013471. ACM Press, New York (2009)"},{"issue":"1","key":"17_CR11","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.entcs.2005.01.030","volume":"132","author":"B. Goldberg","year":"2005","unstructured":"Goldberg, B., Zuck, L.D., Barrett, C.W.: Into the loops: Practical issues in translation validation for optimizing compilers. Electr. Notes Theor. Comput. Sci.\u00a0132(1), 53\u201371 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"17_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511721656","volume-title":"Foundations of Cryptography","author":"O. Goldreich","year":"2004","unstructured":"Goldreich, O.: Foundations of Cryptography. Cambridge University Press, Cambridge (2004)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Programming Languages Design and Implementation, pp. 327\u2013337 (2009)","DOI":"10.1145\/1542476.1542513"},{"issue":"3","key":"17_CR14","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1145\/291889.291895","volume":"20","author":"Y.A. Liu","year":"1998","unstructured":"Liu, Y.A., Stoller, S.D., Teitelbaum, T.: Static caching for incremental computation. ACM Transactions on Programming Languages and Systems\u00a020(3), 546\u2013585 (1998)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/11863908_18","volume-title":"Computer Security \u2013 ESORICS 2006","author":"D.A. Naumann","year":"2006","unstructured":"Naumann, D.A.: From coupling relations to mated invariants for checking information flow. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 279\u2013296. Springer, Heidelberg (2006)"},{"issue":"5","key":"17_CR16","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. ACM SIGPLAN Notices\u00a035(5), 83\u201394 (2000)","journal-title":"ACM SIGPLAN Notices"},{"key":"17_CR17","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., Singerman, E., Siegel, M.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"17_CR18","first-page":"157","volume-title":"ICFP","author":"J. Reed","year":"2010","unstructured":"Reed, J., Pierce, B.C.: Distance makes the types grow stronger: a calculus for differential privacy. In: Hudak, P., Weirich, S. (eds.) ICFP, pp. 157\u2013168. ACM, New York (2010)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T. Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 352\u2013367. Springer, Heidelberg (2005)"},{"issue":"1-3","key":"17_CR20","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. Theoretical Computer Science\u00a0375(1-3), 308\u2013334 (2007)","journal-title":"Theoretical Computer Science"},{"key":"17_CR21","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., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 35\u201351. Springer, Heidelberg (2008)"},{"issue":"3","key":"17_CR22","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","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,28]],"date-time":"2019-03-28T22:09:34Z","timestamp":1553810974000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}