{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,1]],"date-time":"2026-04-01T14:19:22Z","timestamp":1775053162647,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540205364","type":"print"},{"value":"9783540400189","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-40018-9_15","type":"book-chapter","created":{"date-parts":[[2010,9,5]],"date-time":"2010-09-05T23:03:20Z","timestamp":1283727800000},"page":"212-229","source":"Crossref","is-referenced-by-count":20,"title":["Resource Usage Verification"],"prefix":"10.1007","author":[{"given":"Kim","family":"Marriott","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Sulzmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","first-page":"162","volume-title":"Proc. of LICS 1992","author":"J. Talpin","year":"1992","unstructured":"Talpin, J., Jouvelot, P.: The type and effect discipline. In: Proc. of LICS 1992, pp. 162\u2013173. IEEE, Los Alamitos (1992)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Marriott, K., Stuckey, P., Sulzmann, M.: Resource usage verification. Technical report, University of Melbourne (2003), \n                    \n                      http:\/\/www.cs.mu.oz.au\/~pjs\/ruv.ps.gz","DOI":"10.1007\/978-3-540-40018-9_15"},{"key":"15_CR3","volume-title":"Languages and Machines","author":"T. Sudkamp","year":"1988","unstructured":"Sudkamp, T.: Languages and Machines. Addison-Wesley, Reading (1988)"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"F.B. Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. Information and System Security\u00a03, 30\u201350 (2000)","journal-title":"Information and System Security"},{"key":"15_CR5","first-page":"238","volume-title":"Proc. of POPL 1977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL 1977, pp. 238\u2013252. ACM, New York (1977)"},{"key":"15_CR6","first-page":"54","volume-title":"Proc. of POPL 2000","author":"T. Colcombet","year":"2000","unstructured":"Colcombet, T., Fradet, P.: Enforcing trace properties by program transformation. In: Proc. of POPL 2000, pp. 54\u201366. ACM, New York (2000)"},{"key":"15_CR7","first-page":"59","volume-title":"Proc. of PLDI 2001","author":"R. DeLine","year":"2001","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. of PLDI 2001, pp. 59\u201369. ACM, New York (2001)"},{"key":"15_CR8","first-page":"282","volume-title":"Proc. of PLDI 2001","author":"D. Grossman","year":"2001","unstructured":"Grossman, D., Morrisett, G., Jim, T., Hicks, M., Wang, Y., Cheney, J.: Region-based memory management in cyclone. In: Proc. of PLDI 2001, pp. 282\u2013293. ACM, New York (2001)"},{"key":"15_CR9","unstructured":"Tan, G., Ou, X., Walker, D.: Resource usage analysis via scoped methods. In: Foundations of Object-Oriented Languages, FOOL\u201910 (2003)"},{"key":"15_CR10","first-page":"331","volume-title":"Proc. of POPL 2002","author":"A. Igarashi","year":"2002","unstructured":"Igarashi, A., Kobayashi, N.: Resource usage analysis. In: Proc. of POPL 2002, pp. 331\u2013342. ACM, New York (2002)"},{"key":"15_CR11","first-page":"1","volume-title":"Proc. of PLDI 2002","author":"J.S. Foster","year":"2002","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. of PLDI 2002, pp. 1\u201312. ACM, New York (2002)"},{"key":"15_CR12","first-page":"69","volume-title":"Proc. of PLDI 2002","author":"S. Hallem","year":"2002","unstructured":"Hallem, S., Chelf, B., Xie, Y., Engler, D.: A system and language for building system-specific, static analyses. In: Proc. of PLDI 2002, pp. 69\u201382. ACM, New York (2002)"},{"key":"15_CR13","first-page":"57","volume-title":"Proc. of PLDI 2002","author":"M. Das","year":"2002","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. In: Proc. of PLDI 2002, pp. 57\u201368. ACM, New York (2002)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Chen, H., Wagner, D.: Mops: an infrastructure for examining security properties of software. In: Proc. of CCS 2002, pp. 235\u2013244 (2002)","DOI":"10.1145\/586110.586142"},{"key":"15_CR15","doi-asserted-by":"crossref","unstructured":"Erlingsson, U., Schneider, F.B.: SASI enforcement of security policies: A retrospective. In: Proc. of the 1999 New Security Paradigm Workshop (1999)","DOI":"10.1145\/335169.335201"},{"key":"15_CR16","first-page":"254","volume-title":"Proc. of POPL 2000","author":"D. Walker","year":"2000","unstructured":"Walker, D.: A type system for expressive security policies. In: Proc. of POPL 2000, pp. 254\u2013267. ACM, New York (2000)"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-45309-1_5","volume-title":"Programming Languages and Systems","author":"P. Thiemann","year":"2001","unstructured":"Thiemann, P.: Enforcing safety properties using type specialization. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, p. 62. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-40018-9_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:40:07Z","timestamp":1558302007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-40018-9_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540205364","9783540400189"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-40018-9_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003]]}}}