{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:36:23Z","timestamp":1767137783731,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319051185","type":"print"},{"value":"9783319051192","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-05119-2_16","type":"book-chapter","created":{"date-parts":[[2014,3,7]],"date-time":"2014-03-07T04:36:28Z","timestamp":1394166988000},"page":"273-293","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Certificates and Separation Logic"],"prefix":"10.1007","author":[{"given":"Martin","family":"Nordio","sequence":"first","affiliation":[]},{"given":"Cristiano","family":"Calcagno","sequence":"additional","affiliation":[]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2014,3,8]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Bannwart, F.Y., M\u00fcller, P.: A program logic for bytecode. In: Spoto, F. (ed.) BYTECODE. ENTCS, vol. 141(1), pp. 255\u2013273. Elsevier, Amsterdam (2005)","DOI":"10.1016\/j.entcs.2005.02.026"},{"key":"16_CR2","series-title":"LNCS","first-page":"1","volume-title":"FMCO 2007","author":"G Barthe","year":"2008","unstructured":"Barthe, G., Cr\u00e9gut, P., Gr\u00e9goire, B., Jensen, T., Pichardie, D.: The MOBIUS proof carrying code infrastructure. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 1\u201324. Springer, Heidelberg (2008)"},{"key":"16_CR3","series-title":"LNCS(LNAI)","first-page":"83","volume-title":"IJCAR 2008","author":"G Barthe","year":"2008","unstructured":"Barthe, G., Gr\u00e9goire, B., Pavlova, M.I.: Preservation of proof obligations from Java to the Java virtual machine. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS(LNAI), vol. 5195, pp. 83\u201399. Springer, Heidelberg (2008)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Third International Workshop on Formal Aspects in Security and Trust, Newcastle, UK, pp. 112\u2013126 (2005)","DOI":"10.1007\/11679219_9"},{"key":"16_CR5","series-title":"LNCS","first-page":"364","volume-title":"APLAS 2005","author":"N Benton","year":"2005","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Chin, W., David, C., Nguyen, H., Qin, S.: Enhancing modular OO verification with separation logic. In: POPL \u201908, pp. 87\u201399. ACM (2008)","DOI":"10.1145\/1328897.1328452"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA \u201902, vol. 37. ACM (2002)","DOI":"10.1145\/582419.582447"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. In: OOPSLA \u201908, pp. 213\u2013226 (2008)","DOI":"10.1145\/1449955.1449782"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Dong, Y., Wang, S., Zhang, L., Yang, P.: Modular certification of low-level intermediate representation programs. In: ICSAC, pp. 563\u2013570. IEEE Computer Society (2009)","DOI":"10.1109\/COMPSAC.2009.81"},{"key":"16_CR10","series-title":"LNCS","first-page":"237","volume-title":"TGC 2010","author":"C Kunz","year":"2010","unstructured":"Kunz, C.: Certificate translation for the verification of concurrent programs. In: Wirsing, M., Hofmann, M., Rauschmayer, A. (eds.) TGC 2010. LNCS, vol. 6084, pp. 237\u2013252. Springer, Heidelberg (2010)"},{"key":"16_CR11","series-title":"LNICST","first-page":"42","volume-title":"ISDF 2009","author":"Z Zhou","year":"2010","unstructured":"Zhou, Z., Chindaro, S., Deravi, F.: Face recognition using balanced pairwise classifier training. In: Weerasinghe, D. (ed.) ISDF 2009. LNICST, vol. 41, pp. 42\u201349. Springer, Heidelberg (2010)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: SAVCBS \u201907, pp. 39\u201346 (2007)","DOI":"10.1145\/1292316.1292321"},{"key":"16_CR13","unstructured":"Necula, G.: Compiling with proofs. Ph.D. thesis, School of Computer Science, Carnegie Mellon University (1998)"},{"key":"16_CR14","unstructured":"Nordio, M.: Proofs and proof transformations for object-oriented programs. Ph.D. thesis, ETH Zurich (2009)"},{"key":"16_CR15","series-title":"LNBIP","first-page":"195","volume-title":"TOOLS EUROPE 2009","author":"M Nordio","year":"2009","unstructured":"Nordio, M., Calcagno, C., M\u00fcller, P., Meyer, B.: A sound and complete program logic for Eiffel. In: Oriol, M., Meyer, B. (eds.) TOOLS EUROPE 2009. LNBIP, vol. 33, pp. 195\u2013214. Springer, Heidelberg (2009)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Nordio, M., M\u00fcller, P., Meyer, B.: Formalizing proof-transforming compilation of Eiffel programs. Technical report 587, ETH Zurich (2008)","DOI":"10.1007\/978-3-540-69824-1_18"},{"key":"16_CR17","series-title":"LNBIP","first-page":"316","volume-title":"TOOLS-EUROPE 2008","author":"M Nordio","year":"2008","unstructured":"Nordio, M., M\u00fcller, P., Meyer, B.: Proof-transforming compilation of Eiffel programs. In: Paige, R.F., Meyer, B. (eds.) TOOLS-EUROPE 2008. LNBIP, vol. 11, pp. 316\u2013335. Springer, Heidelberg (2008)"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci. 375, 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL \u201904, pp. 268\u2013280. ACM (2004)","DOI":"10.1145\/982962.964024"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL \u201908, pp. 75\u201386. ACM (2008)","DOI":"10.1145\/1328897.1328451"},{"key":"16_CR21","series-title":"LNCS","first-page":"151","volume-title":"TACAS 1998","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"issue":"1\u20132","key":"16_CR22","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. J. Logic Algebr. Program. 77(1\u20132), 131\u2013154 (2008)","journal-title":"J. Logic Algebr. Program."},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Stata, R., Abadi, M.: A type system for Java bytecode subroutines. In: POPL \u201998, pp. 149\u2013160. ACM (1998)","DOI":"10.1145\/268946.268959"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-05119-2_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,22]],"date-time":"2023-12-22T00:12:07Z","timestamp":1703203927000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-05119-2_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319051185","9783319051192"],"references-count":23,"aliases":["10.1007\/978-3-319-14128-2_16"],"URL":"https:\/\/doi.org\/10.1007\/978-3-319-05119-2_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"8 March 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}