{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:01:38Z","timestamp":1779087698329,"version":"3.51.4"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031067723","type":"print"},{"value":"9783031067730","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:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-06773-0_5","type":"book-chapter","created":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T11:24:44Z","timestamp":1652959484000},"page":"88-108","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["The Prusti Project: Formal Verification for\u00a0Rust"],"prefix":"10.1007","author":[{"given":"Vytautas","family":"Astrauskas","sequence":"first","affiliation":[]},{"given":"Aurel","family":"B\u00edl\u00fd","sequence":"additional","affiliation":[]},{"given":"Jon\u00e1\u0161","family":"Fiala","sequence":"additional","affiliation":[]},{"given":"Zachary","family":"Grannan","sequence":"additional","affiliation":[]},{"given":"Christoph","family":"Matheja","sequence":"additional","affiliation":[]},{"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[]},{"given":"Federico","family":"Poli","sequence":"additional","affiliation":[]},{"given":"Alexander J.","family":"Summers","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,5,20]]},"reference":[{"key":"5_CR1","unstructured":"Procedural macros documentation (2022). https:\/\/doc.rust-lang.org\/reference\/procedural-macros.html"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. In: Proceedings of the 3rd Annual Symposium on Logic in Computer Science, pp. 165\u2013175, July 1988. https:\/\/www.microsoft.com\/en-us\/research\/publication\/the-existence-of-refinement-mappings\/, lICS 1988 Test of Time Award","DOI":"10.1109\/LICS.1988.5115"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/978-3-642-54830-7_27","volume-title":"Foundations of Software Science and Computation Structures","author":"T Antonopoulos","year":"2014","unstructured":"Antonopoulos, T., Gorogiannis, N., Haase, C., Kanovich, M., Ouaknine, J.: Foundations for decision problems in separation logic with general inductive predicates. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 411\u2013425. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54830-7_27"},{"key":"5_CR4","unstructured":"Astrauskas, V.: Enable compiler consumers to obtain MIR: Body with Polonius facts. https:\/\/github.com\/rust-lang\/rust\/pull\/86977"},{"key":"5_CR5","doi-asserted-by":"crossref","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), 1\u201327 (2020)","DOI":"10.1145\/3428204"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. Proc. ACM Program. Lang. 3(OOPSLA), 147:1\u2013147:30 (2019). https:\/\/doi.org\/10.1145\/3360573","DOI":"10.1145\/3360573"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/978-3-030-01090-4_32","volume-title":"Automated Technology for Verification and Analysis","author":"M Baranowski","year":"2018","unstructured":"Baranowski, M., He, S., Rakamari\u0107, Z.: Verifying rust programs with SMACK. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 528\u2013535. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_32"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art: The Calculus of Inductive Constructions. In: Texts in Theoretical Computer Science. An EATCS Series, pp. XXV\u2013472. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"5_CR9","unstructured":"Bloch, J.: Extra, extra - read all about it: Nearly all binary searches and mergesorts are broken, June 2006. https:\/\/ai.googleblog.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 259\u2013270 (2005)","DOI":"10.1145\/1047659.1040327"},{"key":"5_CR11","unstructured":"Clippy developers: Clippy: A collection of lints to catch common mistakes and improve your Rust code. https:\/\/github.com\/rust-lang\/rust-clippy"},{"key":"5_CR12","unstructured":"Crichton, W.: Flowistry: Information flow for Rust. https:\/\/github.com\/willcrichton\/flowistry"},{"key":"5_CR13","unstructured":"Tolnay, D.: Parser for Rust source code (2021). https:\/\/crates.io\/crates\/syn"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Denis, X., Jourdan, J.H., March\u00e9, C.: The Creusot environment for the deductive verification of Rust programs (2021)","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Dill, D., Grieskamp, W., Park, J., Qadeer, S., Xu, M., Zhong, E.: Fast and reliable formal verification of smart contracts with the Move prover. arXiv preprint arXiv:2110.08362 (2021)","DOI":"10.1007\/978-3-030-99524-9_10"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Evans, A.N., Campbell, B., Soffa, M.L.: Is rust used safely by software developers? In: 2020 IEEE\/ACM 42nd International Conference on Software Engineering (ICSE), pp. 246\u2013257. IEEE (2020)","DOI":"10.1145\/3377811.3380413"},{"key":"5_CR17","unstructured":"Facebook: MIRAI: an abstract interpreter for the Rust compiler\u2019s mid-level intermediate representation. https:\/\/github.com\/facebookexperimental\/MIRAI"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-58298-2_1","volume-title":"Formal Methods for Industrial Critical Systems","author":"H Garavel","year":"2020","unstructured":"Garavel, H., Beek, M.H., Pol, J.: The 2020 expert survey on formal methods. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 3\u201369. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1"},{"key":"5_CR19","unstructured":"Goes, C.: The interblockchain communication protocol: an overview. arXiv preprint arXiv:2006.15918 (2020)"},{"key":"5_CR20","unstructured":"Hahn, F.: Rust2Viper: building a static verifier for Rust. Master\u2019s thesis, ETH Zurich (2015)"},{"key":"5_CR21","unstructured":"Informal Systems Inc. and ibc-rs authors: Rust implementation of the Inter-Blockchain Communication (IBC) protocol (2021). https:\/\/docs.rs\/ibc"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-11936-6_15","volume-title":"Automated Technology for Verification and Analysis","author":"R Iosif","year":"2014","unstructured":"Iosif, R., Rogalewicz, A., Vojnar, T.: Deciding entailments in inductive separation logic with tree automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 201\u2013218. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_15"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: POPL, pp. 14\u201326. ACM (2001)","DOI":"10.1145\/373243.375719"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","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: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"key":"5_CR25","unstructured":"Jung, R.: The scope of unsafe, January 2016. https:\/\/www.ralfj.de\/blog\/2016\/01\/09\/the-scope-of-unsafe.html"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Jung, R., Dang, H.H., Kang, J., Dreyer, D.: Stacked borrows: an aliasing model for Rust. Proc. ACM Program. Lang. 4(POPL), 1\u201332 (2019)","DOI":"10.1145\/3371109"},{"key":"5_CR27","doi-asserted-by":"crossref","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), 1\u201334 (2017)","DOI":"10.1145\/3158154"},{"key":"5_CR28","unstructured":"Seonghoon, K., et al.: Chrono: Date and Time for Rust (2021). https:\/\/docs.rs\/chrono"},{"issue":"3","key":"5_CR29","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The dynamic frames theory. Formal Aspects Comput. 23(3), 267\u2013289 (2011)","journal-title":"Formal Aspects Comput."},{"key":"5_CR30","unstructured":"Klabnik, S., Nichols, C.: Unsafe Rust (2022). https:\/\/doc.rust-lang.org\/book\/ch19-01-unsafe-rust.html"},{"key":"5_CR31","doi-asserted-by":"crossref","unstructured":"Lindner, M., Aparicius, J., Lindgren, P.: No panic! Verification of Rust programs by symbolic execution. In: 2018 IEEE 16th International Conference on Industrial Informatics (INDIN), pp. 108\u2013114. IEEE (2018)","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"5_CR32","unstructured":"Matsakis, N.D.: Unsafe abstractions (2016). http:\/\/smallcultfollowing.com\/babysteps\/blog\/2016\/05\/23\/unsafe-abstractions"},{"key":"5_CR33","unstructured":"Matsushita, Y.: Extensible functional-correctness verification of rust programs by the technique of prophecy. Master\u2019s thesis, University of Tokyo (2021)"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. In: ESOP, pp. 484\u2013514 (2020)","DOI":"10.1007\/978-3-030-44914-8_18"},{"key":"5_CR35","unstructured":"Meyer, B.: Design by contract. In: Mandrioli, D., Meyer, B. (eds.) Advances in Object-Oriented Software Engineering, pp. 1\u201350. Prentice Hall (1991)"},{"key":"5_CR36","unstructured":"Miri developers: Miri: An interpreter for Rust\u2019s mid-level intermediate representation. https:\/\/github.com\/rust-lang\/miri"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"5_CR38","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"},{"issue":"2","key":"5_CR39","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1145\/3211968","volume":"62","author":"P O\u2019Hearn","year":"2019","unstructured":"O\u2019Hearn, P.: Separation logic. Commun. ACM 62(2), 86\u201395 (2019)","journal-title":"Commun. ACM"},{"key":"5_CR40","doi-asserted-by":"crossref","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)","DOI":"10.2168\/LMCS-8(3:1)2012"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Pratt, V.R.: Top down operator precedence. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 41\u201351 (1973)","DOI":"10.1145\/512927.512931"},{"key":"5_CR42","unstructured":"Reid, A., Church, L., Flur, S., de Haas, S., Johnson, M., Laurie, B.: Towards making formal methods normal: meeting developers where they are. arXiv preprint arXiv:2010.16345 (2020)"},{"key":"5_CR43","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE (2002)"},{"key":"5_CR44","unstructured":"Rust-analyzer developers: Rust-analyzer: A Rust compiler front-end for ides. https:\/\/github.com\/rust-analyzer\/rust-analyzer"},{"key":"5_CR45","unstructured":"Schwerhoff, M., Summers, A.J.: Lightweight support for magic wands in an automatic verifier. In: 29th European Conference on Object-Oriented Programming (ECOOP 2015), vol. 37, pp. 614\u2013638. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"5_CR46","unstructured":"Schwerhoff, M.H.: Advancing automated, permission-based program verification using symbolic execution. Ph.D. thesis, ETH Zurich (2016)"},{"key":"5_CR47","unstructured":"The Prusti Team: Prusti User Guide (2020). https:\/\/viperproject.github.io\/prusti-dev\/user-guide\/"},{"key":"5_CR48","unstructured":"The Prusti Team: Prusti NFM 2022 Online Appendix (2022). https:\/\/github.com\/viperproject\/prusti-dev\/tree\/master\/prusti-tests\/tests\/verify_overflow\/pass\/nfm22"},{"key":"5_CR49","unstructured":"The Rust Survey Team: Rust survey 2019 results: Rust blog, April 2020. https:\/\/blog.rust-lang.org\/2020\/04\/17\/Rust-survey-2019.html"},{"key":"5_CR50","unstructured":"Ullrich, S.: Simple verification of Rust programs via functional purification. Master\u2019s thesis, Karlsruher Institut f\u00fcr Technologie (KIT) (2016)"},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"VanHattum, A., Schwartz-Narbonne, D., Chong, N., Sampson, A.: Verifying dynamic trait objects in Rust (2022)","DOI":"10.1109\/ICSE-SEIP55303.2022.9794041"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"Wolff, F., B\u00edl\u00fd, A., Matheja, C., M\u00fcller, P., Summers, A.J.: Modular specification and verification of closures in Rust. Proc. ACM Program. Lang. 5(OOPSLA), 1\u201329 (2021)","DOI":"10.1145\/3485522"}],"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-031-06773-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,25]],"date-time":"2024-09-25T14:25:20Z","timestamp":1727274320000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-06773-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031067723","9783031067730"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-06773-0_5","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":"20 May 2022","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":"Pasadena, 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":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-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":"118","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":"33","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":"6","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":"28% - 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","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":"6.3","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}