{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:33:48Z","timestamp":1761597228105,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540205364"},{"type":"electronic","value":"9783540400189"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/978-3-540-40018-9_16","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T23:03:20Z","timestamp":1283727800000},"page":"230-245","source":"Crossref","is-referenced-by-count":16,"title":["Automatic Construction of Hoare Proofs from Abstract Interpretation Results"],"prefix":"10.1007","author":[{"given":"Sunae","family":"Seo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kwangkeun","family":"Yi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Appel, W.A.: Foundational proof-carrying code. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, June 2001, pp. 247\u2013258 (2001)","DOI":"10.1109\/LICS.2001.932501"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Appel, W.A., Felty, A.P.: A semantic model of types and machine instructions for proof-carrying code. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2000, pp. 243\u2013253 (2000)","DOI":"10.1145\/325694.325727"},{"key":"16_CR3","series-title":"NATO ASI Series F","volume-title":"Calculational System Design","author":"P. Cousot","year":"1999","unstructured":"Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational System Design. NATO ASI Series F, IOS Press, Amsterdam (1999)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: ACM Symposium on Artificial Intelligence and Programming Languages, ACM SIGPLAN Notices, Rochester, NY, August 1977, vol.\u00a012, pp. 1\u201312 (1977)","DOI":"10.1145\/872734.806926"},{"key":"16_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/567752.567778","volume-title":"Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Hamid, N., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A syntactic approach to foundational proof-carrying code. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, June 2002, pp. 89\u2013100 (2002)","DOI":"10.1109\/LICS.2002.1029819"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Heintze, N., Jaffar, J., Voicu, R.: A framework for combining analysis and verification. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Boston, MA, USA, January 2000, pp. 26\u201339 (2000)","DOI":"10.1145\/325694.325700"},{"issue":"10","key":"16_CR9","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. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1998, pp. 85\u201397 (1998)","DOI":"10.21236\/ADA358572"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 1997, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"16_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-68671-1_5","volume-title":"Mobile Agents and Security","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: Safe, untrusted agents using proof-carrying code. In: Vigna, G. (ed.) Mobile Agents and Security. LNCS, vol.\u00a01419, pp. 61\u201391. Springer, Heidelberg (1998)"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, January 2001, pp. 142\u2013154 (2001)","DOI":"10.1145\/373243.360216"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/3-540-36532-X_18","volume-title":"Software Security \u2013 Theories and Systems","author":"G.C. Necula","year":"2003","unstructured":"Necula, G.C., Schneck, R.: Proof-carrying code with untrusted proof rules. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 283\u2013298. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40018-9_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,25]],"date-time":"2025-02-25T15:51:59Z","timestamp":1740498719000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40018-9_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205364","9783540400189"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40018-9_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}