{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:10:06Z","timestamp":1775873406111,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642119569","type":"print"},{"value":"9783642119576","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_22","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:55:38Z","timestamp":1267991738000},"page":"407-426","source":"Crossref","is-referenced-by-count":39,"title":["Deadlock-Free Channels and Locks"],"prefix":"10.1007","author":[{"given":"K. Rustan M.","family":"Leino","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Smans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-68863-1_2","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java bytecode. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol.\u00a05051, pp. 2\u201318. Springer, Heidelberg (2008)"},{"key":"22_CR2","volume-title":"Concurrent Programming in ERLANG","author":"J. Armstrong","year":"1996","unstructured":"Armstrong, J., Virding, R., Wikstr\u00f6m, C., Williams, M.: Concurrent Programming in ERLANG, 2nd edn. Prentice Hall, Englewood Cliffs (1996)","edition":"2"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"22_CR4","volume-title":"OOPSLA","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA. ACM, New York (2002)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. Springer, Heidelberg (2003)"},{"key":"22_CR6","volume-title":"PLDI","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI. ACM, New York (2006)"},{"key":"22_CR7","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Research Report 159, Compaq Systems Research Center (1998)"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Aiken, M., Hawblitzel, C., Hodson, O., Hunt, G., Larus, J.R., Levi, S.: Language support for fast and reliable message-based communication in Singularity OS. In: EuroSys (2006)","DOI":"10.1145\/1217935.1217953"},{"key":"22_CR9","volume-title":"POPL","author":"X. Feng","year":"2009","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: POPL. ACM, New York (2009)"},{"key":"22_CR10","volume-title":"PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, ACM, New York (2002)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local reasoning for storable locks and threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-89330-1_13","volume-title":"Programming Languages and Systems","author":"C. Haack","year":"2008","unstructured":"Haack, C., Huisman, M., Hurlin, C.: Reasoning about Java\u2019s reentrant locks. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol.\u00a05356, pp. 171\u2013187. Springer, Heidelberg (2008)"},{"key":"22_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-540-79980-1_16","volume-title":"Algebraic Methodology and Software Technology","author":"C. Haack","year":"2008","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork\/join. In: Meseguer, J., Ro\u015fu, G. (eds.) AMAST 2008. LNCS, vol.\u00a05140, pp. 199\u2013215. Springer, Heidelberg (2008)"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM\u00a021(8) (1978)","DOI":"10.1145\/359576.359585"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Hoare, T., O\u2019Hearn, P.: Separation logic semantics for communicating processes. Electronic Notes on Theoretical Comput. Sci.\u00a0212 (2008)","DOI":"10.1016\/j.entcs.2008.04.050"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems","author":"A. Hobor","year":"2008","unstructured":"Hobor, A., Appel, A.W., Nardelli, F.Z.: Oracle semantics for concurrent separation logic. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 353\u2013367. Springer, Heidelberg (2008)"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Jacobs, B.: A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs. PhD thesis, Katholieke Universiteit Leuven (2007)","DOI":"10.1007\/11901433_23"},{"key":"22_CR18","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (2008)"},{"key":"22_CR19","unstructured":"Kobayashi, N.: Type systems for concurrent programs. In: UNU\/IIST 10th Anniversary Colloquium (2002)"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/11817949_16","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"N. Kobayashi","year":"2006","unstructured":"Kobayashi, N.: A new type system for deadlock-free processes. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 233\u2013247. Springer, Heidelberg (2006)"},{"key":"22_CR21","unstructured":"Korty, J.A.: Sema: A Lint-like tool for analyzing semaphore usage in a multithreaded UNIX kernel. In: Proceedings of the Winter 1989 USENIX Conference. USENIX Association (1989)"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-00590-9_27","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P.: A basis for verifying multi-threaded programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol.\u00a05502, pp. 378\u2013393. Springer, Heidelberg (2009)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design V: FOSAD 2007\/2008\/2009 Tutorial Lectures","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Foundations of Security Analysis and Design V: FOSAD 2007\/2008\/2009 Tutorial Lectures. LNCS, vol.\u00a05705. Springer, Heidelberg (2009)"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Deadlock-free channels and locks (extended version). Technical Report CW573, Department of Computer Science, K.U.Leuven (2010)","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Luecke, G.R., Zou, Y., Coyle, J., Hoekstra, J., Kraeva, M.: Deadlock detection in MPI programs. Concurrency and Computation: Practice and Experience\u00a014(11) (2002)","DOI":"10.1002\/cpe.701"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theoretical Comput. Sci.\u00a0375(1-3) (2007)","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"22_CR27","unstructured":"Pike, R.: Newsqueak: A language for communicating with mice. Computing Science Technical Report 143, AT&T Bell Laboratories (1989)"},{"key":"22_CR28","doi-asserted-by":"crossref","unstructured":"Pym, D.J., Tofts, C.M.N.: A calculus and logic of resources and processes. Formal Aspects of Computing\u00a018(4) (2006)","DOI":"10.1007\/s00165-006-0018-z"},{"key":"22_CR29","unstructured":"Ritchie, D.M.: The Limbo programming language. In: Inferno Programmer\u2019s Manual, vol.\u00a02. Vita Nuova Holdings Ltd. (2000)"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-03013-0_8","volume-title":"ECOOP 2009 \u2013 Object-Oriented Programming","author":"J. Smans","year":"2009","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic. In: Drossopoulou, S. (ed.) ECOOP 2009 \u2013 Object-Oriented Programming. LNCS, vol.\u00a05653, pp. 148\u2013172. Springer, Heidelberg (2009)"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78739-6_22","volume-title":"Programming Languages and Systems","author":"T. Terauchi","year":"2008","unstructured":"Terauchi, T., Megacz, A.: Inferring channel buffer bounds via linear programming. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960. Springer, Heidelberg (2008)"},{"key":"22_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/978-3-540-28644-8_32","volume-title":"CONCUR 2004 - Concurrency Theory","author":"V.T. Vasconcelos","year":"2004","unstructured":"Vasconcelos, V.T., Ravara, A., Gay, S.J.: Session types for functional multithreading. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 497\u2013511. Springer, Heidelberg (2004)"},{"key":"22_CR34","volume-title":"Proceedings of the 2000 ACM\/IEEE conference on Supercomputing","author":"J.S. Vetter","year":"2000","unstructured":"Vetter, J.S., de Supinski, B.R.: Dynamic software testing of MPI applications with umpire. In: Proceedings of the 2000 ACM\/IEEE conference on Supercomputing. IEEE, Los Alamitos (2000)"},{"key":"22_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/978-3-642-10672-9_15","volume-title":"APLAS 2009","author":"J. Villard","year":"2009","unstructured":"Villard, J., Lozes, \u00c9., Calcagno, C.: Proving copyless message passing. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 194\u2013209. Springer, Heidelberg (2009)"},{"key":"22_CR36","unstructured":"Winterbottom, P.: Alef language reference manual. In: Plan 9 Programmer\u2019s Manual: Volume Two. AT&T Bell Laboratories (1995)"}],"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-642-11957-6_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:45:44Z","timestamp":1606167944000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}