{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:53:46Z","timestamp":1725573226306},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540254355"},{"type":"electronic","value":"9783540319870"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31987-0_22","type":"book-chapter","created":{"date-parts":[[2010,12,20]],"date-time":"2010-12-20T13:42:00Z","timestamp":1292852520000},"page":"311-325","source":"Crossref","is-referenced-by-count":15,"title":["Enforcing Resource Bounds via Static Verification of Dynamic Checks"],"prefix":"10.1007","author":[{"given":"Ajay","family":"Chander","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Espinosa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nayeem","family":"Islam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George","family":"Necula","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","volume-title":"Foundations for Programming Languages","author":"J.C. Mitchell","year":"1996","unstructured":"Mitchell, J.C.: Foundations for Programming Languages. MIT Press, Cambridge (1996)"},{"key":"22_CR2","volume-title":"A Discipline of Programming","author":"E. Dijkstra","year":"1976","unstructured":"Dijkstra, E.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01, 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"22_CR4","unstructured":"Detlefs, D., Nelson, G., Saxe, J.: Simplify: a theorem prover for program checking. Technical Report HPL-2003-148, HP Laboratories (2003)"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, R., Lilibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation, Berlin, Germany (2002)","DOI":"10.1145\/512529.512558"},{"key":"22_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. Journal of the ACM\u00a031, 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Necula, G.: Proof-carrying code. In: Principles of Programming Languages, Paris, France (1997)","DOI":"10.1145\/263699.263712"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","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":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, p. 500. Springer, Heidelberg (2001)"},{"key":"22_CR10","unstructured":"Endres, T.: Java Tar 2.5 (2003), http:\/\/www.trustice.com"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: Principles of Programming Languages, London, England (2001)","DOI":"10.1145\/360204.360216"},{"key":"22_CR12","volume-title":"Partial Evaluation and Automatic Program Generation","author":"N. Jones","year":"1993","unstructured":"Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1145\/176454.176507","volume":"2","author":"R. Gupta","year":"1993","unstructured":"Gupta, R.: Optimizing array bound checks using flow analysis. ACM Letters on Programming Languages and Systems\u00a02, 135\u2013150 (1993)","journal-title":"ACM Letters on Programming Languages and Systems"},{"key":"22_CR14","volume-title":"Principles of Programming Languages","author":"K. Crary","year":"2000","unstructured":"Crary, K., Weirich, S.: Resource bound certification. In: Principles of Programming Languages, Boston, Massachusetts (2000)"},{"key":"22_CR15","volume-title":"Inside Java 2 Platform Security","author":"L. Gong","year":"1999","unstructured":"Gong, L.: Inside Java 2 Platform Security. Addison-Wesley, Reading (1999)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Czajkowski, G., von Eicken, T.: JRes: a resource accounting interface for Java. In: Object-Oriented Programming, Systems, Languages, and Applications, Vancouver, BC (1998)","DOI":"10.1145\/286936.286944"},{"key":"22_CR17","volume-title":"Security and Privacy","author":"D. Evans","year":"1999","unstructured":"Evans, D., Twyman, A.: Flexible policy-directed code safety. In: Security and Privacy, Oakland, California (1999)"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Erlingsson, U., Schneider, F.: SASI enforcement of security policies: a retrospective. In: New Security Paradigms Workshop, Caledon, Canada (1999)","DOI":"10.1109\/DISCEX.2000.821527"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Principles of Programming Languages, Boston, Massachusetts (2000)","DOI":"10.1145\/325694.325703"},{"key":"22_CR20","doi-asserted-by":"publisher","first-page":"1405","DOI":"10.1002\/1096-9128(20001210)12:14<1405::AID-CPE515>3.0.CO;2-O","volume":"12","author":"R. Pandey","year":"2000","unstructured":"Pandey, R., Hashii, B.: Providing fine-grained access control for Java programs via binary editing. Concurrency: Practice and Experience\u00a012, 1405\u20131430 (2000)","journal-title":"Concurrency: Practice and Experience"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Chander, A., Mitchell, J., Shin, I.: Mobile code security by Java bytecode instrumentation. In: DARPA Information Survivability Confernce and Exposition (2001)","DOI":"10.1109\/DISCEX.2001.932157"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Kim, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance tool for Java programs. Electronic Notes in Theoretical Computer Science 55 (2001)","DOI":"10.1016\/S1571-0661(04)00254-3"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Necula, G., Lee, P.: Safe kernel extensions without run-time checking. In: Operating Systems Design and Implementation, Seattle, Washington (1996)","DOI":"10.1145\/238721.238781"},{"key":"22_CR24","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1145\/363516.363520","volume":"9","author":"D. Wallach","year":"2000","unstructured":"Wallach, D., Appel, A., Felten, E.: SAFKASI: a security mechanism for language-based systems. Transactions on Software Engineering\u00a09, 341\u2013378 (2000)","journal-title":"Transactions on Software Engineering"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Patel, P., Lepreau, J.: Hybrid resource control of active extensions. In: Open Architectures and Network Programming, San Francisco, California (2003)","DOI":"10.1109\/OPNARC.2003.1196370"},{"key":"22_CR26","unstructured":"Vanderwaart, J., Crary, K.: Foundational typed assembly language for grid computing. Technical Report CMU-CS-04-104, Carnegie-Mellon University (2004)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31987-0_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:33:20Z","timestamp":1605742400000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31987-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540254355","9783540319870"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31987-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}