{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:22:28Z","timestamp":1725556948809},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642134630"},{"type":"electronic","value":"9783642134647"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13464-7_14","type":"book-chapter","created":{"date-parts":[[2010,6,7]],"date-time":"2010-06-07T06:50:49Z","timestamp":1275893449000},"page":"170-185","source":"Crossref","is-referenced-by-count":7,"title":["Heap-Dependent Expressions in 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":"14_CR1","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. Behavioral Specifications of Businesses and Systems (1999)","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"14_CR3","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"key":"14_CR5","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":"14_CR6","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":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_16","volume-title":"Fundamental Approaches to Software Engineering","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M., Middelkoop, R.: Practical reasoning about invocations and implementations of pure methods. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503. Springer, Heidelberg (2009)"},{"key":"14_CR8","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":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/978-3-540-71289-3_26","volume-title":"Fundamental Approaches to Software Engineering","author":"\u00c1. Darvas","year":"2007","unstructured":"Darvas, \u00c1., Leino, K.R.M.: Practical reasoning about invocations and implementations of pure methods. In: Dwyer, M.B., Lopes, A. (eds.) FASE 2007. LNCS, vol.\u00a04422, pp. 336\u2013351. Springer, Heidelberg (2007)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Automatic verification of java programs with dynamic frames. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, Springer, Heidelberg (2008)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology\u00a05(5) (2006)","DOI":"10.5381\/jot.2006.5.5.a3"},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"Distefano, D., Parkinson, M.: jStar: Towards practical verification for Java. In: OOPSLA (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"14_CR13","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (2008)"},{"key":"14_CR14","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":"14_CR15","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":"14_CR16","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Foundations of Augmented Cognition","author":"G.T. Leavens","year":"2007","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. In: Schmorrow, D.D., Reeves, L.M. (eds.) HCII 2007 and FAC 2007. LNCS (LNAI), vol.\u00a04565. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13464-7_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:38:16Z","timestamp":1606167496000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13464-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642134630","9783642134647"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13464-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}