{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:18:01Z","timestamp":1775053081810,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540416357","type":"print"},{"value":"9783540445777","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44577-3_11","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T14:23:39Z","timestamp":1181399019000},"page":"157-175","source":"Crossref","is-referenced-by-count":18,"title":["Extended Static Checking: A Ten-Year Perspective"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,29]]},"reference":[{"key":"11_CR1","unstructured":"Alfred V. Aho, Ravi Sethi, and Jeffrey D. Ullman. Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986."},{"key":"11_CR2","series-title":"Lect Notes Comput Sci","first-page":"32","volume-title":"ECOOP\u201997\u2014Object-oriented Programming: 11th European Conference","author":"P. Almeida S\u00e9rgio","year":"1997","unstructured":"Paulo S\u00e9rgio Almeida. Balloon types: Controlling sharing of state in data types. In Mehmet Aksc,it and Satoshi Matsuoka, editors, ECOOP\u201997\u2014Object-oriented Programming: 11th European Conference, volume 1241 of Lecture Notes in Computer Science, pages 32\u201359. Springer, June 1997."},{"key":"11_CR3","first-page":"239","volume":"34","author":"L. Augustsson","year":"1999","unstructured":"Lennart Augustsson. Cayenne \u2014 a language with dependent types. In Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP\u2019 98), volume 34, number 1 in SIGPLAN Notices, pages 239\u2013250. ACM, January 1999.","journal-title":"Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming (ICFP\u2019 98)"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"John Boyland. Alias burying: Unique variables without destructive reads. Software\u2014Practice & Experience. To appear.","DOI":"10.1002\/spe.370"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E. Clark","year":"1979","unstructured":"Edmund Clark. Language constructs for which it is impossible to obtain good Hoare-like axioms. Journal of the ACM, 26(1):129\u2013147, January 1979.","journal-title":"Journal of the ACM"},{"key":"11_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Informatics\u201410 Years Back, 10 Years Ahead","author":"P. Cousot","year":"2000","unstructured":"Patrick Cousot. Progress on abstract interpretation based formal methods and future challenges. In Informatics\u201410 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: a uni.ed lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238\u2013252, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84\u201396, January 1978.","DOI":"10.1145\/512760.512770"},{"key":"11_CR9","unstructured":"David L. Detlefs, K. Rustan M. Leino, and Greg Nelson. Wrestling with rep exposure. Research Report 156, Digital Equipment Corporation Systems Research Center, July 1998."},{"key":"11_CR10","unstructured":"David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, December 1998."},{"key":"11_CR11","unstructured":"Edsger W. Dijkstra. A Discipline of Programming. Prentice Hall, Englewood Cliffs, NJ, 1976."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. Quickly detecting relevant program invariants. In ICSE 2000, Proceedings of the 22nd International Conference on on Software Engineering, pages 449\u2013458, 2000.","DOI":"10.1109\/ICSE.2000.870435"},{"key":"11_CR13","unstructured":"Extended Static Checking for Java home page, Compaq Systems Research Center. On the web at http:\/\/research.compaq.com\/SRC\/esc\/ ."},{"key":"11_CR14","unstructured":"Cormac Flanagan, Rajeev Joshi, and K. Rustan M. Leino. Annotation inference for modu lar checkers. Information Processing Letters. To appear."},{"key":"11_CR15","unstructured":"Cormac Flanagan and K. Rustan M. Leino. Houdini, an annotation assistant for ESC\/Java. Technical Note 2000-003, Compaq Systems Research Center, 2000."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Steven M. German. Automating proofs of the absence of common runtime errors. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 105\u2013118, 1978.","DOI":"10.1145\/512760.512772"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"John Hogg. Islands: Aliasing protection in object-oriented languages. In Andreas Paepcke, editor, Object-Oriented Programming Systems, Languages, and Applications (OOPSLA\u201991), pages 271\u2013285. ACM Press, October 1991.","DOI":"10.1145\/117954.117975"},{"key":"11_CR18","unstructured":"S. C. Johnson. Lint, a C program checker. Computer Science Technical Report 65, Bell Laboratories, Murray Hill, NJ 07974, 1978."},{"key":"11_CR19","unstructured":"K. Rustan M. Leino. Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, 1995. Technical Report Caltech-CS-TR-95-03."},{"key":"11_CR20","unstructured":"K. Rustan M. Leino. Ecstatic: An object-oriented programming language with an axiomatic semantics. In The Fourth International Workshop on Foundations of Object-Oriented Languages, January 1997. Proceedings available from http:\/\/www.cs.williams.edu\/~kim\/FOOL\/ ."},{"issue":"10","key":"11_CR21","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/286936.286953","volume":"33","author":"K. R. M. Leino","year":"1998","unstructured":"K. Rustan M. Leino. Data groups: Specifying the modi.cation of extended state. In Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA\u2019 98), volume 33, number 10 in SIGPLAN Notices, pages 144\u2013153. ACM, October 1998.","journal-title":"Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA\u2019 98)"},{"key":"11_CR22","unstructured":"K. Rustan M. Leino and Greg Nelson. Data abstraction and information hiding. Research Report 160, Compaq Systems Research Center, 2000."},{"key":"11_CR23","unstructured":"K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC\/Java user\u2019s manual. Technical Note 2000-002, Compaq Systems Research Center, October 2000."},{"key":"11_CR24","unstructured":"K. Rustan M. Leino, James B. Saxe, and Raymie Stata. Checking Java programs via guarded commands. In Bart Jacobs, Gary T. Leavens, Peter M\u00fcller, and Arnd Poetzsch-Heffter, editors, Formal Techniques for Java Programs, Technical Report 251. Fernuniversit\u00e4t Hagen, May 1999. Also available as Technical Note 1999\u2013002, Compaq Systems Research Center."},{"key":"11_CR25","unstructured":"K. Rustan M. Leino and Raymie Stata. Checking object invariants. Technical Note 1997\u2013007, Digital Equipment Corporation Systems Research Center, January 1997."},{"key":"11_CR26","unstructured":"Barbara Liskov and John Guttag. Abstraction and Specification in Program Development. MIT Electrical Engineering and Computer Science Series. MIT Press, 1986."},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"David C. Luckham. Programming with Specifications: An Introduction to ANNA, a Language for Specifying Ada Programs. Texts and Monographs in Computer Science. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4613-9685-7"},{"key":"11_CR28","volume-title":"Series in Computer Science","author":"B. Meyer","year":"1988","unstructured":"Bertrand Meyer. Object-oriented Software Construction. Series in Computer Science. Prentice-Hall International, New York, 1988."},{"key":"11_CR29","unstructured":"Todd Millstein. Toward more informative ESC\/Java warning messages. In James Mason, editor, Selected 1999 SRC Summer Intern Reports, Technical Note 1999\u2013003. Compaq Systems Research Center, 1999."},{"key":"11_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BFb0053062","volume-title":"ECOOP\u201996\u2014Object-Oriented Programming: 10th European Conference","author":"N. H. Minsky","year":"1996","unstructured":"Naftaly H. Minsky. Towards alias-free pointers. In Pierre Cointe, editor, ECOOP\u201996\u2014Object-Oriented Programming: 10th European Conference, volume 1098 of Lecture Notes in Computer Science, pages 189\u2013209. Springer, July 1996."},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Greg Nelson. Combining satisfiability procedures by equality-sharing. In W. W. Bledsoe and D. W. Loveland, editors, Automated Theorem Proving: After 25 Years, volume 29 of Contemporary Mathematics, pages 201\u2013211. American Mathematical Society, 1984.","DOI":"10.1090\/conm\/029\/11"},{"issue":"2","key":"11_CR32","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, October 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR33","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP\u201998\u2014Object-oriented Programming: 12th European Conference","author":"J. Noble","year":"1998","unstructured":"James Noble, Jan Vitek, and John Potter. Flexible alias protection. In Eric Jul, editor, ECOOP\u201998\u2014Object-oriented Programming: 12th European Conference, volume 1445 of Lecture Notes in Computer Science, pages 158\u2013185. Springer, July 1998."},{"issue":"5","key":"11_CR34","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1145\/355602.361309","volume":"15","author":"D. L. Parnas","year":"1972","unstructured":"D. L. Parnas. A technique for software module specification with examples. Communications of the ACM, 15(5):330\u2013336, May 1972.","journal-title":"Communications of the ACM"},{"key":"11_CR35","unstructured":"PRE.x. Intrinsa, Mountain View, CA, 1999."},{"issue":"3","key":"11_CR36","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1002\/spe.4380020303","volume":"2","author":"E. Satterthwaite","year":"1972","unstructured":"E. Satterthwaite. Debugging tools for high level languages. Software\u2014Practice & Experience, 2(3):197\u2013217, July-September 1972.","journal-title":"Software\u2014Practice & Experience"},{"key":"11_CR37","series-title":"Lect Notes Comput Sci","volume-title":"Informatics\u201410 Years Back, 10 Years Ahead","author":"F. B. Schneider","year":"2000","unstructured":"Fred B. Schneider, Greg Morrisett, and Robert Harper. A language-based approach to security. In Informatics\u201410 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science. Springer-Verlag, 2000."},{"key":"11_CR38","unstructured":"Richard L. Sites. Proving that Computer Programs Terminate Cleanly. PhDthesis, Stanford University, Stanford, CA 94305, May 1974. Technical Report STAN-CS-74-418."},{"key":"11_CR39","unstructured":"Mark Utting. Reasoning about aliasing. In Proceedings of the Fourth Australasian Refinement Workshop (ARW-95), pages 195\u2013211. School of Computer Science and Engineering, The University of New South Wales, April 1995."},{"key":"11_CR40","doi-asserted-by":"crossref","unstructured":"Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Conference Record of POPL\u201999: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 214\u2013227, January 1999.","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44577-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T20:06:29Z","timestamp":1556481989000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44577-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540416357","9783540445777"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-44577-3_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}