{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:56:35Z","timestamp":1770274595463,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642030123","type":"print"},{"value":"9783642030130","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03013-0_10","type":"book-chapter","created":{"date-parts":[[2009,7,30]],"date-time":"2009-07-30T14:30:01Z","timestamp":1248964201000},"page":"195-219","source":"Crossref","is-referenced-by-count":41,"title":["Practical API Protocol Checking with Access Permissions"],"prefix":"10.1007","author":[{"given":"Kevin","family":"Bierhoff","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nels E.","family":"Beckman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Aldrich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 101\u2013122. Springer, Heidelberg (2001)"},{"issue":"6","key":"10_CR2","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. Journal of Object Technology\u00a03(6), 27\u201356 (2004)","journal-title":"Journal of Object Technology"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Beckman, N.E., Bierhoff, K., Aldrich, J.: Verifying correct usage of Atomic blocks and typestate. In: ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, October 2008, pp. 227\u2013244 (2008)","DOI":"10.1145\/1449764.1449783"},{"key":"10_CR4","first-page":"79","volume-title":"5th International Workshop on Specification and Verification of Component-Based Systems","author":"K. Bierhoff","year":"2006","unstructured":"Bierhoff, K.: Iterator specification with typestates. In: 5th International Workshop on Specification and Verification of Component-Based Systems, pp. 79\u201382. ACM Press, New York (2006)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bierhoff, K.: API Protocol Compliance in Object-Oriented Software. PhD thesis, Carnegie Mellon University, School of Computer Science (April 2009)","DOI":"10.1145\/1449814.1449906"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Lightweight object specification with typestates. In: Joint European Software Engineering Conference and ACM Symposium on the Foundations of Software Engineering, september 2005, pp. 217\u2013226 (2005)","DOI":"10.1145\/1081706.1081741"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Bierhoff, K., Aldrich, J.: Modular typestate checking of aliased objects. In: ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, October 2007, pp. 301\u2013320 (2007)","DOI":"10.1145\/1297027.1297050"},{"key":"10_CR8","unstructured":"Bierhoff, K., Aldrich, J.: Permissions to specify the composite design pattern. In: 7th International Workshop on Specification and Verification of Component-Based Systems (November 2008)"},{"key":"10_CR9","first-page":"971","volume-title":"Companion of the 30th International Conference on Software Engineering","author":"K. Bierhoff","year":"2008","unstructured":"Bierhoff, K., Aldrich, J.: PLURAL: Checking protocol compliance under aliasing. In: Companion of the 30th International Conference on Software Engineering, pp. 971\u2013972. ACM Press, New York (2008)"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Bodden, E., Lam, P., Hendren, L.: Finding programming errors earlier by evaluating runtime monitors ahead-of-time. In: ACM Symposium on the Foundations of Software Engineering, November 2008, pp. 36\u201347 (2008)","DOI":"10.1145\/1453101.1453109"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/3-540-44898-5_4","volume-title":"Static Analysis","author":"J. Boyland","year":"2003","unstructured":"Boyland, J.: Checking interference with fractional permissions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 55\u201372. Springer, Heidelberg (2003)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Boyland, J.T., Retert, W.: Connecting effects and uniqueness with adoption. In: ACM Symposium on Principles of Programming Languages, January 2005, pp. 283\u2013295 (2005)","DOI":"10.1145\/1040305.1040329"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Chin, W.-N., Khoo, S.-C., Qin, S., Popeea, C., Nguyen, H.H.: Verifying safety policies with size properties and alias controls. In: International Conference on Software Engineering, May 2005, pp. 186\u2013195 (2005)","DOI":"10.1145\/1062455.1062500"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1007\/978-3-540-73589-2_26","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"M. Degen","year":"2007","unstructured":"Degen, M., Thiemann, P., Wehr, S.: Tracking linear and affine resources with Java(X). In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 550\u2013574. Springer, Heidelberg (2007)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: ACM Conference on Programming Language Design and Implementation, pp. 59\u201369 (2001)","DOI":"10.1145\/381694.378811"},{"key":"10_CR16","unstructured":"DeLine, R., F\u00e4hndrich, M.: The Fugue protocol checker: Is your software baroque? Technical Report MSR-TR-2004-07, Microsoft Research (2004)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"R. DeLine","year":"2004","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 465\u2013490. Springer, Heidelberg (2004)"},{"key":"10_CR18","first-page":"220","volume-title":"International Conference on Software Engineering","author":"M.B. Dwyer","year":"2007","unstructured":"Dwyer, M.B., Kinneer, A., Elbaum, S.: Adaptive online program analysis. In: International Conference on Software Engineering, pp. 220\u2013229. IEEE Computer Society Press, Los Alamitos (2007)"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Fink, S., Yahav, E., Dor, N., Ramalingam, G., Geay, E.: Effective typestate verification in the presence of aliasing. In: ACM International Symposium on Software Testing and Analysis, July 2006, pp. 133\u2013144 (2006)","DOI":"10.1145\/1146238.1146254"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: ACM Conference on Programming Language Design and Implementation, pp. 1\u201312 (2002)","DOI":"10.1145\/512529.512531"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Haack, C., Hurlin, C.: Resource usage protocols for iterators. In: International Workshop on Aliasing, Confinement and Ownership (July 2008)","DOI":"10.5381\/jot.2009.8.4.a3"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming\u00a08, 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: ACM Symposium on Principles of Programming Languages, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Kobayashi, N.: Resource usage analysis. In: ACM Symposium on Principles of Programming Languages, January 2002, pp. 331\u2013342 (2002)","DOI":"10.1145\/503272.503303"},{"key":"10_CR25","first-page":"83","volume-title":"5th International Workshop on Specification and Verification of Component-Based Systems","author":"N. Krishnaswami","year":"2006","unstructured":"Krishnaswami, N.: Reasoning about iterators with separation logic. In: 5th International Workshop on Specification and Verification of Component-Based Systems, pp. 83\u201386. ACM Press, New York (2006)"},{"issue":"12","key":"10_CR26","doi-asserted-by":"publisher","first-page":"988","DOI":"10.1109\/TSE.2006.125","volume":"32","author":"V. Kuncak","year":"2006","unstructured":"Kuncak, V., Lam, P., Zee, K., Rinard, M.: Modular pluggable analyses for data structure consistency. IEEE Transactions on Software Engineering\u00a032(12), 988\u20131005 (2006)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Boston (1999)"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Livshits, B., Zimmermann, T.: DynaMine: Finding common error patterns by mining software revision histories. In: Joint European Software Engineering Conference and ACM Symposium on the Foundations of Software Engineering, September 2005, pp. 296\u2013305 (2005)","DOI":"10.1145\/1095430.1081754"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Mandelbaum, Y., Walker, D., Harper, R.: An effective theory of type refinements. In: ACM International Conference on Functional Programming, pp. 213\u2013225 (2003)","DOI":"10.1145\/944705.944725"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Naeem, N., Lhot\u00e1k, O.: Typestate-like analysis of multiple interacting objects. In: ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, October 2008, pp. 347\u2013366 (2008)","DOI":"10.1145\/1449955.1449792"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Nanda, M.G., Grothoff, C., Chandra, S.: Deriving object typestates in the presence of inter-object references. In: ACM Conference on Object-Oriented Programming, Systems, Languages & Applications, October 2005, pp. 77\u201396 (2005)","DOI":"10.1145\/1094811.1094818"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: ACM Symposium on Principles of Programming Languages, January 2008, pp. 75\u201386 (2008)","DOI":"10.1145\/1328438.1328451"},{"key":"10_CR33","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"R.E. Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering\u00a012, 157\u2013171 (1986)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10_CR34","first-page":"347","volume-title":"Working Conference on Programming Concepts and Methods","author":"P. Wadler","year":"1990","unstructured":"Wadler, P.: Linear types can change the world? In: Working Conference on Programming Concepts and Methods, pp. 347\u2013359. North-Holland, Amsterdam (1990)"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2009 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03013-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,26]],"date-time":"2023-05-26T05:42:47Z","timestamp":1685079767000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03013-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642030123","9783642030130"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03013-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}