{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,23]],"date-time":"2026-03-23T13:24:09Z","timestamp":1774272249260,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540311393","type":"print"},{"value":"9783540316220","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11609773_20","type":"book-chapter","created":{"date-parts":[[2005,12,12]],"date-time":"2005-12-12T07:28:57Z","timestamp":1134372537000},"page":"298-312","source":"Crossref","is-referenced-by-count":6,"title":["Resource Usage Analysis for the \u03c0-Calculus"],"prefix":"10.1007","author":[{"given":"Naoki","family":"Kobayashi","sequence":"first","affiliation":[]},{"given":"Kohei","family":"Suenaga","sequence":"additional","affiliation":[]},{"given":"Lucian","family":"Wischik","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24756-2_1","volume-title":"Integrated Formal Methods","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 1\u201320. Springer, Heidelberg (2004)"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: Proc. of POPL, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Chaki, S., Rajamani, S., Rehof, J.: Types as models: Model checking message-passing programs. In: Proc. of POPL, pp. 45\u201357 (2002)","DOI":"10.1145\/503272.503278"},{"issue":"1","key":"20_CR4","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1006\/inco.1996.0072","volume":"129","author":"M. Dam","year":"1996","unstructured":"Dam, M.: Model checking mobile processes. Information and Computation\u00a0129(1), 35\u201351 (1996)","journal-title":"Information and Computation"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: Proc. of PLDI, pp. 59\u201369 (2001)","DOI":"10.1145\/378795.378811"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Adoption and focus: Practical linear types for imperative programming. In: Proc. of PLDI (2002)","DOI":"10.1145\/512529.512532"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. of PLDI, pp. 1\u201312 (2002)","DOI":"10.1145\/512529.512531"},{"issue":"1-3","key":"20_CR8","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0304-3975(03)00325-6","volume":"311","author":"A. Igarashi","year":"2004","unstructured":"Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theor. Comput. Sci.\u00a0311(1-3), 121\u2013163 (2004)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"20_CR9","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1145\/1057387.1057390","volume":"27","author":"A. Igarashi","year":"2005","unstructured":"Igarashi, A., Kobayashi, N.: Resource usage analysis. ACM Trans. Prog. Lang. Syst.\u00a027(2), 264\u2013313 (2005); Preliminary summary appeared in Proceedings of POPL 2002","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"20_CR10","unstructured":"Kobayashi, N.: Type-based information flow analysis for the pi-calculus. In: Acta Informatica (to appear)"},{"key":"20_CR11","unstructured":"Kobayashi, N.: TyPiCal: A type-based static analyzer for the pi-calculus. Tool available at, http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/typical\/"},{"issue":"2","key":"20_CR12","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1145\/276393.278524","volume":"20","author":"N. Kobayashi","year":"1998","unstructured":"Kobayashi, N.: A partially deadlock-free typed process calculus. ACM Trans. Prog. Lang. Syst.\u00a020(2), 436\u2013482 (1998)","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"20_CR13","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1016\/S0890-5401(02)93171-8","volume":"177","author":"N. Kobayashi","year":"2002","unstructured":"Kobayashi, N.: A type system for lock-free processes. Info. Comput.\u00a0177, 122\u2013159 (2002)","journal-title":"Info. Comput."},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/3-540-44618-4_35","volume-title":"CONCUR 2000 - Concurrency Theory","author":"N. Kobayashi","year":"2000","unstructured":"Kobayashi, N., Saito, S., Sumii, E.: An implicitly-typed deadlock-free process calculus. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 489\u2013503. Springer, Heidelberg (2000)"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Kobayashi, N., Suenaga, K., Wischik, L.: Resource usage analysis for the pi-calculus. Full version (2005), http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/papers\/usage-pi.pdf","DOI":"10.2168\/LMCS-2(3:4)2006"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-540-40018-9_15","volume-title":"Programming Languages and Systems","author":"K. Marriott","year":"2003","unstructured":"Marriott, K., Stuckey, P.J., Sulzmann, M.: Resource usage verification. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol.\u00a02895, pp. 212\u2013229. Springer, Heidelberg (2003)"},{"key":"20_CR17","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)"},{"key":"20_CR18","unstructured":"Nguyen, N., Rathke, J.: Typed static analysis for concurrent, policy-based, resource access control. draft"},{"key":"20_CR19","volume-title":"Petri Net Theory and the Modeling of Systems","author":"J.L. Peterson","year":"1981","unstructured":"Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-540-30477-7_8","volume-title":"Programming Languages and Systems","author":"C. Skalka","year":"2004","unstructured":"Skalka, C., Smith, S.: History effects and verification. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol.\u00a03302, pp. 107\u2013128. Springer, Heidelberg (2004)"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-58179-0_73","volume-title":"Computer Aided Verification","author":"B. Victor","year":"1994","unstructured":"Victor, B., Moller, F.: The Mobility Workbench \u2014 a tool for the \u03c0-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 428\u2013440. Springer, Heidelberg (1994)"},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/3-540-36384-X_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Yang","year":"2002","unstructured":"Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the pi-calculus: Model checking mobile processes using tabled resolution. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 116\u2013131. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11609773_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:07:01Z","timestamp":1619507221000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11609773_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540311393","9783540316220"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11609773_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}