{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:38:10Z","timestamp":1770295090316,"version":"3.49.0"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The magic wand<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathbin {-\\!\\!*}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mo>-<\/mml:mo><mml:mspace\/><mml:mspace\/><mml:mrow\/><mml:mo>\u2217<\/mml:mo><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>(also called separating implication) is a separation logic connective commonly used to specify properties of partial data structures, for instance during iterative traversals. A<jats:italic>footprint<\/jats:italic>of a magic wand formula \"Equation missing\"is a state that, combined with any state in which<jats:italic>A<\/jats:italic>holds, yields a state in which<jats:italic>B<\/jats:italic>holds. The key challenge of proving a magic wand (also called<jats:italic>packaging<\/jats:italic>a wand) is to find such a footprint. Existing package algorithms either have a high annotation overhead or, as we show in this paper, are unsound.<\/jats:p><jats:p>We present a formal framework that precisely characterises a wide design space of possible package algorithms applicable to a large class of separation logics. We prove in Isabelle\/HOL that our formal framework is sound and complete, and use it to develop a novel package algorithm that offers competitive automation and is sound. Moreover, we present a novel, restricted definition of wands and prove in Isabelle\/HOL that it is possible to soundly combine fractions of such wands, which is not the case for arbitrary wands. We have implemented our techniques for the Viper language, and demonstrate that they are effective in practice.<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_7","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"130-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Sound Automation of Magic Wands"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2719-4856","authenticated-orcid":false,"given":"Thibault","family":"Dardinier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gaurav","family":"Parthasarathy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"No\u00e9","family":"Weeks","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5554-9381","authenticated-orcid":false,"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging Rust types for modular specification and verification. In: OOPSLA (2019)","DOI":"10.1145\/3360573"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"issue":"6","key":"7_CR3","doi-asserted-by":"publisher","first-page":"757","DOI":"10.1007\/s10009-015-0372-3","volume":"17","author":"S Blom","year":"2015","unstructured":"Blom, S., Huisman, M.: Witnessing the elimination of magic wands. Int. J. Softw. Tools Technol. Transfer 17(6), 757\u2013781 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0372-3","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"7_CR4","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. 2694, pp. 55\u201372. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44898-5_4"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Boyland, J.T.: Semantics of fractional permissions with nesting. TOPLAS 32(6), 1\u201333 (2010)","DOI":"10.1145\/1749608.1749611"},{"key":"7_CR6","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1016\/j.ic.2011.12.003","volume":"211","author":"R Brochenin","year":"2012","unstructured":"Brochenin, R., Demri, S., Lozes, E.: On the almighty wand. Inf. Comput. 211, 106\u2013137 (2012)","journal-title":"Inf. Comput."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-030-53291-8_13","volume-title":"Computer Aided Verification","author":"J Brotherston","year":"2020","unstructured":"Brotherston, J., Costa, D., Hobor, A., Wickerson, J.: Reasoning over permissions regions in concurrent separation logic. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 203\u2013224. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_13"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Calcagno, C., O\u2019Hearn, P.W., Yang, H.: Local action and abstract separation logic. In: LICS (2007)","DOI":"10.1109\/LICS.2007.30"},{"key":"7_CR9","unstructured":"Cao, Q., Wang, S., Hobor, A., Appel, A.W.: Proof pearl: magic wand as frame (2019). https:\/\/arxiv.org\/abs\/1909.08789"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Chang, B.E., Rival, X.: Relational inductive shape analysis. In: POPL (2008)","DOI":"10.1145\/1328438.1328469"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-74061-2_24","volume-title":"Static Analysis","author":"B-YE Chang","year":"2007","unstructured":"Chang, B.-Y.E., Rival, X., Necula, G.C.: Shape analysis with structural invariant checkers. In: Nielson, H.R., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 384\u2013401. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-74061-2_24"},{"key":"7_CR12","unstructured":"Coq Development Team, T.: The Coq Reference Manual, version 8.10 (2019). Available electronically at http:\/\/coq.inria.fr\/documentation"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Dardinier, T.: Formalization of a framework for the sound automation of magic wands. AFP, May 2022. https:\/\/isa-afp.org\/entries\/Package_logic.html","DOI":"10.1007\/978-3-031-13188-2_7"},{"key":"7_CR14","unstructured":"Dardinier, T.: A restricted definition of the magic wand to soundly combine fractions of a wand. AFP, May 2022. https:\/\/isa-afp.org\/entries\/Combinable_Wands.html"},{"key":"7_CR15","doi-asserted-by":"publisher","unstructured":"Dardinier, T., Parthasarathy, G., Weeks, N., M\u00fcller, P., Summers, A.J.: Sound automation of magic wands (artifact) (2022). https:\/\/doi.org\/10.5281\/zenodo.6526611","DOI":"10.5281\/zenodo.6526611"},{"key":"7_CR16","unstructured":"Dardinier, T., Parthasarathy, G., Weeks, N., Summers, A.J., M\u00fcller, P.: Sound automation of magic wands (extended version) (2022). https:\/\/arxiv.org\/abs\/2205.11325"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-14107-2_24","volume-title":"ECOOP 2010 \u2013 Object-Oriented Programming","author":"T Dinsdale-Young","year":"2010","unstructured":"Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M.J., Vafeiadis, V.: Concurrent abstract predicates. In: D\u2019Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 504\u2013528. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14107-2_24"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-662-54434-1_16","volume-title":"Programming Languages and Systems","author":"T Dinsdale-Young","year":"2017","unstructured":"Dinsdale-Young, T., da Rocha Pinto, P., Andersen, K.J., Birkedal, L.: Caper. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 420\u2013447. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_16"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-642-10672-9_13","volume-title":"Programming Languages and Systems","author":"R Dockins","year":"2009","unstructured":"Dockins, R., Hobor, A., Appel, A.W.: A fresh look at separation algebras and share accounting. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 161\u2013177. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10672-9_13"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Dodds, M., Jagannathan, S., Parkinson, M.J.: Modular reasoning for deterministic parallelism. In: POPL (2011)","DOI":"10.1145\/1926385.1926416"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Haack, C., Hurlin, C.: Resource usage protocols for iterators. JOT 8(4), 55\u201383 (2009)","DOI":"10.5381\/jot.2009.8.4.a3"},{"issue":"6","key":"7_CR22","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-015-0396-8","volume":"17","author":"M Huisman","year":"2015","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012 - a program verification competition. STTT 17(6), 647\u2013657 (2015)","journal-title":"STTT"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL (2011)","DOI":"10.1145\/1926385.1926417"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: NFM (2011)","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"7_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.5381\/jot.2011.10.1.a2","volume":"10","author":"J Jensen","year":"2011","unstructured":"Jensen, J., Birkedal, L., Sestoft, P.: Modular verification of linked lists with views via separation logic. JOT 10, 1\u201320 (2011)","journal-title":"JOT"},{"key":"7_CR26","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. JFP 28, e20 (2018)","journal-title":"JFP"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Krebbers, R., et al.: MoSeL: a general, extensible modal framework for interactive proofs in separation logic. In: ICFP (2018)","DOI":"10.1145\/3236772"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R.: Reasoning about iterators with separation logic. In: SAVCBS (2006)","DOI":"10.1145\/1181195.1181213"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-319-89884-1_14","volume-title":"Programming Languages and Systems","author":"X-B Le","year":"2018","unstructured":"Le, X.-B., Hobor, A.: Logical reasoning for disjoint permissions. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 385\u2013414. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_14"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Lee, W., Park, S.: A proof system for separation logic with magic wand. In: POPL (2014)","DOI":"10.1145\/2535838.2535871"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/978-3-642-03829-7_7","volume-title":"Foundations of Security Analysis and Design V","author":"KRM Leino","year":"2009","unstructured":"Leino, K.R.M., M\u00fcller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 195\u2013222. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_7"},{"key":"7_CR32","unstructured":"Leino, K.R.M.: This is Boogie 2, June 2008. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Maeda, T., Sato, H., Yonezawa, A.: Extended alias type system using separating implication. In: TLDI (2011)","DOI":"10.1145\/1929553.1929559"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-662-49122-5_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P M\u00fcller","year":"2016","unstructured":"M\u00fcller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41\u201362. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2"},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL (2005)","DOI":"10.1145\/1040305.1040326"},{"key":"7_CR36","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/978-3-642-35182-2_8","DOI":"10.1007\/978-3-642-35182-2_8"},{"key":"7_CR37","doi-asserted-by":"publisher","unstructured":"Piskac, R., Wies, T., Zufferey, D.: GRASShopper\u2013complete heap verification with mixed specifications. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 124\u2013139. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_9","DOI":"10.1007\/978-3-642-54862-8_9"},{"key":"7_CR38","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002)"},{"key":"7_CR39","unstructured":"Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. In: ECOOP (2015)"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames: combining dynamic frames and separation logic. In: ECOOP (2009)","DOI":"10.1007\/978-3-642-03013-0_8"},{"key":"7_CR41","unstructured":"Tuerk, T.: Local reasoning about while-loops. In: VS-Theory (2010)"},{"key":"7_CR42","unstructured":"Yang, H.: An example of local reasoning in bi pointer logic: the Schorr-Waite graph marking algorithm. In: SPACE (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,13]],"date-time":"2023-02-13T19:24:40Z","timestamp":1676316280000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}