{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,24]],"date-time":"2024-07-24T23:09:48Z","timestamp":1721862588641},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2015,3,31]],"date-time":"2015-03-31T00:00:00Z","timestamp":1427760000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,11]]},"DOI":"10.1007\/s10009-015-0372-3","type":"journal-article","created":{"date-parts":[[2015,3,30]],"date-time":"2015-03-30T06:53:36Z","timestamp":1427698416000},"page":"757-781","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Witnessing the elimination of magic wands"],"prefix":"10.1007","volume":"17","author":[{"given":"Stefan","family":"Blom","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,3,31]]},"reference":[{"key":"372_CR1","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Logic in Computer Science, pp. 55\u201374. IEEE Computer Society, Washington, DC (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"372_CR2","doi-asserted-by":"crossref","unstructured":"Blom, S., Huisman, M.: The VerCors tool for verification of concurrent programs. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM. Lecture Notes in Computer Science, vol. 8442, pp. 127\u2013131. Springer (2014)","DOI":"10.1007\/978-3-319-06410-9_9"},{"issue":"10","key":"372_CR3","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"issue":"1","key":"372_CR4","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/2160910.2160911","volume":"34","author":"J Smans","year":"2012","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. ACM Trans. Program. Lang. Syst. 34(1), 2 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3:01","key":"372_CR5","first-page":"1","volume":"8","author":"MJ Parkinson","year":"2012","unstructured":"Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. Log. Methods Comput. Sci. 8(3:01), 1\u201354 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"372_CR6","doi-asserted-by":"crossref","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, pp. 247\u2013258. ACM, New York (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"372_CR7","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis verification competition 2012\u2014organizer\u2019s report. In: Technical Report 2013-01, Department of Informatics, Karlsruhe Institute of Technology (2013). http:\/\/digbib.ubka.uni-karlsruhe.de\/volltexte\/1000034373"},{"key":"372_CR8","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. In: Gordon, A.D. (ed.) ESOP. Lecture Notes in Computer Science, vol. 6012, pp. 85\u2013103. Springer, New York(2010)","DOI":"10.1007\/978-3-642-11957-6_6"},{"issue":"4","key":"372_CR9","doi-asserted-by":"crossref","first-page":"55","DOI":"10.5381\/jot.2009.8.4.a3","volume":"8","author":"C Haack","year":"2009","unstructured":"Haack, C., Hurlin, C.: Resource usage protocols for iterators. J. Object Technol. 8(4), 55\u201383 (2009)","journal-title":"J. Object Technol."},{"key":"372_CR10","doi-asserted-by":"crossref","unstructured":"Hobor, A., Villard, J.: The ramifications of sharing in data structures. In Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 523\u2013536. ACM, New York (2013)","DOI":"10.1145\/2429069.2429131"},{"key":"372_CR11","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R., Aldrich, J., Birkedal, L., Svendsen, K., Buisse, A.: Design patterns in separation logic. In: Kennedy, A., Ahmed, A. (eds.) TLDI, pp. 105\u2013116. ACM, New York (2009)","DOI":"10.1145\/1481861.1481874"},{"key":"372_CR12","doi-asserted-by":"crossref","unstructured":"Maeda, T., Sato, H., Yonezawa, A.: Extended alias type system using separating implication. In: Proceedings of the 7th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI \u201911, pp. 29\u201342. ACM, New York (2011)","DOI":"10.1145\/1929553.1929559"},{"key":"372_CR13","unstructured":"Jacobs, B., Smans, J., Piessens, F.: VeriFast: imperative programs as proofs. In: VSTTE Workshop on Tools & Experiments (2010)"},{"key":"372_CR14","doi-asserted-by":"crossref","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. Lecture Notes in Computer Science, vol. 4111, pp. 115\u2013137. Springer, New York (2005)","DOI":"10.1007\/11804192_6"},{"key":"372_CR15","doi-asserted-by":"crossref","unstructured":"DiStefano, D., Parkinson, M.: jStar: towards practical verification for Java. In: ACM Conference on Object-Oriented Programming Systems, Languages, and Applications, pp. 213\u2013226. ACM Press, New York (2008)","DOI":"10.1145\/1449764.1449782"},{"key":"372_CR16","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. In: Technical Report CW520, Katholieke Universiteit Leuven (2008)"},{"key":"372_CR17","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Lecture Notes of FOSAD. LNCS, vol. 5705, pp. 195\u2013222. Springer, New York (2009)","DOI":"10.1007\/978-3-642-03829-7_7"},{"key":"372_CR18","doi-asserted-by":"crossref","unstructured":"Heule, S., Kassios, I.T., M\u00fcller, P., Summers, A.J.: Verification condition generation for permission logics with abstract predicates and abstraction functions. In: Castagna, G. (ed.) ECOOP. Lecture Notes in Computer Science, vol. 7920, pp. 451\u2013476. Springer, New York (2013)","DOI":"10.1007\/978-3-642-39038-8_19"},{"key":"372_CR19","first-page":"196","volume-title":"VSTTE. Lecture Notes in Computer Science, vol. 7152","author":"Ioannis T Kassios","year":"2012","unstructured":"Kassios, Ioannis T., M\u00fcller, Peter, Schwerhoff, Malte: Comparing verification condition generation with symbolic execution: an experience report. In: Joshi, Rajeev, M\u00fcller, Peter, Podelski, Andreas (eds.) VSTTE. Lecture Notes in Computer Science, vol. 7152, pp. 196\u2013208. Springer, New York (2012)"},{"key":"372_CR20","unstructured":"Chair of Programming Methodology, ETH Z\u00fcrich: Viper project website. http:\/\/www.pm.inf.ethz.ch\/research\/viper"},{"key":"372_CR21","unstructured":"Juhasz, U., Kassios, I.T., M\u00fcller, P., Novacek, M., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Technical report, ETH Zurich (2014)"},{"key":"372_CR22","unstructured":"Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. In: Technical Report. ETH, Z\u00fcrich (2014)"},{"key":"372_CR23","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1016\/j.ic.2011.12.003","volume":"211","author":"R Brochenin","year":"2012","unstructured":"Brochenin, R., Demri, S., Lozes, \u00c9.: On the almighty wand. Inf. Comput. 211, 106\u2013137 (2012)","journal-title":"Inf. Comput."},{"key":"372_CR24","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D.R., M\u00fcller, P., Kiniry, J., Chalin, P.: JML Reference Manual, February 2007. Department of Computer Science, Iowa State University. http:\/\/www.jmlspecs.org (2007)"},{"key":"372_CR25","doi-asserted-by":"crossref","unstructured":"Jost, D., Summers, A.J.: An automatic encoding from VeriFast predicates into implicit dynamic frames. In: Verified Software: Theories, Tools and Experiments (VSTTE) (2013)","DOI":"10.1007\/978-3-642-54108-7_11"},{"key":"372_CR26","unstructured":"Howard, W.: The formulae-as-types notion of construction, pp. 479\u2013490. ACM, New York (1980) (original paper manuscript from 1969)"},{"key":"372_CR27","unstructured":"Reynolds, J.C.: Lecture Notes for the FIRST PhD Fall School on Logics and Semantics of State. ITU University, Copenhagen (2008)"},{"key":"372_CR28","first-page":"378","volume-title":"ESOP. Lecture Notes in Computer Science, vol. 5502","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P.: A basis for verifying multi-threaded programs. In: Castagna, Giuseppe (ed.) ESOP. Lecture Notes in Computer Science, vol. 5502, pp. 378\u2013393. Springer, New York (2009)"},{"key":"372_CR29","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In LICS, pp. 366\u2013378. IEEE Computer Society, Washington, DC (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"372_CR30","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: Necula, G.C., Wadler, P. (eds.) POPL, pp. 75\u201386 (2008). ACM, New York","DOI":"10.1145\/1328438.1328451"},{"key":"372_CR31","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-540-79980-1_16","volume-title":"Algebraic Methodology and Software Technology. LNCS, vol. 5140","author":"C Haack","year":"2008","unstructured":"Haack, C., Hurlin, C.: Separation logic contracts for a Java-like language with fork\/join. In: Meseguer, J., Rosu, G. (eds.) Algebraic Methodology and Software Technology. LNCS, vol. 5140, pp. 199\u2013215. Springer, New York (2008)"},{"key":"372_CR32","unstructured":"Hurlin, C.: Specification and Verification of Multithreaded Object-Oriented Programs with Separation Logic. Ph.D. thesis, Universit\u00e9 Nice Sophia Antipolis (2009)"},{"key":"372_CR33","doi-asserted-by":"crossref","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: Formal Methods for Components and Objects. LNCS, vol. 4111, pp. 364\u2013387. Springer, New York (2005)","DOI":"10.1007\/11804192_17"},{"key":"372_CR34","doi-asserted-by":"crossref","unstructured":"Mendon\u00e7a de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS. LNCS, vol. 4963, pp. 337\u2013340. Springer, New York (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"372_CR35","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C.. O\u2019Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In Palsberg J, Abadi M (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259\u2013270. ACM, New York (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"372_CR36","unstructured":"The VerCors tool online. http:\/\/www.utwente.nl\/vercors\/ (2014)"},{"key":"372_CR37","first-page":"29","volume-title":"VSTTE 2010. Workshop Proceedings","author":"T T\u00fcrk","year":"2010","unstructured":"T\u00fcrk, T.: Local reasoning about while-loops. In: Joshi, R., Margaria, T., M\u00fcller, P., Naumann, D., Yang, H. (eds.) VSTTE 2010. Workshop Proceedings, pp. 29\u201339. ETH, Z\u00fcrich (2010)"},{"key":"372_CR38","first-page":"384","volume-title":"VSTTE. Lecture Notes in Computer Science, vol. 4171","author":"ECR Hehner","year":"2005","unstructured":"Hehner, E.C.R.: Specified blocks. In: Meyer, B., Woodcock, J. (eds.) VSTTE. Lecture Notes in Computer Science, vol. 4171, pp. 384\u2013391. Springer, New York (2005)"},{"key":"372_CR39","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV. Lecture Notes in Computer Science, vol. 4590, pp. 173\u2013177. Springer, New York (2007)","DOI":"10.1007\/978-3-540-73368-3_21"},{"issue":"5","key":"372_CR40","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"GP Huet","year":"1997","unstructured":"Huet, G.P.: The Zipper. J. Funct. Program. 7(5), 549\u2013554 (1997)","journal-title":"J. Funct. Program."},{"key":"372_CR41","unstructured":"Botin\u010dan, M., Distefano, D., Dodds, M., Grigore, R., Parkinson, M.J.: Corestar: the core of jstar. In: Boogie. CiteSeer, Princeton (2011)"},{"key":"372_CR42","doi-asserted-by":"crossref","unstructured":"Park, J., Seo, J., Park, S.: A theorem prover for boolean BI. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 219\u2013232 (2013)","DOI":"10.1145\/2429069.2429095"},{"issue":"4","key":"372_CR43","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1023\/A:1010027404223","volume":"11","author":"JC Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. High. Order Symb. Comput. 11(4), 363\u2013397 (1998)","journal-title":"High. Order Symb. Comput."},{"issue":"6","key":"372_CR44","doi-asserted-by":"crossref","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27\u201356 (2004)","journal-title":"J. Object Technol."},{"key":"372_CR45","doi-asserted-by":"crossref","unstructured":"Ferrara, P., M\u00fcller, P.: Automatic inference of access permissions. In: Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2012). LNCS, pp. 202\u2013218. Springer, New York (2012)","DOI":"10.1007\/978-3-642-27940-9_14"},{"issue":"6","key":"372_CR46","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1145\/2049697.2049700","volume":"58","author":"C Calcagno","year":"2011","unstructured":"Calcagno, C., Distefano, D., O\u2019Hearn, P.W., Yang, H.: Compositional shape analysis by means of bi-abduction. J. ACM 58(6), 26 (2011)","journal-title":"J. ACM"},{"key":"372_CR47","unstructured":"Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201913, Rome, 23\u201325 January 2013. ACM, New York (2013)"},{"key":"372_CR48","unstructured":"Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, 12\u201314 January 2005. ACM, New York (2005)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0372-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0372-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0372-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T16:26:01Z","timestamp":1566491161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0372-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,31]]},"references-count":48,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11]]}},"alternative-id":["372"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0372-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,31]]}}}