{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:51:04Z","timestamp":1750308664553,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2007,8,2]],"date-time":"2007-08-02T00:00:00Z","timestamp":1186012800000},"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":[[2007,8,2]]},"abstract":"<jats:p>We show how to limit a program's resource usage in an efficient way, using a novel combination of dynamic checks and static analysis. Usually, dynamic checking is inefficient due to the overhead of checks, while static analysis is difficult and rejects many safe programs. We propose a hybrid approach that solves these problems. We split each resource-consuming operation into two parts. The first is a dynamic check, called reserve. The second is the actual operation, called consume, which does not perform any dynamic checks. The programmer is then free to hoist and combine reserve operations. Combining reserve operations reduces their overhead, while hoisting reserve operations ensures that the program does not run out of resources at an inconvenient time. A static verifier ensures that the program reserves resources before it consumes them. This verification is both easier and more flexible than an a priori static verification of resource usage. We present a sound and efficient static verifier based on Hoare logic and linear inequalities. As an example, we present a version of tar written in Java.<\/jats:p>","DOI":"10.1145\/1275497.1275503","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Enforcing resource bounds via static verification of dynamic checks"],"prefix":"10.1145","volume":"29","author":[{"given":"Ajay","family":"Chander","sequence":"first","affiliation":[{"name":"DoCoMo Labs USA, Palo Alto, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Espinosa","sequence":"additional","affiliation":[{"name":"DoCoMo Labs USA, Palo Alto, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nayeem","family":"Islam","sequence":"additional","affiliation":[{"name":"DoCoMo Labs USA, Palo Alto, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Lee","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, PA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George C.","family":"Necula","sequence":"additional","affiliation":[{"name":"University of California, Berkeley, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,8,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_14"},{"volume-title":"Proceedings of the DARPA Information Survivability Confernce and Exposition.","author":"Chander A.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325703"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/286936.286944"},{"volume-title":"Simplify: A theorem prover for program checking. Tech. Rep. HPL-2003-148, HP Laboratories. July.","year":"2003","author":"Detlefs D.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","unstructured":"Dijkstra E. 1976. A Discipline of Programming. Prentice-Hall.   Dijkstra E. 1976. A Discipline of Programming. Prentice-Hall."},{"key":"e_1_2_1_8_1","unstructured":"Endres T. 2003. Java tar 2.5. http:\/\/www.trustice.com.  Endres T. 2003. Java tar 2.5. http:\/\/www.trustice.com."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/335169.335201"},{"volume-title":"Proceedings of the IEEE Symposium on Security and Privacy","author":"Evans D.","key":"e_1_2_1_10_1"},{"volume":"2021","volume-title":"Proceedings of the IEEE International Symposium on Formal Methods Europe: Formal Methods for Increasing Software Productivity. Lecture Notes in Computer Science","author":"Flanagan C.","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_1_13_1","unstructured":"Gong L. 1999. Inside Java 2 Platform Security. Addison-Wesley.   Gong L. 1999. Inside Java 2 Platform Security. Addison-Wesley."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/176454.176507"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_1_16_1","unstructured":"Jones N. Gomard C. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall.   Jones N. Gomard C. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall."},{"key":"e_1_2_1_17_1","first-page":"2","article-title":"Java-MaC: A run-time assurance tool for Java programs","volume":"55","author":"Kim M.","year":"2001","journal-title":"Electron. Not. Theor. Comput. Sci."},{"key":"e_1_2_1_18_1","unstructured":"Mitchell J. C. 1996. Foundations for Programming Languages. MIT Press Cambridge MA.   Mitchell J. C. 1996. Foundations for Programming Languages. MIT Press Cambridge MA."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263712"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/238721.238781"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360216"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1002\/1096-9128(20001210)12:14<1405::AID-CPE515>3.0.CO;2-O"},{"volume-title":"Proceedings of the IEEE Conference on Open Architectures and Network Programming","author":"Patel P.","key":"e_1_2_1_24_1"},{"volume-title":"Proceedings of the 13th International Conference on Rewriting Techniques and Applications","author":"Shankar N.","key":"e_1_2_1_25_1"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422.322411"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040294.1040302"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/363516.363520"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275503","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1275497.1275503","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:30Z","timestamp":1750276830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275503"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8,2]]},"references-count":28,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,8,2]]}},"alternative-id":["10.1145\/1275497.1275503"],"URL":"https:\/\/doi.org\/10.1145\/1275497.1275503","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2007,8,2]]},"assertion":[{"value":"2007-08-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}