{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:51Z","timestamp":1780994751171,"version":"3.54.1"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["DGE-1762114"],"award-info":[{"award-number":["DGE-1762114"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>Reasoning about memory aliasing and mutation in software verification is a hard problem. This is especially true for systems using SMT-based automated theorem provers. Memory reasoning in SMT verification typically requires a nontrivial amount of manual effort to specify heap invariants, as well as extensive alias reasoning from the SMT solver. In this paper, we present a hybrid approach that combines linear types with SMT-based verification for memory reasoning. We integrate linear types into Dafny, a verification language with an SMT backend, and show that the two approaches complement each other. By separating memory reasoning from verification conditions, linear types reduce the SMT solving time. At the same time, the expressiveness of SMT queries extends the flexibility of the linear type system. In particular, it allows our linear type system to easily and correctly mix linear and nonlinear data in novel ways, encapsulating linear data inside nonlinear data and vice-versa. We formalize the core of our extensions, prove soundness, and provide algorithms for linear type checking. We evaluate our approach by converting the implementation of a verified storage system (about 24K lines of code and proof) written in Dafny, to use our extended Dafny. The resulting system uses linear types for 91% of the code and SMT-based heap reasoning for the remaining 9%. We show that the converted system has 28% fewer lines of proofs and 30% shorter verification time overall. We discuss the development overhead in the original system due to SMT-based heap reasoning and highlight the improved developer experience when using linear types.<\/jats:p>","DOI":"10.1145\/3527313","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Linear types for large-scale systems verification"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2117-1947","authenticated-orcid":false,"given":"Jialin","family":"Li","sequence":"first","affiliation":[{"name":"University of Washington, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9303-452X","authenticated-orcid":false,"given":"Andrea","family":"Lattuada","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7597-1176","authenticated-orcid":false,"given":"Yi","family":"Zhou","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4870-0615","authenticated-orcid":false,"given":"Jonathan","family":"Cameron","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1781-2473","authenticated-orcid":false,"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"VMware Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-1684","authenticated-orcid":false,"given":"Bryan","family":"Parno","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-0362","authenticated-orcid":false,"given":"Chris","family":"Hawblitzel","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_17"},{"key":"e_1_2_1_4_1","first-page":"22","article-title":"An Introduction to B^\u220a -trees and Write-Optimization. ;login","volume":"40","author":"Bender Michael A.","year":"2015","unstructured":"Michael A. Bender , Martin Farach-Colton , William Jannen , Rob Johnson , Bradley C. Kuszmaul , Donald E. Porter , Jun Yuan , and Yang Zhan . 2015 . An Introduction to B^\u220a -trees and Write-Optimization. ;login : The USENIX Magazine , 40 , 5 (2015), Oct. , 22 \u2013 28 . Michael A. Bender, Martin Farach-Colton, William Jannen, Rob Johnson, Bradley C. Kuszmaul, Donald E. Porter, Jun Yuan, and Yang Zhan. 2015. An Introduction to B^\u220a -trees and Write-Optimization. ;login: The USENIX Magazine, 40, 5 (2015), Oct., 22\u201328.","journal-title":"The USENIX Magazine"},{"key":"e_1_2_1_5_1","volume-title":"SLAyer: Memory Safety for Systems-level Code. In Conference on Computer Aided Verification (CAV).","author":"Berdine Josh","year":"2011","unstructured":"Josh Berdine , Byron Cook , and Samin Ishtiaq . 2011 . SLAyer: Memory Safety for Systems-level Code. In Conference on Computer Aided Verification (CAV). Josh Berdine, Byron Cook, and Samin Ishtiaq. 2011. SLAyer: Memory Safety for Systems-level Code. In Conference on Computer Aided Verification (CAV)."},{"key":"e_1_2_1_6_1","volume-title":"15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21)","author":"Bhardwaj Ankit","year":"2021","unstructured":"Ankit Bhardwaj , Chinmay Kulkarni , Reto Achermann , Irina Calciu , Sanidhya Kashyap , Ryan Stutsman , Amy Tai , and Gerd Zellweger . 2021 . NrOS: Effective Replication and Sharing in an Operating System . In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21) . USENIX Association, 295\u2013312. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/bhardwaj Ankit Bhardwaj, Chinmay Kulkarni, Reto Achermann, Irina Calciu, Sanidhya Kashyap, Ryan Stutsman, Amy Tai, and Gerd Zellweger. 2021. NrOS: Effective Replication and Sharing in an Operating System. In 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI 21). USENIX Association, 295\u2013312. isbn:978-1-939133-22-9 https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/bhardwaj"},{"key":"e_1_2_1_7_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Boos Kevin","year":"2020","unstructured":"Kevin Boos , Namitha Liyanage , Ramla Ijaz , and Lin Zhong . 2020 . Theseus: an Experiment in Operating System Structure and State Management . In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) . USENIX Association, 1\u201319. isbn:978-1-939133-19-9 https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/boos Kevin Boos, Namitha Liyanage, Ramla Ijaz, and Lin Zhong. 2020. Theseus: an Experiment in Operating System Structure and State Management. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 1\u201319. isbn:978-1-939133-19-9 https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/boos"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_2"},{"key":"e_1_2_1_10_1","volume-title":"Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic. https:\/\/www.fstar-lang.org\/papers\/steel\/ In submission.","author":"Fromherz Aymeric","year":"2021","unstructured":"Aymeric Fromherz , Aseem Rastogi , Nikhil Swamy , Sydney Gibson , Guido Mart\u00ednez , Denis Merigoux , and Tahina Ramananandro . 2021 . Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic. https:\/\/www.fstar-lang.org\/papers\/steel\/ In submission. Aymeric Fromherz, Aseem Rastogi, Nikhil Swamy, Sydney Gibson, Guido Mart\u00ednez, Denis Merigoux, and Tahina Ramananandro. 2021. Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic. https:\/\/www.fstar-lang.org\/papers\/steel\/ In submission."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512563"},{"key":"e_1_2_1_13_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020","author":"Hance Travis","year":"2020","unstructured":"Travis Hance , Andrea Lattuada , Chris Hawblitzel , Jon Howell , Rob Johnson , and Bryan Parno . 2020 . Storage Systems are Distributed Systems (So Verify Them That Way!) . In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020 , Virtual Event , November 4-6, 2020. USENIX Association, 99\u2013115. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/hance Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. 2020. Storage Systems are Distributed Systems (So Verify Them That Way!). In 14th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2020, Virtual Event, November 4-6, 2020. USENIX Association, 99\u2013115. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/hance"},{"key":"e_1_2_1_14_1","unstructured":"Travis Hance Andrea Lattuada Chris Hawblitzel Jon Howell Rob Johnson and Bryan Parno. 2020. veribetrkv-osdi2020. https:\/\/github.com\/secure-foundations\/veribetrkv-osdi2020\/tree\/master\/docker-hdd\/src\/veribetrkv-dynamic-frames  Travis Hance Andrea Lattuada Chris Hawblitzel Jon Howell Rob Johnson and Bryan Parno. 2020. veribetrkv-osdi2020. https:\/\/github.com\/secure-foundations\/veribetrkv-osdi2020\/tree\/master\/docker-hdd\/src\/veribetrkv-dynamic-frames"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_2_1_16_1","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R. Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . 2014 . Ironclad Apps: End-to-End Security via Automated Full-System Verification . In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14) . USENIX Association, Broomfield, CO. 165\u2013181. isbn:978-1-93 1971-16-4 https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI 14). USENIX Association, Broomfield, CO. 165\u2013181. isbn:978-1-931971-16-4 https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21668-3_26"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_2_1_20_1","unstructured":"Steve Klabnik Carol Nichols and Rust Community. 2018. The Rust Programming Language https:\/\/doc.rust-lang.org\/book\/.  Steve Klabnik Carol Nichols and Rust Community. 2018. The Rust Programming Language https:\/\/doc.rust-lang.org\/book\/."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_2_1_22_1","volume-title":"Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers","author":"Lamport Leslie","year":"2002","unstructured":"Leslie Lamport . 2002 . Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers . Addison-Wesley . Leslie Lamport. 2002. Specifying Systems: The TLA+ Languange and Tools for Hardware and Software Engineers. Addison-Wesley."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI).","author":"M\u00fcller Peter","unstructured":"Peter M\u00fcller , Malte Schwerhoff , and Alexander J. Summers . 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning . In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)."},{"key":"e_1_2_1_26_1","volume-title":"14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20)","author":"Narayanan Vikram","year":"2020","unstructured":"Vikram Narayanan , Tianjiao Huang , David Detweiler , Dan Appel , Zhaofeng Li , Gerd Zellweger , and Anton Burtsev . 2020 . RedLeaf: Isolation and Communication in a Safe Operating System . In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20) . USENIX Association, 21\u201339. isbn:978-1-939133-19-9 https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/narayanan-vikram Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, and Anton Burtsev. 2020. RedLeaf: Isolation and Communication in a Safe Operating System. In 14th USENIX Symposium on Operating Systems Design and Implementation (OSDI 20). USENIX Association, 21\u201339. isbn:978-1-939133-19-9 https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/narayanan-vikram"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.177855"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods.","author":"Wadler Philip","year":"1990","unstructured":"Philip Wadler . 1990 . Linear Types Can Change the World! . In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods. Philip Wadler. 1990. Linear Types Can Change the World!. In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507658"},{"key":"e_1_2_1_32_1","volume-title":"Oxide: The Essence of Rust. CoRR, abs\/1903.00982","author":"Weiss Aaron","year":"2019","unstructured":"Aaron Weiss , Daniel Patterson , Nicholas D. Matsakis , and Amal Ahmed . 2019 . Oxide: The Essence of Rust. CoRR, abs\/1903.00982 (2019), https:\/\/doi.org\/10.48550\/ARXIV.1903.00982 arXiv:1903.00982. Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019. Oxide: The Essence of Rust. CoRR, abs\/1903.00982 (2019), https:\/\/doi.org\/10.48550\/ARXIV.1903.00982 arXiv:1903.00982."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473597"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527313","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527313","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527313","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527313"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":33,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527313"],"URL":"https:\/\/doi.org\/10.1145\/3527313","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}