{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:05:06Z","timestamp":1767927906477,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540786627","type":"print"},{"value":"9783540786634","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78663-4_4","type":"book-chapter","created":{"date-parts":[[2008,3,8]],"date-time":"2008-03-08T06:00:01Z","timestamp":1204956001000},"page":"23-40","source":"Crossref","is-referenced-by-count":5,"title":["Combining a Verification Condition Generator for a Bytecode Language with Static Analyses"],"prefix":"10.1007","author":[{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jorge Luis","family":"Sacchini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/11799573_14","volume-title":"Logic Programming","author":"E. Albert","year":"2006","unstructured":"Albert, E., Arenas-S\u00e1nchez, P., Puebla, G., Hermenegildo, M.V.: Reduced certificates for abstraction-carrying code. In: Etalle, S., Truszczy\u0144ski, M. (eds.) ICLP 2006. LNCS, vol.\u00a04079, pp. 163\u2013178. Springer, Heidelberg (2006)"},{"key":"4_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-540-32275-7_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E. Albert","year":"2005","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 380\u2013397. Springer, Heidelberg (2005)"},{"issue":"3","key":"4_CR3","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T.P., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci.\u00a0364(3), 273\u2013291 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-71316-6_19","volume-title":"Programming Languages and Systems","author":"F. Besson","year":"2007","unstructured":"Besson, F., Jensen, T.P., Turpin, T.: Small witnesses for abstract interpretation-based proofs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 268\u2013283. Springer, Heidelberg (2007)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/11921240_20","volume-title":"Theoretical Aspects of Computing - ICTAC 2006","author":"A. Chaieb","year":"2006","unstructured":"Chaieb, A.: Proof-producing program analysis. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol.\u00a04281, pp. 287\u2013301. Springer, Heidelberg (2006)"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73589-2_12","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"P. Chalin","year":"2007","unstructured":"Chalin, P., James, P.: Non-null references by default in java: Alleviating the nullity annotation burden. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, Springer, Heidelberg (2007)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"key":"4_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer-Verlag New York, Inc., Secaucus, NJ, USA (1999)"},{"key":"4_CR10","unstructured":"Pichardie, D.: Bicolano \u2013 Byte Code Language in Coq (2006), \n                    \n                      http:\/\/mobius.inia.fr\/bicolano"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-3-540-40018-9_16","volume-title":"Programming Languages and Systems","author":"S. Seo","year":"2003","unstructured":"Seo, S., Yang, H., Yi, K.: Automatic construction of hoare proofs from abstract interpretation results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol.\u00a02895, pp. 230\u2013245. Springer, Heidelberg (2003)"},{"issue":"1","key":"4_CR12","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2005.02.040","volume":"141","author":"M. Wildmoser","year":"2005","unstructured":"Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. Electr. Notes Theor. Comput. Sci.\u00a0141(1), 19\u201334 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-3-540-30142-4_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T.: Certifying machine code safety: Shallow versus deep embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 305\u2013320. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78663-4_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:17:52Z","timestamp":1619522272000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78663-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540786627","9783540786634"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78663-4_4","relation":{},"subject":[]}}