{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T16:02:21Z","timestamp":1781193741483,"version":"3.54.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032280787","type":"print"},{"value":"9783032280794","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28079-4_19","type":"book-chapter","created":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:52Z","timestamp":1781191972000},"page":"415-435","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Verifying the\u00a0Rust Standard Library"],"prefix":"10.1007","author":[{"given":"Byron","family":"Cook","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Remi","family":"Delmas","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zyad","family":"Hassan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ranjit","family":"Jhala","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rahul","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Felipe R.","family":"Monteiro","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thanh","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rebecca","family":"Rumbul","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Tautschnig","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Celina","family":"Val","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carolyn","family":"Zech","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,12]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","unstructured":"Anderson, B., et al.: Engineering the servo web browser engine using rust. In: Proceedings of the 38th International Conference on Software Engineering Companion. ICSE 2016, pp. 81\u201389. Association for Computing Machinery, New York (2016). https:\/\/doi.org\/10.1145\/2889160.2889229","DOI":"10.1145\/2889160.2889229"},{"key":"19_CR2","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., et al.: The prusti project: formal verification for rust. In: NASA Formal Methods: 14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24\u201327, 2022, Proceedings, pp. 88\u2013108. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_5","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"19_CR3","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., Matheja, C., Poli, F., M\u00fcller, P., Summers, A.J.: How do programmers use unsafe rust? Proc. ACM Program. Lang. 4(OOPSLA) (2020). https:\/\/doi.org\/10.1145\/3428204","DOI":"10.1145\/3428204"},{"key":"19_CR4","doi-asserted-by":"publisher","unstructured":"Ayoun, S.E., Denis, X., Maksimovi\u0107, P., Gardner, P.: A hybrid approach to semi-automated rust verification. Proc. ACM Program. Lang. 9(PLDI) (2025). https:\/\/doi.org\/10.1145\/3729289","DOI":"10.1145\/3729289"},{"key":"19_CR5","unstructured":"Bhargavan, K., et al.: Project Everest: perspectives from developing industrial-grade high-assurance software. ACM Trans. Program. Lang. Syst. (2025). https:\/\/project-everest.github.io\/assets\/everest-perspectives-2025.pdf. to appear"},{"key":"19_CR6","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., et al.: hax: Verifying security-critical Rust software using multiple provers. In: Verified Software. Theories, Tools and Experiments (VSTTE), pp. 96\u2013119. Springer, Cham (2025). https:\/\/doi.org\/10.1007\/978-3-031-86695-1_7","DOI":"10.1007\/978-3-031-86695-1_7"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., Hansen, L.L., Kiefer, F., Schneider-Bensch, J., Spitters, B.: Formal security and functional verification of cryptographic protocol implementations in rust. In: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. CCS 2025, pp. 2729\u20132743. Association for Computing Machinery, New York (2025). https:\/\/doi.org\/10.1145\/3719027.3765213","DOI":"10.1145\/3719027.3765213"},{"key":"19_CR8","unstructured":"Blanc, A.L., Lam, P.: Lessons learned so far from a community effort to verify the Rust standard library (work-in-progress). https:\/\/arxiv.org\/abs\/2510.01072 (2025)"},{"key":"19_CR9","unstructured":"Boos, K., Liyanage, N., Ijaz, R., Zhong, L.: Theseus: an experiment in operating system structure and state management. In: Proceedings of the 14th USENIX Conference on Operating Systems Design and Implementation. OSDI 2020, USENIX Association, USA (2020)"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"Chen, H., Ziegler, D., Chajed, T., Chlipala, A., Kaashoek, M.F., Zeldovich, N.: Using crash hoare logic for certifying the FSCQ file system. In: Proceedings of SOSP, pp. 18\u201337. (2015). https:\/\/doi.org\/10.1145\/2815400.2815402","DOI":"10.1145\/2815400.2815402"},{"key":"19_CR11","doi-asserted-by":"publisher","unstructured":"Chong, N., et al.: Code-level model checking in the software development workflow at amazon web services. Softw. Pract. Experience 51(4), 772\u2013797 (2021). https:\/\/doi.org\/10.1002\/spe.2949","DOI":"10.1002\/spe.2949"},{"key":"19_CR12","doi-asserted-by":"publisher","unstructured":"Chong, N., et al.: Code-level model checking in the software development workflow. In: Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice. ICSE-SEIP 2020, pp. 11\u201320. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3377813.3381347","DOI":"10.1145\/3377813.3381347"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"issue":"1","key":"19_CR14","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/s10703-020-00344-2","volume":"57","author":"B Cook","year":"2021","unstructured":"Cook, B., Khazem, K., Kroening, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. Form. Methods Syst. Des. 57(1), 34\u201352 (2021). https:\/\/doi.org\/10.1007\/s10703-020-00344-2","journal-title":"Form. Methods Syst. Des."},{"key":"19_CR15","doi-asserted-by":"publisher","unstructured":"Cui, M., Sun, S., Xu, H., Zhou, Y.: Is unsafe an achilles\u2019 heel? A comprehensive study of safety requirements in unsafe Rust programming. In: Proceedings of ICSE (2024). https:\/\/doi.org\/10.1145\/3597503.3639136","DOI":"10.1145\/3597503.3639136"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Dang, H.H., Jourdan, J.H., Kaiser, J.O., Dreyer, D.: RustBelt meets relaxed memory. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371102","DOI":"10.1145\/3371102"},{"key":"19_CR17","doi-asserted-by":"publisher","unstructured":"Denis, X., Jourdan, J.H., March\u00e9, C.: Creusot: a foundry for the deductive verification of Rust programs. In: Formal Methods and Software Engineering (ICFEM). LNCS, vol. 13478, pp. 90\u2013105. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_6","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: an industrial-strength c model checker. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering. ASE 2018, pp. 888\u2013891. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3238147.3240481","DOI":"10.1145\/3238147.3240481"},{"key":"19_CR19","doi-asserted-by":"publisher","unstructured":"G\u00e4her, L., Sammler, M., Jung, R., Krebbers, R., Dreyer, D.: RefinedRust: a type system for high-assurance verification of Rust programs. Proc. ACM Program. Lang. 8(PLDI) (2024). https:\/\/doi.org\/10.1145\/3656422","DOI":"10.1145\/3656422"},{"key":"19_CR20","doi-asserted-by":"publisher","unstructured":"Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don\u2019t sweat the small stuff: formal verification of C code without the pain. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 429\u2013439 (2014). https:\/\/doi.org\/10.1145\/2594291.2594296","DOI":"10.1145\/2594291.2594296"},{"key":"19_CR21","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X., Kim, J., Sj\u00f6berg, V., Costanzo, D.: CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: Proceedings of OSDI, pp. 653\u2013669 (2016)"},{"key":"19_CR22","unstructured":"Hawblitzel, C., et al.: Ironclad apps: end-to-end security via automated full-system verification. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation (OSDI), pp. 165\u2013181. USENIX Association (2014)"},{"key":"19_CR23","doi-asserted-by":"publisher","unstructured":"Huang, L., Ebersold, S., Kogtenkov, A., Meyer, B., Liu, Y.: Lessons from formally verified deployed software systems. ACM Comput. Surv. 58(8) (2026). https:\/\/doi.org\/10.1145\/3785652","DOI":"10.1145\/3785652"},{"key":"19_CR24","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Fasse, J.: An approach for modularly verifying the core of Rust\u2019s atomic reference counting algorithm against the (Y)C20 memory consistency model. J. Object Technol. 25(3) (2025). https:\/\/doi.org\/10.5381\/jot.2025.25.3.a5","DOI":"10.5381\/jot.2025.25.3.a5"},{"key":"19_CR25","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: Proceedings of the Third International Conference on NASA Formal Methods. NFM 2011, pp. 41\u201355. Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"19_CR26","doi-asserted-by":"publisher","unstructured":"Jung, R., Dang, H.H., Kang, J., Dreyer, D.: Stacked borrows: an aliasing model for rust. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371109","DOI":"10.1145\/3371109"},{"key":"19_CR27","doi-asserted-by":"publisher","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: Rustbelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL) (2017). https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"issue":"4","key":"19_CR28","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/3418295","volume":"64","author":"R Jung","year":"2021","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: Safe systems programming in rust. Commun. ACM 64(4), 144\u2013152 (2021). https:\/\/doi.org\/10.1145\/3418295","journal-title":"Commun. ACM"},{"key":"19_CR29","doi-asserted-by":"publisher","unstructured":"Jung, R., Kimock, B., Poveda, C., S\u00e1nchez Mu\u00f1oz, E., Scherer, O., Wang, Q.: Miri: practical undefined behavior detection for Rust. Proc. ACM Program. Lang 10(POPL) (2026). https:\/\/doi.org\/10.1145\/3776690","DOI":"10.1145\/3776690"},{"key":"19_CR30","doi-asserted-by":"publisher","unstructured":"Lattuada, A., et al.: Verus: verifying rust programs using linear ghost types. Proc. ACM Program. Lang. 7(OOPSLA2) (2023). https:\/\/doi.org\/10.1145\/3586037","DOI":"10.1145\/3586037"},{"key":"19_CR31","doi-asserted-by":"publisher","unstructured":"Lehmann, N., Geller, A.T., Vazou, N., Jhala, R.: Flux: liquid types for rust. Proc. ACM Program. Lang. 7(PLDI) (2023). https:\/\/doi.org\/10.1145\/3591283","DOI":"10.1145\/3591283"},{"issue":"7","key":"19_CR32","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"key":"19_CR33","doi-asserted-by":"publisher","unstructured":"Levy, A., et al.: Multiprogramming a 64kb computer safely and efficiently. In: Proceedings of the 26th Symposium on Operating Systems Principles. SOSP 2017, pp. 234\u2013251. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3132747.3132786","DOI":"10.1145\/3132747.3132786"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Li, Z., Wang, J., Sun, M., Lui, J.C.: Mirchecker: Detecting bugs in rust programs via static analysis. In: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security. CCS 2021, pp. 2183\u20132196. Association for Computing Machinery, New York (2021)","DOI":"10.1145\/3460120.3484541"},{"key":"19_CR35","unstructured":"Rust Team: The rust reference: Behavior considered undefined (2024). https:\/\/doc.rust-lang.org\/reference\/behavior-considered-undefined.html"},{"key":"19_CR36","doi-asserted-by":"publisher","unstructured":"VanHattum, A., Schwartz-Narbonne, D., Chong, N., Sampson, A.: Verifying dynamic trait objects in Rust. In: Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice. ICSE-SEIP 2022, pp. 321\u2013330. Association for Computing Machinery (2022). https:\/\/doi.org\/10.1145\/3510457.3513031","DOI":"10.1145\/3510457.3513031"},{"key":"19_CR37","doi-asserted-by":"publisher","unstructured":"Villani, N., Hostert, J., Dreyer, D., Jung, R.: Tree borrows. Proc. ACM Program. Lang 9(PLDI) (2025). https:\/\/doi.org\/10.1145\/3735592","DOI":"10.1145\/3735592"},{"key":"19_CR38","doi-asserted-by":"publisher","unstructured":"Wang, F., Song, F., Zhang, M., Zhu, X., Zhang, J.: KRust: a formal executable semantics of rust. In: 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE). pp. 44\u201351. IEEE Computer Society, Los Alamitos (2018). https:\/\/doi.org\/10.1109\/TASE.2018.00014","DOI":"10.1109\/TASE.2018.00014"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28079-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,11]],"date-time":"2026-06-11T15:32:55Z","timestamp":1781191975000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28079-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032280787","9783032280794"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28079-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"12 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 May 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/nfm2026.github.io\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}