{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:46:37Z","timestamp":1777347997324,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642228629","type":"print"},{"value":"9783642228636","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-22863-6_6","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T09:47:55Z","timestamp":1312796875000},"page":"39-54","source":"Crossref","is-referenced-by-count":16,"title":["Relational Decomposition"],"prefix":"10.1007","author":[{"given":"Lennart","family":"Beringer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Morrisett and Jones [30], pp. 91\u2013102","DOI":"10.1145\/1111037.1111046"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-11957-6_4","volume-title":"Programming Languages and Systems","author":"T. Amtoft","year":"2010","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E.: Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 43\u201363. Springer, Heidelberg (2010)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-68237-0_17","volume-title":"FM 2008: Formal Methods","author":"T. Amtoft","year":"2008","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E., Robby, Hoag, J., Greve, D.A.: Specification and Checking of Software Contracts for Conditional Information Flow. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 229\u2013245. Springer, Heidelberg (2008)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"A.W. Appel","year":"2008","unstructured":"Appel, A.W.: Foundational high-level static analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, Springer, Heidelberg (2008)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"A.W. Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 1\u201317. Springer, Heidelberg (2011)"},{"issue":"3","key":"6_CR6","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1016\/j.tcs.2007.09.003","volume":"389","author":"D. Aspinall","year":"2007","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resources. Theoretical Computer Science\u00a0389(3), 411\u2013445 (2007)","journal-title":"Theoretical Computer Science"},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.: Stack-based access control for secure information flow. Journal of Functional Programming\u00a015, 131\u2013177 (2005)","journal-title":"Journal of Functional Programming"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1145\/1255329.1255340","volume-title":"Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security (PLAS 2007)","author":"A. Banerjee","year":"2007","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Towards a logical account of declassification. In: Hicks, M.W. (ed.) Proceedings of the 2007 Workshop on Programming Languages and Analysis for Security (PLAS 2007), pp. 61\u201366. ACM Press, New York (2007)"},{"key":"6_CR9","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J. Barnes","year":"2006","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Reading (2006)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs (2011), http:\/\/software.imdea.org\/~ckunz\/rellog\/long-rellog.pdf","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"6_CR11","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":"6_CR12","first-page":"103","volume-title":"Types in Language Design and Implementation","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Rezk, T.: Non-interference for a JVM-like language. In: F\u00e4hndrich, M. (ed.) Types in Language Design and Implementation, pp. 103\u2013112. ACM Press, New York (2005)"},{"key":"6_CR13","first-page":"14","volume-title":"Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL 2004)","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.) Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL 2004), pp. 14\u201325. ACM Press, New York (2004)"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Beringer, L.: Relational decomposition \u2013 Isabelle\/HOL sources (2011), www.cs.princeton.edu\/~eberinge\/RelDecompITP2011.tar.gz","DOI":"10.1007\/978-3-642-22863-6_6"},{"key":"6_CR15","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1109\/CSF.2007.30","volume-title":"IEEE Computer Security Foundations Symposium","author":"L. Beringer","year":"2007","unstructured":"Beringer, L., Hofmann, M.: Secure information flow and program logics. In: IEEE Computer Security Foundations Symposium, pp. 233\u2013248. IEEE Press, Los Alamitos (2007)"},{"key":"6_CR16","first-page":"260","volume-title":"Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005)","author":"L. Birkedal","year":"2005","unstructured":"Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: Proceedings of the 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pp. 260\u2013269. IEEE Press, Los Alamitos (2005)"},{"issue":"3","key":"6_CR17","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic\u00a022(3), 269\u2013285 (1957)","journal-title":"Journal of Symbolic Logic"},{"key":"6_CR18","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Gorrieri, R. (ed.) Workshop on Issues in the Theory of Security. IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS (2003)"},{"issue":"1-3","key":"6_CR19","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/S0304-3975(03)00200-7","volume":"309","author":"P. Gardiner","year":"2003","unstructured":"Gardiner, P.: Power simulation and its relation to traces and failures refinement. Theoretical Computer Science\u00a0309(1-3), 157\u2013176 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"6_CR20","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. Electronic Notes in Theoretical Computer Science\u00a0132(1), 53\u201371 (2005)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"6_CR21","volume-title":"Proceedings of the 37th ACM Symposium on Principles of Programming Languages (POPL 2010)","year":"2010","unstructured":"Hermenegildo, M.V., Palsberg, J. (eds.): Proceedings of the 37th ACM Symposium on Principles of Programming Languages (POPL 2010). ACM Press, New York (2010)"},{"issue":"2","key":"6_CR22","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/0020-0190(87)90106-2","volume":"24","author":"C.A.R. Hoare","year":"1987","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification. Information Processing Letters\u00a024(2), 127\u2013132 (1987)","journal-title":"Information Processing Letters"},{"issue":"2","key":"6_CR23","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","volume":"25","author":"C.A.R. Hoare","year":"1987","unstructured":"Hoare, C.A.R., He, J., Sanders, J.W.: Prespecification in data refinement. Information Processing Letters\u00a025(2), 71\u201376 (1987)","journal-title":"Information Processing Letters"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: Morrisett, Jones (eds.) [30], pp. 79\u201390","DOI":"10.1145\/1111037.1111045"},{"key":"6_CR25","volume-title":"Systematic Software Development Using VDM","author":"C.B. Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall International, Englewood Cliffs (1990)","edition":"2"},{"key":"6_CR26","unstructured":"Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1998)"},{"key":"6_CR27","first-page":"364","volume-title":"Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL 2005)","author":"S. Lerner","year":"2005","unstructured":"Lerner, S., Millstein, T.D., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM Symposium on Principles of Programming Languages (POPL 2005), pp. 364\u2013377. ACM Press, New York (2005)"},{"issue":"4","key":"6_CR28","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"6_CR29","doi-asserted-by":"crossref","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Automatic numeric abstractions for heap-manipulating programs. In: Hermenegildo, Palsberg [21], pp. 211\u2013222","DOI":"10.1145\/1706299.1706326"},{"key":"6_CR30","volume-title":"Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (POPL 2006)","year":"2006","unstructured":"Morrisett, J.G., Jones, S.L.P. (eds.): Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (POPL 2006). ACM Press, New York (2006)"},{"key":"6_CR31","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":"6_CR32","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. SIGPLAN Not.\u00a035(5), 83\u201394 (2000)","journal-title":"SIGPLAN Not."},{"key":"6_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 103\u2013119. Springer, Heidelberg (2002)"},{"issue":"1-2","key":"6_CR34","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/j.jlap.2008.05.007","volume":"77","author":"A. Saabas","year":"2008","unstructured":"Saabas, A., Uustalu, T.: Program and proof optimizations with type systems. Journal of Logic and Algebraic Programming\u00a077(1-2), 131\u2013154 (2008)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"6_CR35","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communication\u00a021, 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communication"},{"key":"6_CR36","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Lerner, S.: Generating compiler optimizations from proofs. In: Hermenegildo, Palsberg [21], pp. 389\u2013402","DOI":"10.1145\/1706299.1706345"},{"key":"6_CR37","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":"3","key":"6_CR38","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security\u00a04(3), 167\u2013187 (1996)","journal-title":"Journal of Computer Security"},{"key":"6_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-03237-0_23","volume-title":"Static Analysis","author":"A. Voronkov","year":"2009","unstructured":"Voronkov, A., Narasamdya, I.: Inter-program properties. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 343\u2013359. Springer, Heidelberg (2009)"},{"issue":"1-3","key":"6_CR40","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"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22863-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,8]],"date-time":"2023-06-08T16:23:29Z","timestamp":1686241409000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}