{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:28:35Z","timestamp":1767929315664,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642005893","type":"print"},{"value":"9783642005909","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-00590-9_27","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T08:05:58Z","timestamp":1238141158000},"page":"378-393","source":"Crossref","is-referenced-by-count":87,"title":["A Basis for Verifying Multi-threaded Programs"],"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"}]}],"member":"297","reference":[{"key":"27_CR1","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":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11804192_6","volume-title":"Formal Methods for Components and Objects","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Smallfoot: Modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 115\u2013137. Springer, Heidelberg (2006)"},{"key":"27_CR3","first-page":"259","volume-title":"POPL 2005","author":"R. Bornat","year":"2005","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL 2005, pp. 259\u2013270. ACM, New York (2005)"},{"key":"27_CR4","first-page":"211","volume-title":"OOPSLA 2002","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Lee, R., Rinard, M.C.: Ownership types for safe programming: Preventing data races and deadlocks. In: OOPSLA 2002, pp. 211\u2013230. ACM, New York (2002)"},{"key":"27_CR5","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":"27_CR6","volume-title":"Operating systems principles","author":"P. Brinch Hansen","year":"1973","unstructured":"Brinch Hansen, P.: Operating systems principles. Prentice-Hall, Englewood Cliffs (1973)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"27_CR8","first-page":"213","volume-title":"OOPSLA 2008","author":"D. Distefano","year":"2008","unstructured":"Distefano, D., Parkinson, M.J.: jStar: Towards practical verification of Java. In: OOPSLA 2008, pp. 213\u2013226. ACM, New York (2008)"},{"key":"27_CR9","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":"27_CR10","volume-title":"The Art of Multiprocessor Programming","author":"M. Herlihy","year":"2008","unstructured":"Herlihy, M., Shavit, N.: The Art of Multiprocessor Programming. Morgan Kaufmann, San Francisco (2008)"},{"issue":"10","key":"27_CR11","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"C.A.R. Hoare","year":"1974","unstructured":"Hoare, C.A.R.: Monitors: an operating system structuring concept. Commun. ACM\u00a017(10), 549\u2013557 (1974)","journal-title":"Commun. ACM"},{"key":"27_CR12","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":"27_CR13","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW520, Katholieke Universiteit Leuven (August 2008)"},{"key":"27_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/11901433_23","volume-title":"Formal Methods and Software Engineering","author":"B. Jacobs","year":"2006","unstructured":"Jacobs, B., Smans, J., Piessens, F., Schulte, W.: A statically verifiable programming model for concurrent object-oriented programs. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 420\u2013439. Springer, Heidelberg (2006)"},{"key":"27_CR15","first-page":"321","volume-title":"IFIP Congress","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321\u2013332. North-Holland, Amsterdam (1983)"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"I.T. Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 268\u2013283. Springer, Heidelberg (2006)"},{"key":"27_CR17","volume-title":"Concurrent Programming in Java: Design Principles and Patterns","author":"D. Lea","year":"1999","unstructured":"Lea, D.: Concurrent Programming in Java: Design Principles and Patterns. Addison-Wesley, Reading (1999)"},{"issue":"1\u20133","key":"27_CR18","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. TCS\u00a0375(1\u20133), 271\u2013307 (2007)","journal-title":"TCS"},{"key":"27_CR19","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. FTfJP 2008, Technical Report ICIS-R08013, Radboud University, pp. 1\u201312 (2008)"},{"issue":"4","key":"27_CR20","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1145\/363911.363923","volume":"22","author":"D. Walker","year":"2000","unstructured":"Walker, D., Crary, K., Morrisett, G.: Typed memory management via static capabilities. ACM TOPLAS\u00a022(4), 701\u2013771 (2000)","journal-title":"ACM TOPLAS"},{"issue":"2","key":"27_CR21","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q. Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing\u00a09(2), 149\u2013174 (1997)","journal-title":"Formal Aspects of Computing"},{"key":"27_CR22","unstructured":"Zhao, Y.: Concurrency Analysis based on Fractional Permission System. PhD thesis, The University of Wisconsin\u2013Milwaukee (2007)"}],"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-00590-9_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,7]],"date-time":"2019-03-07T03:12:46Z","timestamp":1551928366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00590-9_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642005893","9783642005909"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00590-9_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}