{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:09:46Z","timestamp":1763467786485,"version":"3.41.0"},"reference-count":93,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2006,11,1]],"date-time":"2006-11-01T00:00:00Z","timestamp":1162339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2006,11]]},"abstract":"<jats:p>\n            We describe flow-insensitive type qualifiers, a lightweight, practical mechanism for specifying and checking properties not captured by traditional type systems. We present a framework for adding new, user-specified type qualifiers to programming languages with static type systems, such as C and Java. In our system, programmers add a few type qualifier annotations to their program, and automatic type qualifier inference determines the remaining qualifiers and checks the annotations for consistency. We describe a tool CQual for adding type qualifiers to the C programming language. Our tool CQual includes a visualization component for displaying browsable inference results to the programmer. Finally, we present several experiments using our tool, including inferring\n            <jats:italic>const<\/jats:italic>\n            qualifiers, finding security vulnerabilities in several popular C programs, and checking initialization data usage in the Linux kernel. Our results suggest that inference and visualization make type qualifiers lightweight, that type qualifier inference scales to large programs, and that type qualifiers are applicable to a wide variety of problems.\n          <\/jats:p>","DOI":"10.1145\/1186632.1186635","type":"journal-article","created":{"date-parts":[[2007,1,16]],"date-time":"2007-01-16T19:38:29Z","timestamp":1168976309000},"page":"1035-1087","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":51,"title":["Flow-insensitive type qualifiers"],"prefix":"10.1145","volume":"28","author":[{"given":"Jeffrey S.","family":"Foster","sequence":"first","affiliation":[{"name":"University of Maryland, College Park, MD"}]},{"given":"Robert","family":"Johnson","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, Stony Brook, NY"}]},{"given":"John","family":"Kodumal","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, San Francisco, CA"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA"}]}],"member":"320","published-online":{"date-parts":[[2006,11]]},"reference":[{"volume-title":"Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language","author":"Abadi M.","unstructured":"Abadi , M. , Banerjee , A. , Heintze , N. , and Riecke , J. G . 1999. A core calculus of dependency . In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language ( San Antonio, TX). ACM, New York, 147--160.]] 10.1145\/292540.292555 Abadi, M., Banerjee, A., Heintze, N., and Riecke, J. G. 1999. A core calculus of dependency. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language (San Antonio, TX). ACM, New York, 147--160.]] 10.1145\/292540.292555","key":"e_1_2_1_1_1"},{"volume-title":"Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Aiken A.","unstructured":"Aiken , A. , Foster , J. S. , Kodumal , J. , and Terauchi , T . 2003. Checking and inferring local non-aliasing . In Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation ( San Diego, CA). ACM, New York, 129--140.]] 10.1145\/781131.781146 Aiken, A., Foster, J. S., Kodumal, J., and Terauchi, T. 2003. Checking and inferring local non-aliasing. In Proceedings of the 2003 ACM SIGPLAN Conference on Programming Language Design and Implementation (San Diego, CA). ACM, New York, 129--140.]] 10.1145\/781131.781146","key":"e_1_2_1_2_1"},{"unstructured":"Ansi 1989. Rationale for American National Standard for Information Systems---Programming Language---C. ANSI. Associated with ANSI standard X3.159-1989.]]  Ansi 1989. Rationale for American National Standard for Information Systems---Programming Language---C. ANSI. Associated with ANSI standard X3.159-1989.]]","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","first-page":"1999","article-title":"Programming languages---C","volume":"9899","author":"Ansi","year":"1999","unstructured":"Ansi 1999 . Programming languages---C . ANSI\/ISO\/IEC 9899 : 1999 .]] Ansi 1999. Programming languages---C. ANSI\/ISO\/IEC 9899:1999.]]","journal-title":"ANSI\/ISO\/IEC"},{"unstructured":"Bailleux C. 2000. More security problems in bftpd-1.0.12. BugTraq Mailing List. http:\/\/www.securityfocus.com\/archive\/1\/149977.]]  Bailleux C. 2000. More security problems in bftpd-1.0.12. BugTraq Mailing List. http:\/\/www.securityfocus.com\/archive\/1\/149977.]]","key":"e_1_2_1_5_1"},{"volume-title":"Proceedings of the 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Ball T.","unstructured":"Ball , T. , Naik , M. , and Rajamani , S. K . 2003. From symptom to cause: Localizing errors in counterexample traces . In Proceedings of the 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( New Orleans, LA), ACM, New York, 97--105.]] 10.1145\/604131.604140 Ball, T., Naik, M., and Rajamani, S. K. 2003. From symptom to cause: Localizing errors in counterexample traces. In Proceedings of the 30th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (New Orleans, LA), ACM, New York, 97--105.]] 10.1145\/604131.604140","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 8th International SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science","volume":"2057","author":"Ball T.","unstructured":"Ball , T. and Rajamani , S. K . 2001. Automatically validating temporal safety properties of interfaces . In Proceedings of the 8th International SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science , vol. 2057 , Springer-Verlag, New York, 103--122.]] Ball, T. and Rajamani, S. K. 2001. Automatically validating temporal safety properties of interfaces. In Proceedings of the 8th International SPIN Workshop on Model Checking of Software. Lecture Notes in Computer Science, vol. 2057, Springer-Verlag, New York, 103--122.]]"},{"volume-title":"Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Ball T.","unstructured":"Ball , T. and Rajamani , S. K . 2002. The SLAM project: Debugging system software via static analysis . In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( Portland, OR). ACM, New York, 1--3.]] 10.1145\/503272.503274 Ball, T. and Rajamani, S. K. 2002. The SLAM project: Debugging system software via static analysis. In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, OR). ACM, New York, 1--3.]] 10.1145\/503272.503274","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","first-page":"131","article-title":"Checking for race conditions in file accesses","volume":"2","author":"Bishop M.","year":"1996","unstructured":"Bishop , M. and Dilger , M. 1996 . Checking for race conditions in file accesses . Comput. Syst. 2 , 2, 131 -- 152 .]] Bishop, M. and Dilger, M. 1996. Checking for race conditions in file accesses. Comput. Syst. 2, 2, 131--152.]]","journal-title":"Comput. Syst."},{"volume-title":"Proceedings of the 12th Usenix Security Symposium","author":"Broadwell P.","unstructured":"Broadwell , P. , Harren , M. , and Sastry , N . 2003. Scrash: A system for generating secure crash information . In Proceedings of the 12th Usenix Security Symposium ( Washington, DC).]] Broadwell, P., Harren, M., and Sastry, N. 2003. Scrash: A system for generating secure crash information. In Proceedings of the 12th Usenix Security Symposium (Washington, DC).]]","key":"e_1_2_1_10_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_12_1","volume-title":"\u201cCode Red","author":"Cert CERT","year":"2001","unstructured":"Cert . 2001. CERT Advisory CA-2001-19 \u201cCode Red \u201d worm exploiting buffer overflow In IIS indexing service DLL. http:\/\/www.cert.org\/advisories\/CA- 2001 -19.html.]] Cert. 2001. CERT Advisory CA-2001-19 \u201cCode Red\u201d worm exploiting buffer overflow In IIS indexing service DLL. http:\/\/www.cert.org\/advisories\/CA-2001-19.html.]]"},{"volume-title":"Proceedings of the ACM SIGPLAN\/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering","author":"Chandra S.","unstructured":"Chandra , S. and Reps , T. W . 1999. Physical type checking for C . In Proceedings of the ACM SIGPLAN\/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering ( Toulouse, France). ACM, New York, 66--75.]] 10.1145\/316158.316183 Chandra, S. and Reps, T. W. 1999. Physical type checking for C. In Proceedings of the ACM SIGPLAN\/SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (Toulouse, France). ACM, New York, 66--75.]] 10.1145\/316158.316183","key":"e_1_2_1_13_1"},{"volume-title":"Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Chin B.","unstructured":"Chin , B. , Markstrum , S. , and Millstein , T . 2005. Semantic type qualifiers . In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Chicago, IL). ACM, New York.]] 10.1145\/1065010.1065022 Chin, B., Markstrum, S., and Millstein, T. 2005. Semantic type qualifiers. In Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation (Chicago, IL). ACM, New York.]] 10.1145\/1065010.1065022","key":"e_1_2_1_14_1"},{"volume-title":"Proceedings of the 4th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM","author":"Cousot P.","unstructured":"Cousot , P. and Cousot , R . 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints . In Proceedings of the 4th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM , New York, 238--252.]] 10.1145\/512950.512973 Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, New York, 238--252.]] 10.1145\/512950.512973","key":"e_1_2_1_15_1"},{"volume-title":"Proceedings of the 10th Usenix Security Symposium","author":"Cowan C.","unstructured":"Cowan , C. , Barringer , M. , Beattie , S. , and Kroah-Hartman , G . 2001. FormatGuard: Automatic protection from print format string vulnerabilities . In Proceedings of the 10th Usenix Security Symposium ( Washington, DC).]] Cowan, C., Barringer, M., Beattie, S., and Kroah-Hartman, G. 2001. FormatGuard: Automatic protection from print format string vulnerabilities. In Proceedings of the 10th Usenix Security Symposium (Washington, DC).]]","key":"e_1_2_1_16_1"},{"volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Das M.","unstructured":"Das , M. , Lerner , S. , and Seigle , M . 2002. ESP: Path-sensitive program verification in polynomial time . In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Berlin, Germany). ACM, New York, 57--68.]] 10.1145\/512529.512538 Das, M., Lerner, S., and Seigle, M. 2002. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, Germany). ACM, New York, 57--68.]] 10.1145\/512529.512538","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","volume-title":"Eighth International Symposium","volume":"2126","author":"Das M.","unstructured":"Das , M. , Liblit , B. , F\u00e4hndrich , M. , and Rehof , J . 2001. Estimating the impact of scalable pointer analysis on optimization. In Static Analysis , Eighth International Symposium ( Paris, France), P. Cousot, Ed. Lecture Notes in Computer Science , vol. 2126 . Springer-Verlag, New York.]] Das, M., Liblit, B., F\u00e4hndrich, M., and Rehof, J. 2001. Estimating the impact of scalable pointer analysis on optimization. In Static Analysis, Eighth International Symposium (Paris, France), P. Cousot, Ed. Lecture Notes in Computer Science, vol. 2126. Springer-Verlag, New York.]]"},{"unstructured":"Davey B. A. and Priestley H. A. 1990. Introduction to Lattices and Order. Cambridge University Press.]]  Davey B. A. and Priestley H. A. 1990. Introduction to Lattices and Order. Cambridge University Press.]]","key":"e_1_2_1_19_1"},{"unstructured":"DeKok A. 2000. PScan: A limited problem scanner for C source files. http:\/\/www.striker.ottawa.on.ca\/~aland\/pscan.]]  DeKok A. 2000. PScan: A limited problem scanner for C source files. http:\/\/www.striker.ottawa.on.ca\/~aland\/pscan.]]","key":"e_1_2_1_20_1"},{"volume-title":"Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"DeLine R.","unstructured":"DeLine , R. and F\u00e4hndrich , M . 2001. Enforcing high-level protocols in low-level software . In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Snowbird, UT). ACM, New York, 59--69.]] 10.1145\/378795.378811 DeLine, R. and F\u00e4hndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (Snowbird, UT). ACM, New York, 59--69.]] 10.1145\/378795.378811","key":"e_1_2_1_21_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/360051.360056"},{"key":"e_1_2_1_23_1","volume-title":"Tech. Rep. 159","author":"Detlefs D. L.","year":"1998","unstructured":"Detlefs , D. L. , Leino , K. R. M. , Nelson , G. , and Saxe, J. B. 1998 . Extended static checking. Tech. Rep. 159 , Compaq Systems Research Center . Dec.]] Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Tech. Rep. 159, Compaq Systems Research Center. Dec.]]"},{"key":"e_1_2_1_24_1","volume-title":"Second International Symposium (Glasgow, Scotland), A. Mycroft, Ed. Lecture Notes in Computer Science","volume":"983","author":"Dussart D.","unstructured":"Dussart , D. , Henglein , F. , and Mossin , C . 1995. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Static Analysis , Second International Symposium (Glasgow, Scotland), A. Mycroft, Ed. Lecture Notes in Computer Science , vol. 983 . Springer-Verlag, New York, 118--135.]] Dussart, D., Henglein, F., and Mossin, C. 1995. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Static Analysis, Second International Symposium (Glasgow, Scotland), A. Mycroft, Ed. Lecture Notes in Computer Science, vol. 983. Springer-Verlag, New York, 118--135.]]"},{"key":"e_1_2_1_25_1","volume-title":"Eleventh Annual Conference. Electronic Notes in Theoretical Computer Science","volume":"1","author":"Eifrig J.","unstructured":"Eifrig , J. , Smith , S. , and Trifonov , V . 1995. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics , Eleventh Annual Conference. Electronic Notes in Theoretical Computer Science , vol. 1 . Elsevier-North Holland, Amsterdam, The Netherlands.]] Eifrig, J., Smith, S., and Trifonov, V. 1995. Type inference for recursively constrained types and its application to OOP. In Mathematical Foundations of Programming Semantics, Eleventh Annual Conference. Electronic Notes in Theoretical Computer Science, vol. 1. Elsevier-North Holland, Amsterdam, The Netherlands.]]"},{"volume-title":"Proceedings of the 4th Symposium on Operating System Design and Implementation","author":"Engler D.","unstructured":"Engler , D. , Chelf , B. , Chou , A. , and Hallem , S . 2000. Checking system rules using system-specific, programmer-written compiler extensions . In Proceedings of the 4th Symposium on Operating System Design and Implementation ( San Diego, CA).]] Engler, D., Chelf, B., Chou, A., and Hallem, S. 2000. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the 4th Symposium on Operating System Design and Implementation (San Diego, CA).]]","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Evans D.","year":"1996","unstructured":"Evans , D. 1996 . Static detection of dynamic memory errors . Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Philadelphia, PA). ACM, New York, 44--53.]] 10.1145\/231379.231389 Evans, D. 1996. Static detection of dynamic memory errors. Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA). ACM, New York, 44--53.]] 10.1145\/231379.231389"},{"unstructured":"F\u00e4hndrich M. 1999. BANE: A library for scalable constraint-based program analysis. Ph.D. thesis University of California Berkeley.]]  F\u00e4hndrich M. 1999. BANE: A library for scalable constraint-based program analysis. Ph.D. thesis University of California Berkeley.]]","key":"e_1_2_1_28_1"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"F\u00e4hndrich M.","year":"2002","unstructured":"F\u00e4hndrich , M. and DeLine , R. 2002 . Adoption and focus: Practical linear types for imperative programming . Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Berlin, Germany). ACM, New York, 13--24.]] 10.1145\/512529.512532 F\u00e4hndrich, M. and DeLine, R. 2002. Adoption and focus: Practical linear types for imperative programming. Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, Germany). ACM, New York, 13--24.]] 10.1145\/512529.512532"},{"volume-title":"Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (Montreal, Ont., Canada). ACM","author":"F\u00e4hndrich M.","unstructured":"F\u00e4hndrich , M. , Foster , J. S. , Su , Z. , and Aiken , A . 1998. Partial online cycle elimination in inclusion constraint graphs . In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (Montreal, Ont., Canada). ACM , New York, 85--96.]] 10.1145\/277650.277667 F\u00e4hndrich, M., Foster, J. S., Su, Z., and Aiken, A. 1998. Partial online cycle elimination in inclusion constraint graphs. In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (Montreal, Ont., Canada). ACM, New York, 85--96.]] 10.1145\/277650.277667","key":"e_1_2_1_30_1"},{"volume-title":"Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Flanagan C.","unstructured":"Flanagan , C. , Flatt , M. , Krishnamurthi , S. , Weirich , S. , and Felleisen , M . 1996. Catching bugs in the web of program invariants . Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Philadelphia, PA). ACM, New York, 23--32.]] 10.1145\/231379.231387 Flanagan, C., Flatt, M., Krishnamurthi, S., Weirich, S., and Felleisen, M. 1996. Catching bugs in the web of program invariants. Proceedings of the 1996 ACM SIGPLAN Conference on Programming Language Design and Implementation (Philadelphia, PA). ACM, New York, 23--32.]] 10.1145\/231379.231387","key":"e_1_2_1_31_1"},{"key":"e_1_2_1_32_1","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods","volume":"2021","author":"Flanagan C.","unstructured":"Flanagan , C. and Leino , K. R. M. 2001. Houdini, an annotation assitant for ESC\/Java . In FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods ( Berlin, Germany) J. N. Oliverira and P. Zave, Eds. Lecture Notes in Computer Science , vol. 2021 . Springer-Verlag, New York, 500--517.]] Flanagan, C. and Leino, K. R. M. 2001. Houdini, an annotation assitant for ESC\/Java. In FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods (Berlin, Germany) J. N. Oliverira and P. Zave, Eds. Lecture Notes in Computer Science, vol. 2021. Springer-Verlag, New York, 500--517.]]"},{"volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Flanagan C.","unstructured":"Flanagan , C. , Leino , K. R. M. , Lillibridge , M. , Nelson , G. , Saxe , J. B. , and Stata , R . 2002. Extended static checking for Java . Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Berlin, Germany). ACM, New York, 234--245.]] 10.1145\/512529.512558 Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for Java. Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, Germany). ACM, New York, 234--245.]] 10.1145\/512529.512558","key":"e_1_2_1_33_1"},{"volume-title":"Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Foster J. S.","unstructured":"Foster , J. S. , F\u00e4hndrich , M. , and Aiken , A . 1999. A theory of type qualifiers . In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Atlanta, GA). ACM, New York, 192--203.]] 10.1145\/301618.301665 Foster, J. S., F\u00e4hndrich, M., and Aiken, A. 1999. A theory of type qualifiers. In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation (Atlanta, GA). ACM, New York, 192--203.]] 10.1145\/301618.301665","key":"e_1_2_1_35_1"},{"volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Foster J. S.","unstructured":"Foster , J. S. , Terauchi , T. , and Aiken , A . 2002. Flow-sensitive type qualifiers . In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Berlin, Germany). ACM, New York, 1--12.]] 10.1145\/512529.512531 Foster, J. S., Terauchi, T., and Aiken, A. 2002. Flow-sensitive type qualifiers. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, Germany). ACM, New York, 1--12.]] 10.1145\/512529.512531","key":"e_1_2_1_36_1"},{"unstructured":"Frasunek P. 2001a. format string vulnerability in mars_nwe 0.99pl19. http:\/\/online.securityfocus.com\/archive\/1\/158959.]]  Frasunek P. 2001a. format string vulnerability in mars_nwe 0.99pl19. http:\/\/online.securityfocus.com\/archive\/1\/158959.]]","key":"e_1_2_1_37_1"},{"unstructured":"Frasunek P. 2001b. ports\/24733: mars_nwe remote format string vulnerability. http:\/\/groups.google.com\/groups?q=mars_nwe+vulnerability&hl=en&lr=&ie=UTF-8&oe=UTF-8&selm=9566si%24gpv%241%40FreeBSD.csie.NCTU.edu.tw&rnum=1.]]  Frasunek P. 2001b. ports\/24733: mars_nwe remote format string vulnerability. http:\/\/groups.google.com\/groups?q=mars_nwe+vulnerability&hl=en&lr=&ie=UTF-8&oe=UTF-8&selm=9566si%24gpv%241%40FreeBSD.csie.NCTU.edu.tw&rnum=1.]]","key":"e_1_2_1_38_1"},{"volume-title":"Proceedings of the 1991 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Freeman T.","unstructured":"Freeman , T. and Pfenning , F . 1991. Refinement types for ML . In Proceedings of the 1991 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Toronto, Ont., Canada). ACM, New York, 268--277.]] 10.1145\/113445.113468 Freeman, T. and Pfenning, F. 1991. Refinement types for ML. In Proceedings of the 1991 ACM SIGPLAN Conference on Programming Language Design and Implementation (Toronto, Ont., Canada). ACM, New York, 268--277.]] 10.1145\/113445.113468","key":"e_1_2_1_39_1"},{"unstructured":"Gates B. 2002. Trustworthy computing. Microsoft internal memo. Available at http:\/\/www.theregister.co.uk\/content\/4\/23715.html.]]  Gates B. 2002. Trustworthy computing. Microsoft internal memo. Available at http:\/\/www.theregister.co.uk\/content\/4\/23715.html.]]","key":"e_1_2_1_40_1"},{"volume-title":"Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Gay D.","unstructured":"Gay , D. and Aiken , A . 2001. Language support for regions . In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Snowbird, UT). ACM, New York, 70--80.]] 10.1145\/378795.378815 Gay, D. and Aiken, A. 2001. Language support for regions. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (Snowbird, UT). ACM, New York, 70--80.]] 10.1145\/378795.378815","key":"e_1_2_1_41_1"},{"key":"e_1_2_1_42_1","volume-title":"Tech. Rep. MIT\/LCS\/TR-407, MIT Laboratory for Computer Science. Sept.]]","author":"Gifford D. K.","year":"1987","unstructured":"Gifford , D. K. , Jouvelot , P. , Lucassen , J. M. , and Sheldon , M. A . 1987 . FX-87 Reference Manual . Tech. Rep. MIT\/LCS\/TR-407, MIT Laboratory for Computer Science. Sept.]] Gifford, D. K., Jouvelot, P., Lucassen, J. M., and Sheldon, M. A. 1987. FX-87 Reference Manual. Tech. Rep. MIT\/LCS\/TR-407, MIT Laboratory for Computer Science. Sept.]]"},{"volume-title":"Proceedings of the Workshop on Eclipse Technology eXchange","author":"Greenfieldboyce D.","unstructured":"Greenfieldboyce , D. and Foster , J. S . 2004. Visualizing type qualifier inference with eclipse . In Proceedings of the Workshop on Eclipse Technology eXchange ( Vancouver, B.C., Canada). ACM, New York.]] 10.1145\/1066129.1066141 Greenfieldboyce, D. and Foster, J. S. 2004. Visualizing type qualifier inference with eclipse. In Proceedings of the Workshop on Eclipse Technology eXchange (Vancouver, B.C., Canada). ACM, New York.]] 10.1145\/1066129.1066141","key":"e_1_2_1_43_1"},{"volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Grossman D.","unstructured":"Grossman , D. , Morrisett , G. , Jim , T. , Hicks , M. , Wang , Y. , and Cheney , J . 2002. Region-based memory management in cyclone . Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Berlin, Germany). ACM, New York, 282--293.]] 10.1145\/512529.512563 Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., and Cheney, J. 2002. Region-based memory management in cyclone. Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, Germany). ACM, New York, 282--293.]] 10.1145\/512529.512563","key":"e_1_2_1_44_1"},{"key":"e_1_2_1_45_1","volume-title":"Tech. Rep. 2001-1855, Department of Computer Science","author":"Grossman D.","year":"2001","unstructured":"Grossman , D. , Morrisett , G. , Wang , Y. , Jim , T. , Hicks , M. , and Cheney , J . 2001 . Cyclone user's manual. Tech. Rep. 2001-1855, Department of Computer Science , Cornell University . Nov.]] Grossman, D., Morrisett, G., Wang, Y., Jim, T., Hicks, M., and Cheney, J. 2001. Cyclone user's manual. Tech. Rep. 2001-1855, Department of Computer Science, Cornell University. Nov.]]"},{"volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Hallem S.","unstructured":"Hallem , S. , Chelf , B. , Xie , Y. , and Engler , D . 2002. A system and language for building system-specific, static analyses . In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Berlin, Germany). ACM, New York, 69--82.]] 10.1145\/512529.512539 Hallem, S., Chelf, B., Xie, Y., and Engler, D. 2002. A system and language for building system-specific, static analyses. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (Berlin, Germany). ACM, New York, 69--82.]] 10.1145\/512529.512539","key":"e_1_2_1_46_1"},{"unstructured":"Harrelson C. 2001. Program analysis mode. http:\/\/www.cs.berkeley.edu\/~chrishtr\/pam.]]  Harrelson C. 2001. Program analysis mode. http:\/\/www.cs.berkeley.edu\/~chrishtr\/pam.]]","key":"e_1_2_1_47_1"},{"volume-title":"Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Heintze N.","unstructured":"Heintze , N. and Tardieu , O . 2001. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second . In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Snowbird, UT). ACM, New York, 254--263.]] 10.1145\/378795.378855 Heintze, N. and Tardieu, O. 2001. Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (Snowbird, UT). ACM, New York, 254--263.]] 10.1145\/378795.378855","key":"e_1_2_1_48_1"},{"key":"e_1_2_1_49_1","volume-title":"FPCA '91 Conference on Functional Programming Languages and Computer Architecture","volume":"523","author":"Henglein F.","year":"1991","unstructured":"Henglein , F. 1991 . Efficient type inference for higher-order binding-time analysis . In FPCA '91 Conference on Functional Programming Languages and Computer Architecture ( Cambridge, MA), J. Hughes, Ed. Lecture Notes in Computer Science , vol. 523 . Springer-Verlag, New York, 448--472.]] Henglein, F. 1991. Efficient type inference for higher-order binding-time analysis. In FPCA '91 Conference on Functional Programming Languages and Computer Architecture (Cambridge, MA), J. Hughes, Ed. Lecture Notes in Computer Science, vol. 523. Springer-Verlag, New York, 448--472.]]"},{"doi-asserted-by":"publisher","key":"e_1_2_1_50_1","DOI":"10.1145\/169701.169692"},{"unstructured":"Henrion M. 2000. MUH IRC bouncer remote vulnerability. FreeBSD-SA-00:57. http:\/\/www.securityfocus.com\/advisories\/2741.]]  Henrion M. 2000. MUH IRC bouncer remote vulnerability. FreeBSD-SA-00:57. http:\/\/www.securityfocus.com\/advisories\/2741.]]","key":"e_1_2_1_51_1"},{"volume-title":"Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Henzinger T. A.","unstructured":"Henzinger , T. A. , Jhala , R. , Majumdar , R. , and Sutre , G . 2002. Lazy abstraction . In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( Portland, OR). ACM, New York, 58--70.]] 10.1145\/503272.503279 Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2002. Lazy abstraction. In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, OR). ACM, New York, 58--70.]] 10.1145\/503272.503279","key":"e_1_2_1_52_1"},{"volume-title":"Proceedings of the 3rd Symposium on the Foundations of Software Engineering","author":"Horwitz S.","unstructured":"Horwitz , S. , Reps , T. , and Sagiv , M . 1995. Demand interprocedural dataflow analysis . In Proceedings of the 3rd Symposium on the Foundations of Software Engineering ( Washington, DC), 104--115.]] 10.1145\/222124.222146 Horwitz, S., Reps, T., and Sagiv, M. 1995. Demand interprocedural dataflow analysis. In Proceedings of the 3rd Symposium on the Foundations of Software Engineering (Washington, DC), 104--115.]] 10.1145\/222124.222146","key":"e_1_2_1_53_1"},{"unstructured":"Huuskonen J. 2000a. Possibility for format char errors in syslog call. https:\/\/bugzilla.redhat.com\/bugzilla\/show_bug.cgi?id=17349.]]  Huuskonen J. 2000a. Possibility for format char errors in syslog call. https:\/\/bugzilla.redhat.com\/bugzilla\/show_bug.cgi?id=17349.]]","key":"e_1_2_1_54_1"},{"unstructured":"Huuskonen J. 2000b. Some possible format string errors. Linux security audit project mailing list. http:\/\/www2.merton.ox.ac.uk\/~security\/security-audit-200009\/0118.html.]]  Huuskonen J. 2000b. Some possible format string errors. Linux security audit project mailing list. http:\/\/www2.merton.ox.ac.uk\/~security\/security-audit-200009\/0118.html.]]","key":"e_1_2_1_55_1"},{"unstructured":"Huuskonen J. 2000c. syslog(prio buf) in mars_nwe. Linux security audit project mailing list. http:\/\/www2.merton.ox.ac.uk\/~security\/security-audit-200009\/0136.html.]]  Huuskonen J. 2000c. syslog(prio buf) in mars_nwe. Linux security audit project mailing list. http:\/\/www2.merton.ox.ac.uk\/~security\/security-audit-200009\/0136.html.]]","key":"e_1_2_1_56_1"},{"volume-title":"Proceedings of the 13th Usenix Security Symposium","author":"Johnson R.","unstructured":"Johnson , R. and Wagner , D . 2004. Finding user\/kernel bugs with type inference . In Proceedings of the 13th Usenix Security Symposium ( San Diego, CA).]] Johnson, R. and Wagner, D. 2004. Finding user\/kernel bugs with type inference. In Proceedings of the 13th Usenix Security Symposium (San Diego, CA).]]","key":"e_1_2_1_57_1"},{"volume-title":"Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Klarlund N.","unstructured":"Klarlund , N. and Schwartzbach , M. I . 1993. Graph types . In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( Charleston, SC). ACM, New York, 196--205.]] 10.1145\/158511.158628 Klarlund, N. and Schwartzbach, M. I. 1993. Graph types. In Proceedings of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Charleston, SC). ACM, New York, 196--205.]] 10.1145\/158511.158628","key":"e_1_2_1_58_1"},{"volume-title":"Proceedings of the 10th Usenix Security Symposium","author":"Larochelle D.","unstructured":"Larochelle , D. and Evans , D . 2001. Statically detecting likely buffer overflow vulnerabilities . In Proceedings of the 10th Usenix Security Symposium ( Washington, DC).]] Larochelle, D. and Evans, D. 2001. Statically detecting likely buffer overflow vulnerabilities. In Proceedings of the 10th Usenix Security Symposium (Washington, DC).]]","key":"e_1_2_1_59_1"},{"key":"e_1_2_1_60_1","volume-title":"7th International Conference","volume":"1383","author":"Leino K. R. M.","unstructured":"Leino , K. R. M. and Nelson , G . 1998. An extended static checker for modula-3. In Compiler Construction , 7th International Conference ( Lisbon, Portugal). K. Koskimies, Ed. Lecture Notes in Computer Science , vol. 1383 . Springer-Verlag, New York, 302--305.]] Leino, K. R. M. and Nelson, G. 1998. An extended static checker for modula-3. In Compiler Construction, 7th International Conference (Lisbon, Portugal). K. Koskimies, Ed. Lecture Notes in Computer Science, vol. 1383. Springer-Verlag, New York, 302--305.]]"},{"volume-title":"Proceedings of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Liblit B.","unstructured":"Liblit , B. and Aiken , A . 2000. Type systems for distributed data structures . In Proceedings of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( Boston, MA). ACM, New York, 199--213.]] 10.1145\/325694.325717 Liblit, B. and Aiken, A. 2000. Type systems for distributed data structures. In Proceedings of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Boston, MA). ACM, New York, 199--213.]] 10.1145\/325694.325717","key":"e_1_2_1_61_1"},{"volume-title":"Proceedings of the 15th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Lucassen J. M.","unstructured":"Lucassen , J. M. and Gifford , D. K . 1988. Polymorphic effect systems . In Proceedings of the 15th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( San Diego, CA). ACM, New York, 47--57.]] 10.1145\/73560.73564 Lucassen, J. M. and Gifford, D. K. 1988. Polymorphic effect systems. In Proceedings of the 15th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, CA). ACM, New York, 47--57.]] 10.1145\/73560.73564","key":"e_1_2_1_62_1"},{"volume-title":"Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming","author":"Mandelbaum Y.","unstructured":"Mandelbaum , Y. , Walker , D. , and Harper , R . 2003. An effective theory of type refinements . In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming ( Uppsala, Sweden). ACM, New York, 213--225.]] 10.1145\/944705.944725 Mandelbaum, Y., Walker, D., and Harper, R. 2003. An effective theory of type refinements. In Proceedings of the 8th ACM SIGPLAN International Conference on Functional Programming (Uppsala, Sweden). ACM, New York, 213--225.]] 10.1145\/944705.944725","key":"e_1_2_1_63_1"},{"unstructured":"Mars Climate Orbiter Mishap Investigation Board. 1999. Phase I Report. ftp:\/\/ftp.hq.nasa.gov\/pub\/pao\/reports\/1999\/MCO_report.pdf.]]  Mars Climate Orbiter Mishap Investigation Board. 1999. Phase I Report. ftp:\/\/ftp.hq.nasa.gov\/pub\/pao\/reports\/1999\/MCO_report.pdf.]]","key":"e_1_2_1_64_1"},{"key":"e_1_2_1_65_1","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","article-title":"A theory of type polymorphism in programming","volume":"17","author":"Milner R.","year":"1978","unstructured":"Milner , R. 1978 . A theory of type polymorphism in programming . J. Comput. Syst. Sci. 17 , 348 -- 375 .]] Milner, R. 1978. A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348--375.]]","journal-title":"J. Comput. Syst. Sci."},{"key":"e_1_2_1_66_1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S0956796800000113","article-title":"Type inference with simple subtypes","volume":"1","author":"Mitchell J. C.","year":"1991","unstructured":"Mitchell , J. C. 1991 . Type inference with simple subtypes . J. Funct. Prog. 1 , 3 (July), 245--285.]] Mitchell, J. C. 1991. Type inference with simple subtypes. J. Funct. Prog. 1, 3 (July), 245--285.]]","journal-title":"J. Funct. Prog."},{"volume-title":"Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"M\u00f8ller A.","unstructured":"M\u00f8ller , A. and Schwartzbach , M. I . 2001. The pointer assertion logic engine . In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Snowbird, UT). ACM, New York, 221--231.]] 10.1145\/378795.378851 M\u00f8ller, A. and Schwartzbach, M. I. 2001. The pointer assertion logic engine. In Proceedings of the 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (Snowbird, UT). ACM, New York, 221--231.]] 10.1145\/378795.378851","key":"e_1_2_1_67_1"},{"volume-title":"Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Necula G.","unstructured":"Necula , G. , McPeak , S. , and Weimer , W . 2002. CCured: Type-safe retrofitting of legacy code . In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( Portland, OR). ACM, New York, 128--139.]] 10.1145\/503272.503286 Necula, G., McPeak, S., and Weimer, W. 2002. CCured: Type-safe retrofitting of legacy code. In Proceedings of the 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Portland, OR). ACM, New York, 128--139.]] 10.1145\/503272.503286","key":"e_1_2_1_69_1"},{"unstructured":"Newsham T. 2000. Format string attacks. http:\/\/online.securityfocus.com\/guest\/3342.]]  Newsham T. 2000. Format string attacks. http:\/\/online.securityfocus.com\/guest\/3342.]]","key":"e_1_2_1_70_1"},{"volume-title":"Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages, B. Pierce, Ed.]]","author":"Odersky M.","unstructured":"Odersky , M. , Sulzmann , M. , and Wehr , M . 1997. Type inference with constrained types . In Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages, B. Pierce, Ed.]] Odersky, M., Sulzmann, M., and Wehr, M. 1997. Type inference with constrained types. In Proceedings of the 4th International Workshop on Foundations of Object-Oriented Languages, B. Pierce, Ed.]]","key":"e_1_2_1_72_1"},{"key":"e_1_2_1_73_1","first-page":"75","article-title":"Trust in the \u03bb-calculus","volume":"3","author":"\u00d8rb\u00e6k P.","year":"1997","unstructured":"\u00d8rb\u00e6k , P. and Palsberg , J. 1997 . Trust in the \u03bb-calculus . J. Funct. Prog. 3 , 2, 75 -- 85 .]] \u00d8rb\u00e6k, P. and Palsberg, J. 1997. Trust in the \u03bb-calculus. J. Funct. Prog. 3, 2, 75--85.]]","journal-title":"J. Funct. Prog."},{"volume-title":"Types and Programming Languages","author":"Pierce B. C.","unstructured":"Pierce , B. C. 2002. Types and Programming Languages . MIT Press, Cambridge , MA .]] Pierce, B. C. 2002. Types and Programming Languages. MIT Press, Cambridge, MA.]]","key":"e_1_2_1_74_1"},{"unstructured":"PITAC. 1999. President's Information Technology Advisory Committee Report to the President. http:\/\/www.ccic.gov\/ac\/report.]]  PITAC. 1999. President's Information Technology Advisory Committee Report to the President. http:\/\/www.ccic.gov\/ac\/report.]]","key":"e_1_2_1_75_1"},{"volume-title":"Proceedings of the 19th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications. 206--223","author":"Pratikakis P.","unstructured":"Pratikakis , P. , Spacco , J. , and Hicks , M . 2004. Transparent proxies for Java futures . In Proceedings of the 19th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications. 206--223 .]] 10.1145\/1028976.1028994 Pratikakis, P., Spacco, J., and Hicks, M. 2004. Transparent proxies for Java futures. In Proceedings of the 19th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications. 206--223.]] 10.1145\/1028976.1028994","key":"e_1_2_1_76_1"},{"key":"e_1_2_1_77_1","first-page":"1","article-title":"Satisfiability of inequalities in a poset. Funda","volume":"28","author":"Pratt V.","year":"1996","unstructured":"Pratt , V. and Tiuryn , J. 1996 . Satisfiability of inequalities in a poset. Funda . Inf. 28 , 1 - 2 , 165--182.]] Pratt, V. and Tiuryn, J. 1996. Satisfiability of inequalities in a poset. Funda. Inf. 28, 1-2, 165--182.]]","journal-title":"Inf."},{"volume-title":"Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Rehof J.","unstructured":"Rehof , J. and F\u00e4hndrich , M . 2001. Type-based flow analysis: From polymorphic subtyping to CFL-reachability . In Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( London, United Kingdom). ACM, New York, 54--66.]] 10.1145\/360204.360208 Rehof, J. and F\u00e4hndrich, M. 2001. Type-based flow analysis: From polymorphic subtyping to CFL-reachability. In Proceedings of the 28th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London, United Kingdom). ACM, New York, 54--66.]] 10.1145\/360204.360208","key":"e_1_2_1_78_1"},{"key":"e_1_2_1_79_1","volume-title":"Third International Symposium","volume":"1145","author":"Rehof J.","unstructured":"Rehof , J. and Mogensen , T . \u00c6. 1996. Tractable constraints in finite semilattices. In Static Analysis , Third International Symposium ( Aachen, Germany). R. Cousot and D. A. Schmidt, Eds. Lecture Notes in Computer Science , vol. 1145 . Springer-Verlag, New York, 285--300.]] Rehof, J. and Mogensen, T. \u00c6. 1996. Tractable constraints in finite semilattices. In Static Analysis, Third International Symposium (Aachen, Germany). R. Cousot and D. A. Schmidt, Eds. Lecture Notes in Computer Science, vol. 1145. Springer-Verlag, New York, 285--300.]]"},{"key":"e_1_2_1_80_1","volume-title":"Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Reps T.","year":"1994","unstructured":"Reps , T. , Horwitz , S. , and Sagiv , M . 1995. Precise interprocedural dataflow analysis via graph reachability . In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( San Francisco, CA). ACM, New York, 49--61.]] 10.1145\/ 1994 48.199462 Reps, T., Horwitz, S., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph reachability. In Proceedings of the 22nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Francisco, CA). ACM, New York, 49--61.]] 10.1145\/199448.199462"},{"unstructured":"Robbins T. J. 2001. Libformat--Protection against format string attacks. http:\/\/www.wiretapped.net\/~fyre\/software\/libformat.html.]]  Robbins T. J. 2001. Libformat--Protection against format string attacks. http:\/\/www.wiretapped.net\/~fyre\/software\/libformat.html.]]","key":"e_1_2_1_81_1"},{"volume-title":"Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Sagiv M.","unstructured":"Sagiv , M. , Reps , T. , and Wilhelm , R . 1999. Parametric shape analysis via 3-valued logic . In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( San Antonio, TX). ACM, New York, 105--118.]] 10.1145\/292540.292552 Sagiv, M., Reps, T., and Wilhelm, R. 1999. Parametric shape analysis via 3-valued logic. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Antonio, TX). ACM, New York, 105--118.]] 10.1145\/292540.292552","key":"e_1_2_1_82_1"},{"unstructured":"Savola P. 2000. Very probable remote root vulnerability in cfengine. BugTraq mailing list. http:\/\/www.securityfocus.com\/archive\/1\/136751.]]  Savola P. 2000. Very probable remote root vulnerability in cfengine. BugTraq mailing list. http:\/\/www.securityfocus.com\/archive\/1\/136751.]]","key":"e_1_2_1_83_1"},{"volume-title":"Proceedings of the 10th Usenix Security Symposium","author":"Shankar U.","unstructured":"Shankar , U. , Talwar , K. , Foster , J. S. , and Wagner , D . 2001. Detecting format string vulnerabilities with type qualifiers . In Proceedings of the 10th Usenix Security Symposium ( Washington, DC).]] Shankar, U., Talwar, K., Foster, J. S., and Wagner, D. 2001. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the 10th Usenix Security Symposium (Washington, DC).]]","key":"e_1_2_1_84_1"},{"volume-title":"Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (Montreal, Que., Canada) ACM","author":"Skalka C.","unstructured":"Skalka , C. and Smith , S . 2000. Static enforcement of security with types . In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (Montreal, Que., Canada) ACM , New York, 34--45.]] 10.1145\/351240.351244 Skalka, C. and Smith, S. 2000. Static enforcement of security with types. In Proceedings of the 5th ACM SIGPLAN International Conference on Functional Programming (Montreal, Que., Canada) ACM, New York, 34--45.]] 10.1145\/351240.351244","key":"e_1_2_1_85_1"},{"volume-title":"Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","author":"Smith G.","unstructured":"Smith , G. and Volpano , D . 1998. Secure information flow in a multi-threaded imperative language . In Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages ( San Diego, CA). ACM, New York, 355--364.]] 10.1145\/268946.268975 Smith, G. and Volpano, D. 1998. Secure information flow in a multi-threaded imperative language. In Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (San Diego, CA). ACM, New York, 355--364.]] 10.1145\/268946.268975","key":"e_1_2_1_86_1"},{"unstructured":"Stroustrup B. 2005. C&plus;&plus; style and technique FAQ. http:\/\/www.research.att.com\/~bs\/bs_faq2.html#constplacement.]]  Stroustrup B. 2005. C&plus;&plus; style and technique FAQ. http:\/\/www.research.att.com\/~bs\/bs_faq2.html#constplacement.]]","key":"e_1_2_1_88_1"},{"key":"e_1_2_1_89_1","volume-title":"Proceedings of the 16th Annual Computer Security Applications Conference. http:\/\/www.acsac.org.]]","author":"Viega J.","year":"2000","unstructured":"Viega , J. , Bloch , J. , Kohno , T. , and McGraw , G. 2000 . ITS4: A static vulnerability scanner for C and C&plus;&plus; Code . In Proceedings of the 16th Annual Computer Security Applications Conference. http:\/\/www.acsac.org.]] Viega, J., Bloch, J., Kohno, T., and McGraw, G. 2000. ITS4: A static vulnerability scanner for C and C&plus;&plus; Code. In Proceedings of the 16th Annual Computer Security Applications Conference. http:\/\/www.acsac.org.]]"},{"key":"e_1_2_1_90_1","volume-title":"7th International Joint Conference","volume":"1214","author":"Volpano D.","unstructured":"Volpano , D. and Smith , G . 1997. A type-based approach to program security. In Theory and Practice of Software Development , 7th International Joint Conference ( Lille, France). M. Bidoit and M. Dauchet, Eds. Lecture Notes in Computer Science , vol. 1214 . Springer-Verlag, New York, 607--621.]] Volpano, D. and Smith, G. 1997. A type-based approach to program security. In Theory and Practice of Software Development, 7th International Joint Conference (Lille, France). M. Bidoit and M. Dauchet, Eds. Lecture Notes in Computer Science, vol. 1214. Springer-Verlag, New York, 607--621.]]"},{"unstructured":"Wall L. Christiansen T. and Orwant J. 2000. Programming Perl 3rd Edition ed. O'Reilly & Associates.]]   Wall L. Christiansen T. and Orwant J. 2000. Programming Perl 3rd Edition ed. O'Reilly & Associates.]]","key":"e_1_2_1_91_1"},{"key":"e_1_2_1_92_1","volume-title":"LISP and Symbolic Computation 8.","author":"Wright A. K.","year":"1882","unstructured":"Wright , A. K. 1995. Simple imperative polymorphism . In LISP and Symbolic Computation 8. Vol. 4 . 343--356.]] 10.1007\/BF010 1882 8 Wright, A. K. 1995. Simple imperative polymorphism. In LISP and Symbolic Computation 8. Vol. 4. 343--356.]] 10.1007\/BF01018828"},{"doi-asserted-by":"publisher","key":"e_1_2_1_93_1","DOI":"10.1006\/inco.1994.1093"},{"volume-title":"Proceedings of the 10th ACM Conference on Computer and Communication Security","author":"Yang J.","unstructured":"Yang , J. , Kremenek , T. , Xie , Y. , and Engler , D . 2003. MECA: An extensible, expressive system and language for statically checking security properties . In Proceedings of the 10th ACM Conference on Computer and Communication Security ( Washington, DC). ACM, New York, 321--334.]] 10.1145\/948109.948153 Yang, J., Kremenek, T., Xie, Y., and Engler, D. 2003. MECA: An extensible, expressive system and language for statically checking security properties. In Proceedings of the 10th ACM Conference on Computer and Communication Security (Washington, DC). ACM, New York, 321--334.]] 10.1145\/948109.948153","key":"e_1_2_1_94_1"},{"volume-title":"Proceedings of the ACM 1998 Workshop on Java for High-Performance Network Computing. ACM","author":"Yelick K.","unstructured":"Yelick , K. , Semenzato , L. , Pike , G. , Miyamoto , C. , Liblit , B. , Krishnamurthy , A. , Hilfinger , P. , Graham , S. , Gay , D. , Colella , P. , and Aiken , A . 1998. Titanium: A high-performance Java dialect . In Proceedings of the ACM 1998 Workshop on Java for High-Performance Network Computing. ACM , New York.]] Yelick, K., Semenzato, L., Pike, G., Miyamoto, C., Liblit, B., Krishnamurthy, A., Hilfinger, P., Graham, S., Gay, D., Colella, P., and Aiken, A. 1998. Titanium: A high-performance Java dialect. In Proceedings of the ACM 1998 Workshop on Java for High-Performance Network Computing. ACM, New York.]]","key":"e_1_2_1_95_1"},{"volume-title":"Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"Yong S. H.","unstructured":"Yong , S. H. , Horwitz , S. , and Reps , T . 1999. Pointer analysis for programs with structures and casting . In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation ( Atlanta, CA). ACM, New York, 91--103.]] 10.1145\/301618.301647 Yong, S. H., Horwitz, S., and Reps, T. 1999. Pointer analysis for programs with structures and casting. In Proceedings of the 1999 ACM SIGPLAN Conference on Programming Language Design and Implementation (Atlanta, CA). ACM, New York, 91--103.]] 10.1145\/301618.301647","key":"e_1_2_1_96_1"},{"volume-title":"Proceedings of the 11th Usenix Security Symposium","author":"Zhang X.","unstructured":"Zhang , X. , Edwards , A. , and Jaeger , T . 2002. Using CQUAL for static analysis of authorization hook placement . In Proceedings of the 11th Usenix Security Symposium ( San Francisco, CA).]] Zhang, X., Edwards, A., and Jaeger, T. 2002. Using CQUAL for static analysis of authorization hook placement. In Proceedings of the 11th Usenix Security Symposium (San Francisco, CA).]]","key":"e_1_2_1_97_1"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1186632.1186635","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1186632.1186635","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:51Z","timestamp":1750258071000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1186632.1186635"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,11]]},"references-count":93,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2006,11]]}},"alternative-id":["10.1145\/1186632.1186635"],"URL":"https:\/\/doi.org\/10.1145\/1186632.1186635","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2006,11]]},"assertion":[{"value":"2006-11-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}