{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:29:15Z","timestamp":1767929355706,"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_8","type":"book-chapter","created":{"date-parts":[[2009,7,30]],"date-time":"2009-07-30T10:30:01Z","timestamp":1248949801000},"page":"148-172","source":"Crossref","is-referenced-by-count":85,"title":["Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic"],"prefix":"10.1007","author":[{"given":"Jan","family":"Smans","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","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":"8_CR2","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":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-540-87873-5_16","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A. Banerjee","year":"2008","unstructured":"Banerjee, A., Barnett, M., Naumann, D.A.: Boogie meets regions: a verification experience report. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 177\u2013191. Springer, Heidelberg (2008)"},{"key":"8_CR4","unstructured":"Rustan, K., Leino, M.: Specification and verification of object-oriented software. In: Marktoberdorf International Summer School (2008)"},{"key":"8_CR5","unstructured":"Schoeller, B.: Making Classes Provable through Contracts, Models and Frames. PhD thesis, Departement Informatik ETH Zurich (2007)"},{"key":"8_CR6","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":"8_CR7","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: Combining dynamic frames and separation logic (soundness proof). Technical Report CW542, Katholieke Universiteit Leuven (2009)","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"8_CR8","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":"8_CR9","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":"8_CR10","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":"8_CR11","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":"8_CR12","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Inspector methods for state abstraction. Journal of Object Technology\u00a06(5) (2007)","DOI":"10.5381\/jot.2007.6.5.a1"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Middelkoop, R.: Proving consistency of pure methods and model fields. In: FASE (2009)","DOI":"10.1007\/978-3-642-00593-0_16"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11901433_2","volume-title":"Formal Methods and Software Engineering","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T.: JML\u2019s rich, inherited specifications for behavioral subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol.\u00a04260, pp. 2\u201334. Springer, Heidelberg (2006)"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic, abstraction and inheritance. In: POPL (2008)","DOI":"10.1145\/1328438.1328451"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.: jStar: Towards Practical Verification for Java. In: OOPSLA (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"8_CR18","unstructured":"Parkinson, M.: Local Reasoning for Java. PhD thesis, University of Cambridge (2005)"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: Full functional verification of linked data structures. In: PLDI (2008)","DOI":"10.1145\/1375581.1375624"},{"key":"8_CR20","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":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-27764-4_5","volume-title":"Mathematics of Program Construction","author":"M. Barnett","year":"2004","unstructured":"Barnett, M., Naumann, D.A.: Friends need a bit more: Maintaining invariants over shared state. In: Kozen, D. (ed.) MPC 2004. LNCS, vol.\u00a03125, pp. 54\u201384. Springer, Heidelberg (2004)"},{"key":"8_CR22","unstructured":"Parkinson, M.: Class invariants: The end of the road? In: IWACO (2007)"},{"key":"8_CR23","unstructured":"Leino, K.R.M., Monahan, R.: Automatic verification of textbook programs that use comprehensions. In: FTFJP (2007)"},{"key":"8_CR24","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":"8_CR25","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-540-78163-9_19","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H.H. Nguyen","year":"2008","unstructured":"Nguyen, H.H., Kuncak, V., Chin, W.-N.: Runtime checking for separation logic. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 203\u2013217. Springer, Heidelberg (2008)"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: PLDI (2002)","DOI":"10.1145\/512529.512559"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs. PhD thesis, FernUniversit\u00e4t Hagen (2001)","DOI":"10.1007\/3-540-45651-1"},{"key":"8_CR29","doi-asserted-by":"crossref","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) (2003)","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design (1999)","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS, vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI (2002)","DOI":"10.1145\/512529.512558"},{"key":"8_CR33","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. In: FTFJP (2008)"},{"key":"8_CR34","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)"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T15:52:09Z","timestamp":1558453929000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03013-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642030123","9783642030130"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03013-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}