{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T13:57:54Z","timestamp":1775743074533,"version":"3.50.1"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T00:00:00Z","timestamp":1720483200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T00:00:00Z","timestamp":1720483200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62172217"],"award-info":[{"award-number":["62172217"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61902180"],"award-info":[{"award-number":["61902180"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Natural Science Foundation of China and the Civil Aviation Administration of China","award":["U1533130"],"award-info":[{"award-number":["U1533130"]}]},{"DOI":"10.13039\/501100022210","name":"National Satellite of Excellence in Trustworthy Software Systems, National University of Singapore","doi-asserted-by":"publisher","award":["NRF2014NCR-NCR001-30"],"award-info":[{"award-number":["NRF2014NCR-NCR001-30"]}],"id":[{"id":"10.13039\/501100022210","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"DOI":"10.1007\/s10703-024-00460-3","type":"journal-article","created":{"date-parts":[[2024,7,9]],"date-time":"2024-07-09T16:02:10Z","timestamp":1720540930000},"page":"200-236","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formally understanding Rust\u2019s ownership and borrowing system at the memory level"],"prefix":"10.1007","volume":"64","author":[{"given":"Shuanglong","family":"Kan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhe","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"San\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,9]]},"reference":[{"key":"460_CR1","unstructured":"Rust-Team: the Rust language homepage. https:\/\/www.rust-lang.org\/en-US\/ (2016)"},{"key":"460_CR2","doi-asserted-by":"publisher","unstructured":"Jung R, Jourdan J-H, Krebbers R, Dreyer D (2018) RustBelt: Securing the foundations of the Rust programming language. In: Proceedings of the ACM Program. Lang. 2, POPL, Article. https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"460_CR3","unstructured":"Reed E (2015) Patina: a formalization of the Rust programming language. Technical report, University of Washington"},{"issue":"POPL","key":"460_CR4","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1145\/3371109","volume":"4","author":"R Jung","year":"2020","unstructured":"Jung R, Dang H, Kang J, Dreyer D (2020) Stacked borrows: an aliasing model for rust. Proc ACM Program Lang 4(POPL):41\u201314132","journal-title":"Proc ACM Program Lang"},{"key":"460_CR5","unstructured":"Matsakis N (2016) Introducing MIR. https:\/\/blog.rust-lang.org\/2016\/04\/19\/MIR.html"},{"issue":"6","key":"460_CR6","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu G, \u015eerb\u0103nu\u0163\u0103 TF (2010) An overview of the K semantic framework. J Logic Algebr Program 79(6):397\u2013434","journal-title":"J Logic Algebr Program"},{"key":"460_CR7","doi-asserted-by":"publisher","unstructured":"Bogd\u0103na\u015f D, Ro\u015fu G (2015) K-Java: a complete semantics of Java. In: Proceedings of the 42nd symposium on principles of programming languages (POPL\u201915. ACM, New York), pp 445\u2013456. https:\/\/doi.org\/10.1145\/2676726.2676982","DOI":"10.1145\/2676726.2676982"},{"key":"460_CR8","doi-asserted-by":"publisher","unstructured":"Hathhorn C, Ellison C, Ro\u015fu G (2015) Defining the undefinedness of c. In: Proceedings of the 36th ACM SIGPLAN conference on programming language design and implementation (PLDI\u201915). ACM, New York, pp 336\u2013345. https:\/\/doi.org\/10.1145\/2813885.2737979","DOI":"10.1145\/2813885.2737979"},{"key":"460_CR9","doi-asserted-by":"publisher","unstructured":"Ellison C, Rosu G (2012) An executable formal semantics of c with applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL\u201912). ACM, New York, pp. 33\u2013544. https:\/\/doi.org\/10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"460_CR10","unstructured":"Davidoff SS (2018) How Rust\u2019s standard library was vulnerable for years and nobody noticed. https:\/\/medium.com\/@shnatsel\/how-rusts-standard-library-was-vulnerable-for-years-and-nobody-noticed-aebf0503c3d6"},{"key":"460_CR11","unstructured":"Rust-Benchmark: Rust Benchmark. https:\/\/github.com\/rust-lang\/rust\/tree\/master\/src\/test (2020)"},{"key":"460_CR12","unstructured":"Rust-Team (2018) The Rust programming language. Mozilla Research. Mozilla Research. https:\/\/doc.rust-lang.org\/book\/foreword.html"},{"key":"460_CR13","unstructured":"Rust-team: non-lexical lifetimes. https:\/\/doc.rust-lang.org\/edition-guide\/rust-2018\/ownership-and-lifetimes\/non-lexical-lifetimes.html (2018)"},{"key":"460_CR14","unstructured":"Matsakis N (2017) Nested method calls via two-phase borrowing. http:\/\/smallcultfollowing.com\/babysteps\/blog\/2017\/03\/01\/nested-method-calls-via-two-phase-borrowing\/"},{"key":"460_CR15","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr"},{"key":"460_CR16","doi-asserted-by":"publisher","unstructured":"Nipkow T, Klein G (2014) Concrete Semantics\u2014with Isabelle\/HOL. Springer, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-319-10542-0","DOI":"10.1007\/978-3-319-10542-0"},{"key":"460_CR17","doi-asserted-by":"publisher","unstructured":"Chen Z, Yan J, Kan S, Qian J, Xue J (2019) Detecting memory errors at runtime with source-level instrumentation. In: Zhang D, M\u00f8ller A (eds) Proceedings of the 28th ACM SIGSOFT international symposium on software testing and analysis, ISSTA 2019, Beijing, China, July 15-19, 2019. ACM, New York, pp 341\u2013351. https:\/\/doi.org\/10.1145\/3293882.3330581","DOI":"10.1145\/3293882.3330581"},{"key":"460_CR18","unstructured":"Team K-F (2024) C-Semantics in KFramework. https:\/\/github.com\/kframework\/c-semantics"},{"key":"460_CR19","doi-asserted-by":"publisher","unstructured":"de Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Tools and Algorithms for the Construction and Analysis of Systems, 14th international conference, TACAS 2008, Held as part of the joint european conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29\u2013April 6, 2008. Proceedings. Lecture Notes in Computer Science. Springer, Heidelberg, vol 4963, pp 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"460_CR20","doi-asserted-by":"publisher","unstructured":"\u015etef\u0103nescu A, Park D, Yuwen S, Li Y, Ro\u015fu G (2016) Semantics-based program verifiers for all languages. In: Proceedings of the 31th conference on object-oriented programming, systems, languages, and applications (OOPSLA\u201916). ACM, New York, pp 74\u201391. https:\/\/doi.org\/10.1145\/2983990.2984027","DOI":"10.1145\/2983990.2984027"},{"key":"460_CR21","unstructured":"issue 44800, V. https:\/\/github.com\/rust-lang\/rust\/issues\/44800 (2017)"},{"key":"460_CR22","doi-asserted-by":"crossref","unstructured":"Ishtiaq SS, O\u2019Hearn PW (2001) BI as an assertion language for mutable data structures. In: Hankin C, Schmidt D (eds) Conference record of POPL 2001: the 28th ACM SIGPLAN-SIGACT symposium on principles of programming languages, London, UK, January 17\u201319, 2001. ACM, New York, pp 14\u201326. http:\/\/dl.acm.org\/citation.cfm?id=360204","DOI":"10.1145\/360204.375719"},{"key":"460_CR23","doi-asserted-by":"publisher","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: 17th IEEE symposium on logic in computer science (LICS 2002), 22\u201325 July 2002, Copenhagen, Denmark, Proceedings. IEEE Computer Society, Washington DC, pp 55\u201374. https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"4","key":"460_CR24","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/3462205","volume":"43","author":"Y Matsushita","year":"2021","unstructured":"Matsushita Y, Tsukada T, Kobayashi N (2021) Rusthorn: CHC-based verification for rust programs. ACM Trans Program Lang Syst 43(4):15\u201311554. https:\/\/doi.org\/10.1145\/3462205","journal-title":"ACM Trans Program Lang Syst"},{"key":"460_CR25","doi-asserted-by":"publisher","unstructured":"Toman J, Pernsteiner S, Torlak E (2015) Crust: a bounded verifier for Rust (N). In: Cohen MB, Grunske L, Whalen M (eds) 30th IEEE\/ACM international conference on automated software engineering, ASE 2015, Lincoln, NE, USA, November 9\u201313, 2015. IEEE Computer Society, Washington DC, pp 75\u201380. https:\/\/doi.org\/10.1109\/ASE.2015.77","DOI":"10.1109\/ASE.2015.77"},{"key":"460_CR26","doi-asserted-by":"publisher","unstructured":"Baranowski MS, He S, Rakamaric Z (2018) Verifying Rust programs with SMACK. In: Lahiri SK, Wang C (eds) Automated technology for verification and analysis\u201416th international symposium, ATVA 2018, Los Angeles, CA, USA, October 7\u201310, 2018, Proceedings. lecture notes in computer science. Springer, Heidelberg, vol 11138, pp 528\u2013535. https:\/\/doi.org\/10.1007\/978-3-030-01090-4. https:\/\/doi.org\/10.1007\/978-3-030-01090-4_32","DOI":"10.1007\/978-3-030-01090-4 10.1007\/978-3-030-01090-4_32"},{"key":"460_CR27","doi-asserted-by":"publisher","unstructured":"Astrauskas V, M\u00fcller P, Poli F, Summers AJ (2019) Leveraging Rust types for modular specification and verification. In: To appear in object-oriented programming systems, languages, and applications (OOPSLA). ACM, New York. https:\/\/doi.org\/10.1145\/3360573","DOI":"10.1145\/3360573"},{"key":"460_CR28","doi-asserted-by":"publisher","unstructured":"Carter M, He S, Whitaker J, Rakamaric Z, Emmi M (2016) SMACK software verification toolchain. In: Dillon LK, Visser W, Williams L (eds) Proceedings of the 38th international conference on software engineering, ICSE 2016, Austin, TX, USA, May 14\u201322, 2016\u2014Companion Volume. ACM, New York, pp 589\u2013592. https:\/\/doi.org\/10.1145\/2889160.2889163","DOI":"10.1145\/2889160.2889163"},{"key":"460_CR29","doi-asserted-by":"publisher","unstructured":"M\u00fcller P, Schwerhoff M, Summers AJ (2016) Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann B, Leino KRM (eds) Verification, model checking, and abstract interpretation\u201417th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17\u201319, 2016. Proceedings. Lecture notes in computer science. Springer, Heidelberg, vol 9583, pp 41\u201362. https:\/\/doi.org\/10.1007\/978-3-662-49122-5_2","DOI":"10.1007\/978-3-662-49122-5_2"},{"issue":"ICFP","key":"460_CR30","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1145\/3547647","volume":"6","author":"S Ho","year":"2022","unstructured":"Ho S, Protzenko J (2022) AENEAS: Rust verification by functional translation. Proc ACM Program Lang 6(ICFP):711\u2013741. https:\/\/doi.org\/10.1145\/3547647","journal-title":"Proc ACM Program Lang"},{"key":"#cr-split#-460_CR31.1","unstructured":"Jim T, Morrisett JG, Grossman D, Hicks MW, Cheney J, Wang Y (2002) Cyclone: a safe dialect of C. In: Ellis CS"},{"key":"#cr-split#-460_CR31.2","unstructured":"(ed) Proceedings of the general track: 2002 USENIX annual technical conference, June 10-15, 2002, Monterey, California, USA, pp. 275-288. USENIX, Berkeley (2002). http:\/\/www.usenix.org\/publications\/library\/proceedings\/usenix02\/jim.html"},{"key":"460_CR32","doi-asserted-by":"publisher","unstructured":"Tofte M, Talpin J (1994) Implementation of the typed call-by-value lambda-calculus using a stack of regions. In: Boehm H, Lang B, Yellin DM (eds) conference record of POPL\u201994: 21st ACM SIGPLAN-SIGACT symposium on principles of programming languages, Portland, Oregon, USA, January 17\u201321, 1994. ACM Press, New York, pp 188\u2013201. https:\/\/doi.org\/10.1145\/174675.177855","DOI":"10.1145\/174675.177855"},{"issue":"4","key":"460_CR33","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/2837022","volume":"38","author":"T Balabonski","year":"2016","unstructured":"Balabonski T, Pottier F, Protzenko J (2016) The design and formalization of Mezzo, a permission-based programming language. ACM Trans Program Lang Syst 38(4):14\u201311494","journal-title":"ACM Trans Program Lang Syst"},{"key":"460_CR34","doi-asserted-by":"publisher","unstructured":"Tov JA, Pucella R (2011) Practical affine types. In: Ball T, Sagiv M (eds) Proceedings of the 38th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL 2011, Austin, TX, USA, January 26\u201328, 2011. ACM, New York, pp 447\u2013458. https:\/\/doi.org\/10.1145\/1926385.1926436","DOI":"10.1145\/1926385.1926436"},{"key":"460_CR35","doi-asserted-by":"publisher","unstructured":"Boyland J, Noble J, Retert W (2001) Capabilities for sharing: a generalisation of uniqueness and read-only. In: Knudsen JL (ed) ECOOP 2001\u2014object-oriented programming, 15th European conference, Budapest, Hungary, June 18\u201322, 2001, Proceedings. lecture notes in computer science Springer, Heidelberg, vol 2072, pp 2\u201327. https:\/\/doi.org\/10.1007\/3-540-45337-7_2","DOI":"10.1007\/3-540-45337-7_2"},{"key":"460_CR36","doi-asserted-by":"publisher","unstructured":"Clebsch S, Drossopoulou S, Blessing S, McNeil A (2015) Deny capabilities for safe, fast actors. In: Boix EG, Haller P, Ricci A, Varela C (eds) Proceedings of the 5th international workshop on programming based on actors, agents, and decentralized control, AGERE! 2015, Pittsburgh, PA, USA, October 26, 2015. ACM, New York, pp 1\u201312. https:\/\/doi.org\/10.1145\/2824815.2824816","DOI":"10.1145\/2824815.2824816"},{"key":"460_CR37","doi-asserted-by":"publisher","unstructured":"Stork S, Naden K, Sunshine J, Mohr M, Fonseca A, Marques P, Aldrich J (2014) \u00c6minium: a permission based concurrent-by-default programming language approach. In: O\u2019Boyle MFP, Pingali K (eds) ACM SIGPLAN conference on programming language design and implementation, PLDI\u201914, Edinburgh, United Kingdom\u2014June 09\u201311, 2014. ACM, New York, p 26. https:\/\/doi.org\/10.1145\/2594291.2594344","DOI":"10.1145\/2594291.2594344"},{"key":"460_CR38","doi-asserted-by":"publisher","unstructured":"Matsushita Y, Denis X, Jourdan J, Dreyer D (2022) Rusthornbelt: a semantic foundation for functional verification of rust programs with unsafe code. In: Jhala R, Dillig I (eds) PLDI\u201922: 43rd ACM SIGPLAN international conference on programming language design and implementation, San Diego, CA, USA, June 13\u201317, 2022. ACM, San Diego, pp 841\u2013856. https:\/\/doi.org\/10.1145\/3519939.3523704","DOI":"10.1145\/3519939.3523704"},{"key":"460_CR39","unstructured":"Weiss A, Patterson D, Matsakis ND, Ahmed A (2019) Oxide: the essence of Rust arXiv: 1903.00982"},{"key":"460_CR40","doi-asserted-by":"crossref","unstructured":"Wang F, Song F, Zhang M, Zhu X, Zhang J (2018) KRust: a formal executable semantics of Rust arXiv: 1804.10806","DOI":"10.1109\/TASE.2018.00014"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00460-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-024-00460-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-024-00460-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:03:34Z","timestamp":1735409014000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-024-00460-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,9]]},"references-count":41,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["460"],"URL":"https:\/\/doi.org\/10.1007\/s10703-024-00460-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,9]]},"assertion":[{"value":"2 January 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 May 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 July 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The datasets generated during and\/or analysed during the current study are available in the <b>Rust-Semantics repository<\/b>, .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}}]}}