{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:43:35Z","timestamp":1725486215367},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423140"},{"type":"electronic","value":"9783540477648"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-47764-0_11","type":"book-chapter","created":{"date-parts":[[2007,6,12]],"date-time":"2007-06-12T04:55:55Z","timestamp":1181624155000},"page":"185-193","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Applications of Extended Static Checking"],"prefix":"10.1007","author":[{"given":"K.","family":"Rustan","sequence":"first","affiliation":[]},{"given":"M.","family":"Leino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Thomas Ball and Sriram K. Rajamani. Automatically validating temporal safety properties of interfaces. In Proceedings SPIN 2001, 2001. To appear.","DOI":"10.1007\/3-540-45139-0_7"},{"key":"11_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/3-540-44518-8_21","volume-title":"Abstract State Machines, Theory and Applications, International Workshop, ASM 2000","author":"M. Barnett","year":"2000","unstructured":"Mike Barnett, Egon B\u00f6rger, Yuri Gurevich, Wolfram Schulte, and Margus Veanes. Using abstract state machines at Microsoft: A case study. In Abstract State Machines, Theory and Applications, International Workshop, ASM 2000, volume 1912 of Lecture Notes in Computer Science, pages 367\u2013379. Springer, 2000."},{"key":"11_CR3","unstructured":"John Boyland. Alias burying: Unique variables without destructive reads. Software\u2014Practice & Experience, To appear."},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","volume":"30","author":"W. R. Bush","year":"2000","unstructured":"William R. Bush, Jonathan D. Pincus, and David J. Sielaff. A static analyzer for finding dynamic programming errors. Software\u2014Practice & Experience, 30:775\u2013802, 2000.","journal-title":"Software\u2014Practice & Experience"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified 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. ACM, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"11_CR6","unstructured":"Rob DeLine and Manuel F\u00e4hndrich. Vault project home page. On the web at http:\/\/research.microsoft.com\/vault\/ , 2001."},{"key":"11_CR7","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_CR8","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_CR9","unstructured":"Michael D. Ernst, Adam Czeisler, William G. Griswold, and David Notkin. Quickly detecting relevant program invariants. In Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), Limerick, Ireland, June 2000."},{"key":"11_CR10","unstructured":"Extended Static Checking for Java home page. On the web at http:\/\/research.compaq.com\/SRC\/esc\/ , November 2000."},{"key":"11_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C. Flanagan","year":"2001","unstructured":"Cormac Flanagan and K. Rustan M. Leino. Houdini, an annotation assistant for ESC\/Java. In Jos\u00e9 Nuno Oliveira and Pamela Zave, editors, FME 2001: Formal Methods for Increasing Software Productivity, volume 2021 of Lecture Notes in Computer Science, pages 500\u2013517. Springer, March 2001."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Rustan M. Leino. Data groups: Specifying the modification 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.","DOI":"10.1145\/286942.286953"},{"key":"11_CR13","series-title":"Lect Notes Comput Sci","first-page":"157","volume-title":"Informatics\u201410 Years Back, 10 Years Ahead","author":"K. Rustan","year":"2001","unstructured":"K. Rustan M. Leino. Extended static checking: A ten-year perspective. In Reinhard Wilhelm, editor, Informatics\u201410 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pages 157\u2013175. Springer, January 2001."},{"key":"11_CR14","unstructured":"K. Rustan M. Leino and Greg Nelson. Data abstraction and information hiding. Research Report 160, Compaq Systems Research Center, November 2000."},{"key":"11_CR15","unstructured":"K. Rustan M. Leino, Greg Nelson, and James B. Saxe. ESC\/Java user\u2019s manual. Technical Note 2000-002, Compaq Systems Research Center, November 2000."},{"key":"11_CR16","unstructured":"Barbara Liskov and John Guttag. Abstraction and Specification in Program Development. MIT Electrical Engineering and Computer Science Series. MIT Press, 1986."},{"key":"11_CR17","unstructured":"Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. MIT Press, 1990."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Peter M\u00fcller. Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversit\u00e4t Hagen, 2001. Available from http:\/\/www.informatik.fernuni-hagen.de\/pi5\/publications.html .","DOI":"10.1007\/3-540-45651-1"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Jeremy W. Nimmer and Michael D. Ernst. Static verification of dynamically detected program invariants: Integrating Daikon and ESC\/Java. In preparation, MIT, 2001.","DOI":"10.1016\/S1571-0661(04)00256-7"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-47764-0_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,12]],"date-time":"2023-05-12T10:41:38Z","timestamp":1683888098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-47764-0_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423140","9783540477648"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-47764-0_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"4 July 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}