{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T03:06:42Z","timestamp":1725505602482},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540787907"},{"type":"electronic","value":"9783540787914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78791-4_16","type":"book-chapter","created":{"date-parts":[[2008,4,1]],"date-time":"2008-04-01T19:13:15Z","timestamp":1207077195000},"page":"229-244","source":"Crossref","is-referenced-by-count":4,"title":["Java Bytecode Verification for @NonNull Types"],"prefix":"10.1007","author":[{"given":"Chris","family":"Male","sequence":"first","affiliation":[]},{"given":"David J.","family":"Pearce","sequence":"additional","affiliation":[]},{"given":"Alex","family":"Potanin","sequence":"additional","affiliation":[]},{"given":"Constantine","family":"Dymnikov","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2\u20133","key":"16_CR1","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0167-6423(99)00007-6","volume":"35","author":"A. Aiken","year":"1999","unstructured":"Aiken, A.: Introduction to set constraint-based program analysis. Science of Computer Programming\u00a035(2\u20133), 79\u2013111 (1999)","journal-title":"Science of Computer Programming"},{"key":"16_CR2","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/1167473.1167479","volume-title":"OOPSLA","author":"C. Andreae","year":"2006","unstructured":"Andreae, C., Noble, J., Markstrum, S., Millstein, T.: A framework for implementing pluggable type systems. In: OOPSLA, pp. 57\u201374. ACM Press, New York (2006)"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","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.R.: Non-null references by default in Java: Alleviating the nullity annotation burden. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 227\u2013247. Springer, Heidelberg (2007)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/978-3-540-30579-8_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B.-Y.E. Chang","year":"2005","unstructured":"Chang, B.-Y.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 147\u2013163. Springer, Heidelberg (2005)"},{"key":"16_CR5","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/1065010.1065022","volume-title":"PLDI","author":"B. Chin","year":"2005","unstructured":"Chin, B., Markstrum, S., Millstein, T.: Semantic type qualifiers. In: PLDI, pp. 85\u201395. ACM Press, New York (2005)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/11693024_18","volume-title":"Programming Languages and Systems","author":"B. Chin","year":"2006","unstructured":"Chin, B., Markstrum, S., Millstein, T., Palsberg, J.: Inference of user-defined type qualifiers and qualifier rules. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol.\u00a03924, pp. 264\u2013278. Springer, Heidelberg (2006)"},{"key":"16_CR7","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1145\/1168054.1168073","volume-title":"PPPJ","author":"M. Cielecki","year":"2006","unstructured":"Cielecki, M., Fulara, J., Jakubczyk, K., Jancewicz, L.: Propagation of JML non-null annotations in Java programs. In: PPPJ, pp. 135\u2013140. ACM Press, New York (2006)"},{"issue":"9","key":"16_CR8","doi-asserted-by":"crossref","first-page":"455","DOI":"10.5381\/jot.2007.6.9.a23","volume":"6","author":"T. Ekman","year":"2007","unstructured":"Ekman, T., Hedin, G.: Pluggable checking and inferencing of non-null types for Java. Journal of Object Technology\u00a06(9), 455\u2013475 (2007)","journal-title":"Journal of Object Technology"},{"key":"16_CR9","unstructured":"Ernst, M.: Annotations on Java types. Java Specification Request (JSR) 308 (2007)"},{"key":"16_CR10","first-page":"302","volume-title":"OOPSLA","author":"M. F\u00e4hndrich","year":"2003","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA, pp. 302\u2013312. ACM Press, New York (2003)"},{"key":"16_CR11","doi-asserted-by":"crossref","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proc. PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. PLDI, pp. 234\u2013245. ACM Press, New York (2002)"},{"key":"16_CR12","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1145\/301618.301665","volume-title":"Proc. PLDI","author":"J.S. Foster","year":"1999","unstructured":"Foster, J.S., F\u00e4hndrich, M., Aiken, A.: A theory of type qualifiers. In: Proc. PLDI, pp. 192\u2013203. ACM Press, New York (1999)"},{"key":"16_CR13","first-page":"1","volume-title":"Proc. PLDI","author":"J.S. Foster","year":"2002","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. PLDI, pp. 1\u201312. ACM Press, New York (2002)"},{"key":"16_CR14","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1145\/288090.288104","volume-title":"Conference on Computer & Communications Security","author":"A. Goldberg","year":"1998","unstructured":"Goldberg, A.: A Specification of Java Loading and Bytecode Verification. In: Conference on Computer & Communications Security, pp. 49\u201358. ACM Press, New York (1998)"},{"key":"16_CR15","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/1251535.1251537","volume-title":"Proc. PASTE","author":"D. Hovemeyer","year":"2007","unstructured":"Hovemeyer, D., Pugh, W.: Finding more null pointer bugs, but not too many. In: Proc. PASTE, pp. 9\u201314. ACM Press, New York (2007)"},{"key":"16_CR16","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/1108792.1108798","volume-title":"Proc. PASTE","author":"D. Hovemeyer","year":"2005","unstructured":"Hovemeyer, D., Spacco, J., Pugh, W.: Evaluating and tuning a static analysis to find null pointer bugs. In: Proc. PASTE, pp. 13\u201319. ACM Press, New York (2005)"},{"issue":"3\/4","key":"16_CR17","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1025055424017","volume":"30","author":"X. Leroy","year":"2003","unstructured":"Leroy, X.: Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning\u00a030(3\/4), 235\u2013269 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/11688839_5","volume-title":"Compiler Construction","author":"O. Lhot\u00e1k","year":"2006","unstructured":"Lhot\u00e1k, O., Hendren, L.J.: Context-sensitive points-to analysis: Is it worth it? In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol.\u00a03923, pp. 47\u201364. Springer, Heidelberg (2006)"},{"key":"16_CR19","series-title":"The Java Series","volume-title":"The Java Virtual Machine Specification","author":"T. Lindholm","year":"1999","unstructured":"Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. The Java Series. Addison Wesley Longman, Inc., Amsterdam (1999)","edition":"2"},{"key":"16_CR20","unstructured":"Male, C., Pearce, D.J., Potanin, A., Dymnikov, C.: Java bytecode verification for @NonNull types. Technical report, Victoria University of Wellington (2007)"},{"key":"16_CR21","first-page":"146","volume-title":"Proc. OOPSLA","author":"J. Palsberg","year":"1991","unstructured":"Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. In: Proc. OOPSLA, pp. 146\u2013161. ACM Press, New York (1991)"},{"issue":"4","key":"16_CR22","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1023\/B:SQJO.0000039791.93071.a2","volume":"12","author":"D.J. Pearce","year":"2004","unstructured":"Pearce, D.J., Kelly, P.H.J., Hankin, C.: Online cycle detection and difference propagation: Applications to pointer analysis. Software Quality Journal\u00a012(4), 309\u2013335 (2004)","journal-title":"Software Quality Journal"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Pearce, D.J., Kelly, P.H.J., Hankin, C.: Efficient field-sensitive pointer analysis for C. Transactions on Programming Languages and Systems\u00a030(1) (2008)","DOI":"10.1145\/1290520.1290524"},{"key":"16_CR24","first-page":"324","volume-title":"Proc. OOPSLA","author":"J. Plevyak","year":"1994","unstructured":"Plevyak, J., Chien, A.A.: Precise concrete type inference for object-oriented languages. In: Proc. OOPSLA, pp. 324\u2013340. ACM Press, New York (1994)"},{"key":"16_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-45306-7_23","volume-title":"Compiler Construction","author":"P. Pominville","year":"2001","unstructured":"Pominville, P., Qian, F., Vall\u00e9e-Rai, R., Hendren, L., Verbrugge, C.: A framework for optimizing Java using attributes. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol.\u00a02027, pp. 334\u2013554. Springer, Heidelberg (2001)"},{"key":"16_CR26","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/504282.504286","volume-title":"Proc. OOPSLA","author":"A. Rountev","year":"2001","unstructured":"Rountev, A., Milanova, A., Ryder, B.G.: Points-to analysis for Java using annotated constraints. In: Proc. OOPSLA, pp. 43\u201355. ACM Press, New York (2001)"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, pp. 366\u2013381. Springer, Heidelberg (2000)"},{"key":"16_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/3-540-45337-7_6","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"T. Wang","year":"2001","unstructured":"Wang, T., Smith, S.F.: Precise constraint-based type inference for Java. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, pp. 99\u2013117. Springer, Heidelberg (2001)"},{"key":"16_CR29","series-title":"Lecture Notes in Computer Science","volume-title":"LOPSTR 2007","author":"Y. Zhang","year":"2007","unstructured":"Zhang, Y., Nielson, F.: A scalable inclusion constraint solver using unification. In: King, A. (ed.) LOPSTR 2007. LNCS, vol.\u00a04915, Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Compiler Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78791-4_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,17]],"date-time":"2023-05-17T07:32:36Z","timestamp":1684308756000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78791-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787907","9783540787914"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78791-4_16","relation":{},"subject":[]}}