{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T11:00:13Z","timestamp":1753182013599,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4S","license":[{"start":{"date-parts":[[2013,7,9]],"date-time":"2013-07-09T00:00:00Z","timestamp":1373328000000},"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":["SIGPLAN Not."],"published-print":{"date-parts":[[2013,7,9]]},"abstract":"<jats:p>Software development and maintenance are costly endeavors. The cost can be reduced if more software defects are detected earlier in the development cycle. This paper introduces the Extended Static Checker for Java (ESC\/Java), an experimental compile-time program checker that finds common programming errors. The checker is powered by verification-condition generation and automatic theoremproving techniques. It provides programmers with a simple annotation language with which programmer design decisions can be expressed formally. ESC\/Java examines the annotated software and warns of inconsistencies between the design decisions recorded in the annotations and the actual code, and also warns of potential runtime errors in the code. This paper gives an overview of the checker architecture and annotation language and describes our experience applying the checker to tens of thousands of lines of Java programs.<\/jats:p>","DOI":"10.1145\/2502508.2502520","type":"journal-article","created":{"date-parts":[[2013,7,16]],"date-time":"2013-07-16T18:06:45Z","timestamp":1373998005000},"page":"22-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["PLDI 2002"],"prefix":"10.1145","volume":"48","author":[{"given":"Cormac","family":"Flanagan","sequence":"first","affiliation":[{"name":"Compaq Systems Research Center, Palo Alto, CA"}]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, WA"}]},{"given":"Mark","family":"Lillibridge","sequence":"additional","affiliation":[{"name":"Compaq Systems Research Center, Palo Alto, CA"}]},{"given":"Greg","family":"Nelson","sequence":"additional","affiliation":[{"name":"Compaq Systems Research Center, Palo Alto, CA"}]},{"given":"James B.","family":"Saxe","sequence":"additional","affiliation":[{"name":"Compaq Systems Research Center, Palo Alto, CA"}]},{"given":"Raymie","family":"Stata","sequence":"additional","affiliation":[{"name":"Compaq Systems Research Center, Palo Alto, CA"}]}],"member":"320","published-online":{"date-parts":[[2013,7,9]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"LNCS","first-page":"103","volume-title":"Proc. 8th SPIN Workshop","author":"Ball T.","year":"2001","unstructured":"T. Ball and S. K. Rajamani . Automatically validating temporal safety properties of interfaces . In M. B. Dwyer, editor, Proc. 8th SPIN Workshop , volume 2057 of LNCS , pages 103 -- 122 . Springer , May 2001 . T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In M. B. Dwyer, editor, Proc. 8th SPIN Workshop, volume 2057 of LNCS, pages 103--122. Springer, May 2001."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(200006)30:7%3C775::AID-SPE309%3E3.0.CO;2-H"},{"key":"e_1_2_1_4_1","volume-title":"Proc. of Formal Methods Europe (FME 2002","author":"Cata\u00f1o N.","year":"2002","unstructured":"N. Cata\u00f1o and M. Huisman . Formal specification of Gemplus' electronic purse case study . In Proc. of Formal Methods Europe (FME 2002 ). Springer-Verlag , 2002 . To Appear. N. Cata\u00f1o and M. Huisman. Formal specification of Gemplus' electronic purse case study. In Proc. of Formal Methods Europe (FME 2002). Springer-Verlag, 2002. To Appear."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/337180.337234"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378811"},{"key":"e_1_2_1_10_1","volume-title":"A Discipline of Programming","author":"Dijkstra E. W.","year":"1976","unstructured":"E. W. Dijkstra . A Discipline of Programming . Prentice Hall , Englewood Cliffs, NJ , 1976 . E. W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976."},{"key":"e_1_2_1_11_1","volume-title":"Dept. of Comp. and Inf. Sciences","author":"Dwyer M.","year":"2001","unstructured":"M. Dwyer , J. Hatcliff , and R. Howell . CIS 771: Software specification. Kansas State Univ ., Dept. of Comp. and Inf. Sciences , Spring 2001 . M. Dwyer, J. Hatcliff, and R. Howell. CIS 771: Software specification. Kansas State Univ., Dept. of Comp. and Inf. Sciences, Spring 2001."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502041"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/302405.302467"},{"key":"e_1_2_1_14_1","unstructured":"Escher Technologies Inc. Getting started with Perfect. Available from www.eschertech.com 2001.  Escher Technologies Inc. Getting started with Perfect. Available from www.eschertech.com 2001."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/193173.195297"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0020-0190(00)00196-4"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"C.\n      Flanagan\n     and \n      K. R. M.\n      Leino\n    . Houdini an annotation assistant for ESC\/Java\n  . In J. N. Oliveira and P. Zave editors FME \n  2001\n  : Formal Methods for Increasing Software Productivity volume \n  2021\n   of \n  LNCS pages \n  500\n  --\n  517\n  . \n  Springer Mar. 2001.   C. Flanagan and K. R. M. Leino. Houdini an annotation assistant for ESC\/Java. In J. N. Oliveira and P. Zave editors FME 2001: Formal Methods for Increasing Software Productivity volume 2021 of LNCS pages 500--517. Springer Mar. 2001.","DOI":"10.1007\/3-540-45251-6_29"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_2_1_20_1","series-title":"LNCS","first-page":"72","volume-title":"Proc. 9th CAV","author":"Graf S.","year":"1997","unstructured":"S. Graf and H. Sa\u00efdi . Construction of abstract state graphs via PVS . In O. Grumberg, editor, Proc. 9th CAV , volume 1254 of LNCS , pages 72 -- 83 . Springer , 1997 . S. Graf and H. Sa\u00efdi. Construction of abstract state graphs via PVS. In O. Grumberg, editor, Proc. 9th CAV, volume 1254 of LNCS, pages 72--83. Springer, 1997."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019213109274"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/367845.367996"},{"key":"e_1_2_1_27_1","first-page":"4","article-title":"An object-oriented programming language with an axiomatic semantics","author":"Leino K. R. M.","year":"1997","unstructured":"K. R. M. Leino . Ecstatic : An object-oriented programming language with an axiomatic semantics . In FOOL 4 , 1997 . K. R. M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. In FOOL 4, 1997.","journal-title":"FOOL"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286953"},{"key":"e_1_2_1_29_1","doi-asserted-by":"crossref","unstructured":"K. R. M.\n      Leino\n    .\n  Applications of extended static checking\n  . In P. Cousot editor 8th Intl. Static Analysis Symp. volume \n  2126\n   of \n  LNCS pages \n  185\n  --\n  193\n  . \n  Springer July \n  2001\n  .   K. R. M. Leino. Applications of extended static checking. In P. Cousot editor 8th Intl. Static Analysis Symp. volume 2126 of LNCS pages 185--193. Springer July 2001.","DOI":"10.1007\/3-540-47764-0_11"},{"key":"e_1_2_1_30_1","doi-asserted-by":"crossref","unstructured":"K. R. M.\n      Leino\n    .\n  Extended static checking: A ten-year perspective\n  . In R. Wilhelm editor Informatics'10 Years Back 10 Years Ahead volume \n  2000\n   of \n  LNCS pages \n  157\n  --\n  175\n  . \n  Springer Jan. \n  2001\n  .   K. R. M. Leino. Extended static checking: A ten-year perspective. In R. Wilhelm editor Informatics'10 Years Back 10 Years Ahead volume 2000 of LNCS pages 157--175. Springer Jan. 2001.","DOI":"10.1007\/3-540-44577-3_11"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00165-0"},{"key":"e_1_2_1_33_1","volume-title":"Compaq SRC","author":"Leino K. R. M.","year":"2000","unstructured":"K. R. M. Leino , G. Nelson , and J. B. Saxe . ESC\/Java user's manual. Tech. Note 2000-002 , Compaq SRC , Oct. 2000 . K. R. M. Leino, G. Nelson, and J. B. Saxe. ESC\/Java user's manual. Tech. Note 2000-002, Compaq SRC, Oct. 2000."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512559"},{"key":"e_1_2_1_36_1","volume-title":"DEC SRC","author":"Leino K. R. M.","year":"1997","unstructured":"K. R. M. Leino and R. Stata . Checking object invariants. Tech. Note 1997-007 , DEC SRC , Jan. 1997 . K. R. M. Leino and R. Stata. Checking object invariants. Tech. Note 1997-007, DEC SRC, Jan. 1997."},{"key":"e_1_2_1_37_1","series-title":"Series in Computer Science","volume-title":"Object-oriented software construction","author":"Meyer B.","year":"1988","unstructured":"B. Meyer . Object-oriented software construction . Series in Computer Science . Prentice-Hall Intl ., 1988 . B. Meyer. Object-oriented software construction. Series in Computer Science. Prentice-Hall Intl., 1988."},{"key":"e_1_2_1_38_1","volume-title":"Compaq SRC","author":"Millstein T.","year":"1999","unstructured":"T. Millstein . Toward more informative ESC\/Java warning messages. In J. Mason, editor, Selected 1999 SRC summer intern reports, Tech. Note 1999-003 . Compaq SRC , 1999 . T. Millstein. Toward more informative ESC\/Java warning messages. In J. Mason, editor, Selected 1999 SRC summer intern reports, Tech. Note 1999-003. Compaq SRC, 1999."},{"key":"e_1_2_1_41_1","series-title":"LNCS","first-page":"411","volume-title":"Proc. 8th CAV","author":"Owre S.","year":"1996","unstructured":"S. Owre , S. Rajan , J. M. Rushby , N. Shankar , and M. K. Srivas . PVS: Combining specification, proof checking, and model checking . In R. Alur and T. A. Henzinger, editors, Proc. 8th CAV , volume 1102 of LNCS , pages 411 -- 414 . Springer , 1996 . S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Proc. 8th CAV, volume 1102 of LNCS, pages 411--414. Springer, 1996."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/366214.366268"},{"key":"e_1_2_1_43_1","volume-title":"Proc.","author":"Sterling N.","year":"1993","unstructured":"N. Sterling . WARLOCK --- a static data race analysis tool . In Proc. Winter 1993 USENIX Conf., pages 97--106. USENIX Assoc. , Jan. 1993. N. Sterling. WARLOCK --- a static data race analysis tool. In Proc. Winter 1993 USENIX Conf., pages 97--106. USENIX Assoc., Jan. 1993."},{"key":"e_1_2_1_44_1","first-page":"21","article-title":"La verification des programmes d'ariane","volume":"243","author":"Turin M.","year":"1998","unstructured":"M. Turin , A. Deutsch , and G. Gonthier . La verification des programmes d'ariane . Pour la Science , 243 : 21 -- 22 , Jan. 1998 . (In French). M. Turin, A. Deutsch, and G. Gonthier. La verification des programmes d'ariane. Pour la Science, 243:21--22, Jan. 1998. (In French).","journal-title":"Pour la Science"},{"key":"e_1_2_1_45_1","series-title":"LNCS","first-page":"299","volume-title":"Proc. TACAS","author":"van den Berg J.","year":"2001","unstructured":"J. van den Berg and B. Jacobs . The LOOP compiler for Java and JML . In Proc. TACAS , volume 2031 of LNCS , pages 299 -- 312 . Springer , 2001 . J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In Proc. TACAS, volume 2031 of LNCS, pages 299--312. Springer, 2001."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/786768.786967"},{"key":"e_1_2_1_48_1","volume-title":"Software Engineering with B","author":"Wordsworth J. B.","year":"1996","unstructured":"J. B. Wordsworth . Software Engineering with B . Addison-Wesley , 1996 . J. B. Wordsworth. Software Engineering with B. Addison-Wesley, 1996."},{"key":"e_1_2_1_49_1","first-page":"375","volume-title":"Proc. 15th LICS","author":"Xi H.","year":"2000","unstructured":"H. Xi . Imperative programming with dependent types . In Proc. 15th LICS , pages 375 -- 387 , June 2000 . H. Xi. Imperative programming with dependent types. In Proc. 15th LICS, pages 375--387, June 2000."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502508.2502520","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2502508.2502520","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:54Z","timestamp":1750234734000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2502508.2502520"}},"subtitle":["Extended static checking for Java"],"short-title":[],"issued":{"date-parts":[[2013,7,9]]},"references-count":40,"journal-issue":{"issue":"4S","published-print":{"date-parts":[[2013,7,9]]}},"alternative-id":["10.1145\/2502508.2502520"],"URL":"https:\/\/doi.org\/10.1145\/2502508.2502520","relation":{},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"type":"print","value":"0362-1340"},{"type":"electronic","value":"1558-1160"}],"subject":[],"published":{"date-parts":[[2013,7,9]]},"assertion":[{"value":"2013-07-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}