{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:56:06Z","timestamp":1725551766999},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297352"},{"type":"electronic","value":"9783540322474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11575467_18","type":"book-chapter","created":{"date-parts":[[2005,11,11]],"date-time":"2005-11-11T13:58:51Z","timestamp":1131717531000},"page":"264-280","source":"Crossref","is-referenced-by-count":2,"title":["A Path Sensitive Type System for Resource Usage Verification of C Like Languages"],"prefix":"10.1007","author":[{"given":"Hyun-Goo","family":"Kang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Youil","family":"Kim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taisook","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hwansoo","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Aiken, A., F\u00e4hndrich, M., Levien, R.: Better Static Memory Management: Improving Region-Based Analysis of Higher-Order Languages. In: PLDI (1995)","key":"18_CR1","DOI":"10.1145\/207110.207137"},{"doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.: The SLAM Project: Debugging System Software via Static Analysis. In: POPL (2002)","key":"18_CR2","DOI":"10.1145\/503272.503274"},{"doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular Verification of Software Components in C. In: ICSE (2003)","key":"18_CR3","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A Tool for Checking ANSI-C Programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-Sensitive Program Verification in Polynomial Time. In: PLDI (2002)","key":"18_CR5","DOI":"10.1145\/512529.512538"},{"doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing High-Level Protocols in Low-Level Software. In: PLDI (2001)","key":"18_CR6","DOI":"10.1145\/378795.378811"},{"doi-asserted-by":"crossref","unstructured":"Dor, N., Adams, S., Das, M., Yang, Z.: Software Validation via Scalable Path-Sensitive Value Flow Analysis. In: ISSTA (2004)","key":"18_CR7","DOI":"10.1145\/1007512.1007515"},{"doi-asserted-by":"crossref","unstructured":"Engler, D., Chelf, B., Chou, A., Hallem, S.: Checking System Rules Using System-Specific, Programmer-Written Compiler Extensions. In: OSDI (2000)","key":"18_CR8","DOI":"10.21236\/ADA419626"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"M. F\u00e4hndrich","year":"2004","unstructured":"F\u00e4hndrich, M., DeLine, R.: Typestates for Objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 465\u2013490. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Field, J., Goyal, D., Ramalingam, G., Yahav, E.: Typestate Verification: Abstraction Techniques and Complexity Result. In: SAS (2003)","key":"18_CR10","DOI":"10.1007\/3-540-44898-5_25"},{"doi-asserted-by":"crossref","unstructured":"Flanagan, C., Abadi, M.: Object Types Against Races. In: CONCUR (1999)","key":"18_CR11","DOI":"10.1007\/3-540-48320-9_21"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-49099-X_7","volume-title":"Programming Languages and Systems","author":"C. Flanagan","year":"1999","unstructured":"Flanagan, C., Abadi, M.: Types for Safe Locking. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol.\u00a01576, p. 91. Springer, Heidelberg (1999)"},{"doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., State, R.: Extended Static Checking for Java. In: PLDI (2002)","key":"18_CR13","DOI":"10.1145\/512529.512558"},{"doi-asserted-by":"crossref","unstructured":"Foster, J., Terauhi, T., Aiken, A.: Flow-Sensitive Type Qualifiers. In: PLDI (2002)","key":"18_CR14","DOI":"10.21236\/ADA603588"},{"issue":"6","key":"18_CR15","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1145\/330643.330646","volume":"21","author":"S. Freund","year":"1999","unstructured":"Freund, S., Mitchell, J.: The Type System for Object Initialization in the Java Bytecode Language. TOPLAS\u00a021(6), 1196\u20131250 (1999)","journal-title":"TOPLAS"},{"doi-asserted-by":"crossref","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: 10th International SPIN Workshop (2003)","key":"18_CR16","DOI":"10.1007\/3-540-44829-2_17"},{"doi-asserted-by":"crossref","unstructured":"Igarashi, A., Kobayashi, N.: Resource Usage Analysis. In: POPL (2002)","key":"18_CR17","DOI":"10.1145\/503272.503303"},{"doi-asserted-by":"crossref","unstructured":"Kang, H.-G., Kim, Y., Han, T., Han, H.: A Path Sensitive Type System for Resource Usage Verification of C like Languages (2005), http:\/\/pllab.kaist.ac.kr\/~hgkang\/pruv-tm.pdf","key":"18_CR18","DOI":"10.1007\/11575467_18"},{"doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Quasi-Linear Types. In: POPL (1999)","key":"18_CR19","DOI":"10.1145\/292540.292546"},{"doi-asserted-by":"crossref","unstructured":"Kobayashi, N.: Time Regions and Effects for Resource Usage Analysis. In: TLDI (2003)","key":"18_CR20","DOI":"10.1145\/604174.604182"},{"issue":"1","key":"18_CR21","doi-asserted-by":"publisher","first-page":"741","DOI":"10.1016\/S0304-3975(02)00330-4","volume":"290","author":"C. Laneve","year":"2003","unstructured":"Laneve, C.: A Type System for JVM Threads. Theoretical Computer Science\u00a0290(1), 741\u2013778 (2003)","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Lee, O., Yang, H., Yi, K.: Inserting Safe Memory Reuse Commands into ML-like Programs. In: SAS (2003)","key":"18_CR22","DOI":"10.1007\/3-540-44898-5_10"},{"doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)","key":"18_CR23","DOI":"10.1145\/378239.379017"},{"doi-asserted-by":"crossref","unstructured":"Shapiro, M., Horwitz, S.: The Effects of the Precision of Pointer Analysis. In: SAS (1997)","key":"18_CR24","DOI":"10.1007\/BFb0032731"},{"unstructured":"Smith, G.: Polymorphic Type Inference for Languages with Overloading and Subtyping. PhD thesis, Cornell University (August 1991)","key":"18_CR25"},{"unstructured":"SPEC. SPEC Benchmarks Suite, http:\/\/www.spec.org\/","key":"18_CR26"},{"issue":"1","key":"18_CR27","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R. Strom","year":"1986","unstructured":"Strom, R., Yemini, S.: Typestate: A Programming Language Concept for Enhancing Software Reliability. IEEE Transactions on Software Engineering\u00a012(1), 157\u2013171 (1986)","journal-title":"IEEE Transactions on Software Engineering"},{"unstructured":"Tan, G., Ou, X., Walker, D.: Enforcing Resource Usage Protocols via Scoped Methods. In: FOOL (2003)","key":"18_CR28"},{"issue":"4","key":"18_CR29","doi-asserted-by":"publisher","first-page":"734","DOI":"10.1145\/291891.291894","volume":"20","author":"M. Tofte","year":"1998","unstructured":"Tofte, M., Birkedal, L.: A Region Inference Algorithm. TOPLAS\u00a020(4), 734\u2013767 (1998)","journal-title":"TOPLAS"},{"issue":"4","key":"18_CR30","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1145\/363911.363923","volume":"22","author":"D. Walker","year":"2000","unstructured":"Walker, D., Crary, K., Morriset, G.: Typed Memory Management via Static Capabilities. TOPLAS\u00a022(4), 701\u2013771 (2000)","journal-title":"TOPLAS"},{"doi-asserted-by":"crossref","unstructured":"Xie, Y., Aiken, A.: Scalable Error Detection using Boolean Satisfiability. In: POPL, pp. 351\u2013363 (2005)","key":"18_CR31","DOI":"10.1145\/1040305.1040334"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11575467_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:57:27Z","timestamp":1605643047000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11575467_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297352","9783540322474"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/11575467_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}