{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:24:57Z","timestamp":1745994297538},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141065"},{"type":"electronic","value":"9783642141072"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14107-2_8","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T12:10:14Z","timestamp":1277813414000},"page":"151-174","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Executable Object-Oriented Specifications with Separation Logic"],"prefix":"10.1007","author":[{"given":"Stephan","family":"van Staden","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristiano","family":"Calcagno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bertrand","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"ECMA International: Standard ECMA-367. Eiffel: Analysis, Design and Programming Language. 2nd edn. (June 2006)"},{"key":"8_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 2005. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"issue":"3","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes\u00a031(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Van Staden, S., Calcagno, C.: Reasoning about multiple related abstractions with MultiStar. Technical Report 666, ETH Zurich (2010)","DOI":"10.1145\/1869459.1869501"},{"key":"8_CR5","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/1328438.1328451","volume-title":"POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"M.J. Parkinson","year":"2008","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 75\u201386. ACM, New York (2008)"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1145\/1449764.1449782","volume-title":"OOPSLA 2008: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications","author":"D. Distefano","year":"2008","unstructured":"Distefano, D., Parkinson, J., Matthew, J.: jStar: towards practical verification for Java. In: OOPSLA 2008: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications, pp. 213\u2013226. ACM, New York (2008)"},{"key":"8_CR7","unstructured":"Jacobs, B., Smans, J., Piessens, F.: Verifying the composite pattern using separation logic. SAVCBS Composite pattern challenge track (2008)"},{"issue":"3","key":"8_CR8","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","volume":"62","author":"P. M\u00fcller","year":"2006","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Science of Computer Programming\u00a062(3), 253\u2013286 (2006)","journal-title":"Science of Computer Programming"},{"issue":"6","key":"8_CR9","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1002\/spe.649","volume":"35","author":"Y. Cheon","year":"2005","unstructured":"Cheon, Y., Leavens, G., Sitaraman, M., Edwards, S.: Model variables: cleanly supporting abstraction in design by contract: Research articles. Softw. Pract. Exper.\u00a035(6), 583\u2013599 (2005)","journal-title":"Softw. Pract. Exper."},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11786160_3","volume-title":"Architecting Systems with Trustworthy Components","author":"B. Schoeller","year":"2006","unstructured":"Schoeller, B., Widmer, T., Meyer, B.: Making specifications complete through models. In: Reussner, R., Stafford, J.A., Szyperski, C. (eds.) Architecting Systems with Trustworthy Components. LNCS, vol.\u00a03938, pp. 48\u201370. Springer, Heidelberg (2006)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P.W. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"issue":"2:4","key":"8_CR12","first-page":"1","volume":"5","author":"M. Raza","year":"2009","unstructured":"Raza, M., Gardner, P.: Footprints in local reasoning. Logical Methods in Computer Science 5(2:4), 1\u201327 (2009)","journal-title":"Logical Methods in Computer Science"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"LICS 2002: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, Washington, DC, USA, pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"8_CR14","unstructured":"Parkinson, M.J.: Local reasoning for Java. PhD thesis, University of Cambridge, Computer Laboratory. Technical Report UCAM-CL-TR-654 (November 2005)"},{"key":"8_CR15","first-page":"247","volume-title":"POPL 2005: Proceedings of the 32nd annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"M. Parkinson","year":"2005","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL 2005: Proceedings of the 32nd annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 247\u2013258. ACM, New York (2005)"},{"key":"8_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1562154.1562160","volume-title":"IWACO 2009: International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming","author":"A.J. Summers","year":"2009","unstructured":"Summers, A.J., Drossopoulou, S., M\u00fcller, P.: The need for flexible object invariants. In: IWACO 2009: International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming, pp. 1\u20139. ACM, New York (2009)"},{"key":"8_CR17","first-page":"351","volume":"9","author":"K.R.M. Leino","year":"2007","unstructured":"Leino, K.R.M., Schulte, W.: A verifying compiler for a multi-threaded object-oriented language. Software System Reliability and Security\u00a09, 351\u2013416 (2007)","journal-title":"Software System Reliability and Security"},{"issue":"2","key":"8_CR18","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/s00165-007-0026-7","volume":"19","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. Formal Aspects of Computing\u00a019(2), 159\u2013189 (2007)","journal-title":"Formal Aspects of Computing"},{"issue":"6","key":"8_CR19","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1049\/iet-sen:20080011","volume":"2","author":"\u00c1. Darvas","year":"2008","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Faithful mapping of model classes to mathematical structures. IET Software\u00a02(6), 477\u2013499 (2008)","journal-title":"IET Software"},{"issue":"5","key":"8_CR20","doi-asserted-by":"crossref","first-page":"59","DOI":"10.5381\/jot.2006.5.5.a3","volume":"5","author":"A. Darvas","year":"2006","unstructured":"Darvas, A., M\u00fcller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology (JOT)\u00a05(5), 59\u201385 (2006)","journal-title":"Journal of Object Technology (JOT)"},{"issue":"3","key":"8_CR21","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/j.tcs.2007.02.004","volume":"376","author":"D.A. Naumann","year":"2007","unstructured":"Naumann, D.A.: Observational purity and encapsulation. Theor. Comput. Sci.\u00a0376(3), 205\u2013224 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"8_CR22","doi-asserted-by":"crossref","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 (STTT)\u00a07(3), 212\u2013232 (2005)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"8_CR23","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1145\/1328438.1328453","volume-title":"POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"J. Brotherston","year":"2008","unstructured":"Brotherston, J., Bornat, R., Calcagno, C.: Cyclic proofs of program termination in separation logic. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 101\u2013112. ACM, New York (2008)"},{"key":"8_CR24","unstructured":"Van Staden, S.: jStar sources of the examples, http:\/\/se.inf.ethz.ch\/people\/vanstaden\/executablespecs.tgz"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-78739-6_24","volume-title":"Programming Languages and Systems","author":"K.R.M. Leino","year":"2008","unstructured":"Leino, K.R.M., M\u00fcller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 307\u2013321. Springer, Heidelberg (2008)"},{"key":"8_CR26","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/1328438.1328452","volume-title":"POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"W.N. Chin","year":"2008","unstructured":"Chin, W.N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular OO verification with separation logic. In: POPL 2008: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 87\u201399. ACM, New York (2008)"},{"key":"8_CR27","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java modeling language (JML). In: Proceedings of the international conference on Software engineering research and practice (SERP 2002), Las Vegas, pp. 322\u2013328. CSREA Press (2002)"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-540-69507-3_9","volume-title":"SOFSEM 2007: Theory and Practice of Computer Science","author":"B. Meyer","year":"2007","unstructured":"Meyer, B., Ciupa, I., Leitner, A., Liu, L.L.: Automatic testing of object-oriented software. In: van Leeuwen, J., Italiano, G.F., van der Hoek, W., Meinel, C., Sack, H., Pl\u00e1\u0161il, F. (eds.) SOFSEM 2007. LNCS, vol.\u00a04362, pp. 114\u2013129. Springer, Heidelberg (2007)"},{"key":"8_CR29","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/1273463.1273476","volume-title":"ISSTA 2007: Proceedings of the 2007 international symposium on Software testing and analysis","author":"I. Ciupa","year":"2007","unstructured":"Ciupa, I., Leitner, A., Oriol, M., Meyer, B.: Experimental assessment of random testing for object-oriented software. In: ISSTA 2007: Proceedings of the 2007 international symposium on Software testing and analysis, pp. 84\u201394. ACM, New York (2007)"},{"key":"8_CR30","first-page":"289","volume-title":"POPL 2009: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"C. Calcagno","year":"2009","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL 2009: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 289\u2013300. ACM, New York (2009)"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-03237-0_14","volume-title":"Static Analysis","author":"B.S. Gulavani","year":"2009","unstructured":"Gulavani, B.S., Chakraborty, S., Ramalingam, G., Nori, A.V.: Bottom-up shape analysis. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol.\u00a05673, pp. 188\u2013204. Springer, Heidelberg (2009)"},{"key":"8_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-02047-6_4","volume-title":"Object-Oriented Technology. ECOOP 2008 Workshop Reader","author":"D. Clarke","year":"2009","unstructured":"Clarke, D., Drossopoulou, S., M\u00fcller, P., Noble, J., Wrigstad, T.: Aliasing, confinement, and ownership in object-oriented programming (IWACO). In: Eugster, P. (ed.) ECOOP 2008 Workshops. LNCS, vol.\u00a05475, pp. 30\u201341. Springer, Heidelberg (2009)"},{"key":"8_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-540-30579-8_14","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Salcianu","year":"2005","unstructured":"Salcianu, A., Rinard, M.C.: Purity and side effect analysis for Java programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 199\u2013215. Springer, Heidelberg (2005)"},{"key":"8_CR34","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":"A. Darvas","year":"2007","unstructured":"Darvas, A., 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":"8_CR35","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)"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2010 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14107-2_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T14:30:20Z","timestamp":1559226620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14107-2_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141065","9783642141072"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14107-2_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}