{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:48:11Z","timestamp":1777348091572,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642038280","type":"print"},{"value":"9783642038297","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-03829-7_7","type":"book-chapter","created":{"date-parts":[[2009,8,10]],"date-time":"2009-08-10T05:05:20Z","timestamp":1249880720000},"page":"195-222","source":"Crossref","is-referenced-by-count":56,"title":["Verification of Concurrent Programs with Chalice"],"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":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11808107_4","volume-title":"Dependable Systems: Software, Computing, Networks","author":"V. Arslan","year":"2006","unstructured":"Arslan, V., Eugster, P.T., Nienaltowski, P., Vaucouleur, S.: SCOOP \u2013 concurrency made easy. In: Kohlas, J., Meyer, B., Schiper, A. (eds.) Dependable Systems: Software, Computing, Networks. LNCS, vol.\u00a04028, pp. 82\u2013102. Springer, Heidelberg (2006)"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-70592-5_17","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"A. Banerjee","year":"2008","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Regional logic for local reasoning about global invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol.\u00a05142, pp. 387\u2013411. Springer, Heidelberg (2008)"},{"key":"7_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":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"7_CR5","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":"7_CR6","first-page":"211","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002","author":"C. Boyapati","year":"2002","unstructured":"Boyapati, C., Lee, R., Rinard, M.: Ownership types for safe programming: Preventing data races and deadlocks. In: Proceedings of the 2002 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA 2002, pp. 211\u2013230. ACM, New York (2002)"},{"key":"7_CR7","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)"},{"issue":"3","key":"7_CR8","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"TPHOLs 2009","author":"E. Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moska\u0142, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"7_CR10","unstructured":"Cunningham, D., Drossopoulou, S., Eisenbach, S.: Universe types for race safety. In: Proceedings of the 1st Workshop on Verification and Analysis of Multi-threaded Java-like Programs (VAMP), number ICIS-R07021 in Technical Report, pp. 20\u201351. Radboud University Nijmegen (September 2007)"},{"key":"7_CR11","volume-title":"Concurrency Verification","author":"W.-P. Roever de","year":"2001","unstructured":"de Roever, W.-P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Zwiers, J.: Concurrency Verification. Cambridge University Press, Cambridge (2001)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-73589-2_3","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"W. Dietl","year":"2007","unstructured":"Dietl, W., Drossopoulou, S., M\u00fcller, P.: Generic universe types. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol.\u00a04609, pp. 28\u201353. Springer, Heidelberg (2007)"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"E.W. Dijkstra","year":"1971","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informatica\u00a01, 115\u2013138 (1971)","journal-title":"Acta Informatica"},{"key":"7_CR14","series-title":"SIGPLAN Notices","first-page":"213","volume-title":"Object-Oriented Programming Systems, Languages and Applications (OOPSLA)","author":"D. Distefano","year":"2008","unstructured":"Distefano, D., Parkinson, M.J.: jStar: Towards practical verification of Java. In: Harris, G.E. (ed.) Object-Oriented Programming Systems, Languages and Applications (OOPSLA). SIGPLAN Notices, vol.\u00a037(11), pp. 213\u2013226. ACM, New York (2008)"},{"key":"7_CR15","first-page":"315","volume-title":"Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"X. Feng","year":"2009","unstructured":"Feng, X.: Local rely-guarantee reasoning. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 315\u2013327. ACM, New York (2009)"},{"key":"7_CR16","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (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: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 234\u2013245. ACM, New York (2002)"},{"key":"7_CR17","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":"7_CR18","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":"7_CR19","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)"},{"issue":"10","key":"7_CR20","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. Communications of the ACM\u00a017(10), 549\u2013557 (1974)","journal-title":"Communications of the ACM"},{"key":"7_CR21","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":"7_CR22","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Leino, K.R.M., Piessens, F., Schulte, W., Smans, J.: A programming model for concurrent object-oriented programs. ACM Transactions on Programming Languages and Systems\u00a031(1) (December 2008)","DOI":"10.1145\/1452044.1452045"},{"key":"7_CR23","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (August 2008)"},{"key":"7_CR24","first-page":"321","volume-title":"Proceedings of IFIP 1983","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. In: Proceedings of IFIP 1983, pp. 321\u2013332. North-Holland, Amsterdam (1983)"},{"key":"7_CR25","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":"7_CR26","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, Dordrecht (1999)"},{"key":"7_CR27","unstructured":"Leino, K.R.M.: Toward Reliable Modular Programs. PhD thesis, California Institute of Technology, Technical Report Caltech-CS-TR-95-03 (1995)"},{"key":"7_CR28","series-title":"NATO Security Through Science Series; Sub-Series D","first-page":"231","volume-title":"Engineering Methods and Tools for Software Safety and Security","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. In: Engineering Methods and Tools for Software Safety and Security. NATO Security Through Science Series; Sub-Series D, vol.\u00a022, pp. 231\u2013266. IOS Press, Amsterdam (2009)"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/978-3-642-00593-0_16","volume-title":"FASE 2009","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M., Middelkoop, R.: Proving consistency of pure methods and model fields. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 231\u2013245. Springer, Heidelberg (2009)"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"K.R.M. Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol.\u00a03086, pp. 491\u2013515. Springer, Heidelberg (2004)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-642-00590-9_27","volume-title":"ESOP 2009","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)"},{"issue":"5","key":"7_CR32","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1145\/570886.570888","volume":"24","author":"K.R.M. Leino","year":"2002","unstructured":"Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Transactions on Programming Languages and Systems\u00a024(5), 491\u2013553 (2002)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR33","unstructured":"Musuvathi, M., Qadeer, S., Ball, T., Basler, G., Nainar, P.A., Neamtiu, I.: Finding and reproducing Heisenbugs in concurrent programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 2008, pp. 267\u2013280. USENIX Association (2008)"},{"issue":"1-3","key":"7_CR34","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. Theoretical Computer Science\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"issue":"5","key":"7_CR35","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. Communications of the ACM\u00a019(5), 279\u2013285 (1976)","journal-title":"Communications of the ACM"},{"key":"7_CR36","first-page":"247","volume-title":"Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005","author":"M.J. Parkinson","year":"2005","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic and abstraction. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp. 247\u2013258. ACM, New York (2005)"},{"key":"7_CR37","unstructured":"Parkinson, M.J.: Local Reasoning for Java. PhD thesis. University of Cambridge (2005)"},{"key":"7_CR38","first-page":"55","volume-title":"17th IEEE Symposium on Logic in Computer Science (LICS 2002)","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55\u201374. IEEE, Los Alamitos (2002)"},{"key":"7_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-540-68237-0_7","volume-title":"FM 2008: Formal Methods","author":"A. Rudich","year":"2008","unstructured":"Rudich, A., Darvas, \u00c1., M\u00fcller, P.: Checking well-formedness of pure-method specifications. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 68\u201383. Springer, Heidelberg (2008)"},{"key":"7_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-642-03013-0_8","volume-title":"ECOOP 2009","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. LNCS, vol.\u00a05653, pp. 148\u2013172. Springer, Heidelberg (2009)"},{"key":"7_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-540-78743-3_19","volume-title":"Fundamental Approaches to Software Engineering","author":"J. Smans","year":"2008","unstructured":"Smans, J., Jacobs, B., Piessens, F., Schulte, W.: An automatic verifier for java-like programs based on dynamic frames. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 261\u2013275. Springer, Heidelberg (2008)"},{"key":"7_CR42","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":"7_CR43","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/1375581.1375624","volume-title":"Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp. 349\u2013361. ACM, New York (2008)"}],"container-title":["Lecture Notes in Computer Science","Foundations of Security Analysis and Design V"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03829-7_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:11:00Z","timestamp":1558267860000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03829-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642038280","9783642038297"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03829-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}