{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T22:30:05Z","timestamp":1769725805939,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":50,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,14]],"date-time":"2024-04-14T00:00:00Z","timestamp":1713052800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["NSF-1929701"],"award-info":[{"award-number":["NSF-1929701"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CCF-1845446"],"award-info":[{"award-number":["CCF-1845446"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,14]]},"DOI":"10.1145\/3639477.3639714","type":"proceedings-article","created":{"date-parts":[[2024,5,31]],"date-time":"2024-05-31T13:27:26Z","timestamp":1717162046000},"page":"441-451","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Broadly Enabling KLEE to Effortlessly Find Unrecoverable Errors in Rust"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2770-9189","authenticated-orcid":false,"given":"Ying","family":"Zhang","sequence":"first","affiliation":[{"name":"Virginia Tech, Blacksburg, Virginia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-7043-2645","authenticated-orcid":false,"given":"Peng","family":"Li","sequence":"additional","affiliation":[{"name":"Zoox, Foster City, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-1918-782X","authenticated-orcid":false,"given":"Yu","family":"Ding","sequence":"additional","affiliation":[{"name":"Google, Mountain View, California, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1946-7539","authenticated-orcid":false,"given":"Lingxiang","family":"Wang","sequence":"additional","affiliation":[{"name":"Microsoft, Seattle, Washington, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1537-0525","authenticated-orcid":false,"given":"Dan","family":"Williams","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, Virginia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0230-5524","authenticated-orcid":false,"given":"Na","family":"Meng","sequence":"additional","affiliation":[{"name":"Virginia Tech, Blacksburg, Virginia, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,5,31]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"\"Why is Rust programming language so popular?\" https:\/\/codilime.com\/blog\/why-is-rust-programming-language-so-popular\/ 2021."},{"key":"e_1_3_2_1_2_1","unstructured":"\"Error Handling \" https:\/\/doc.rust-lang.org\/book\/ch09-00-error-handling.html 2022."},{"key":"e_1_3_2_1_3_1","unstructured":"\"Rust - Error Handling \" https:\/\/www.tutorialspoint.com\/rust\/rust_error_handling.htm 2022."},{"key":"e_1_3_2_1_4_1","unstructured":"\"Rust Error Handling In Practice \" https:\/\/medium.com\/coinmonks\/rust-error-handling-in-practice-376d86ba12ca 2023."},{"key":"e_1_3_2_1_5_1","unstructured":"\"Panics - Comprehensive Rust \" https:\/\/google.github.io\/comprehensive-rust\/error-handling\/panics.html 2023."},{"key":"e_1_3_2_1_6_1","first-page":"108","volume-title":"IEEE","author":"Lindner M.","year":"2018","unstructured":"M. Lindner, J. Aparicius, and P. Lindgren, \"No panic! verification of rust programs by symbolic execution,\" in 2018 IEEE 16th International Conference on Industrial Informatics (INDIN). IEEE, 2018, pp. 108--114."},{"key":"e_1_3_2_1_7_1","first-page":"432","volume-title":"Verification of safety functions implemented in rust - a symbolic execution based approach,\" in 2019 IEEE 17th International Conference on Industrial Informatics (INDIN)","author":"Lindner M.","year":"2019","unstructured":"M. Lindner, N. Fitinghoff, J. Eriksson, and P. Lindgren, \"Verification of safety functions implemented in rust - a symbolic execution based approach,\" in 2019 IEEE 17th International Conference on Industrial Informatics (INDIN), vol. 1. IEEE, 2019, pp. 432--439."},{"key":"e_1_3_2_1_8_1","unstructured":"\"project-oak\/rust-verification-tools \" https:\/\/github.com\/project-oak\/rust-verification-tools\/\/ 2022."},{"key":"e_1_3_2_1_9_1","first-page":"16345","article-title":"Towards making formal methods normal: meeting developers where they are","volume":"2010","author":"Reid A.","year":"2020","unstructured":"A. Reid, L. Church, S. Flur, S. de Haas, M. Johnson, and B. Laurie, \"Towards making formal methods normal: meeting developers where they are,\" CoRR, vol. abs\/2010.16345, 2020. [Online]. Available: https:\/\/arxiv.org\/abs\/2010.16345","journal-title":"CoRR"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081749"},{"key":"e_1_3_2_1_11_1","unstructured":"\"Rust\/KLEE status update \" https:\/\/project-oak.github.io\/rust-verification-tools\/2021\/03\/29\/klee-status.html 2021."},{"key":"e_1_3_2_1_12_1","first-page":"1","volume-title":"GA: USENIX Association","author":"Sigurbjarnarson H.","year":"2016","unstructured":"H. Sigurbjarnarson, J. Bornholt, E. Torlak, and X. Wang, \"Push-Button verification of file systems via crash refinement,\" in 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). Savannah, GA: USENIX Association, Nov. 2016, pp. 1--16. [Online]. Available: https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/sigurbjarnarson"},{"key":"e_1_3_2_1_13_1","first-page":"209","volume-title":"OSDI'08","author":"Cadar C.","year":"2008","unstructured":"C. Cadar, D. Dunbar, and D. Engler, \"Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs,\" in Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, ser. OSDI'08. USA: USENIX Association, 2008, pp. 209--224."},{"key":"e_1_3_2_1_14_1","volume-title":"https:\/\/alastairreid.github.io\/automatic-rust-verification-tools-2021\/","year":"2021","unstructured":"\"Automatic Rust verification tools (2021),\" https:\/\/alastairreid.github.io\/automatic-rust-verification-tools-2021\/, 2021."},{"key":"e_1_3_2_1_15_1","unstructured":"\"Type of bugs that KLEE can find \" http:\/\/mailman.ic.ac.uk\/pipermail\/klee-dev\/2020-April\/001983.html 2020."},{"key":"e_1_3_2_1_16_1","unstructured":"\"Crates \" https:\/\/doc.rust-lang.org\/rust-by-example\/crates.html."},{"key":"e_1_3_2_1_17_1","unstructured":"\"integer-encoding 1.1.7 \" https:\/\/crates.io\/crates\/integer-encoding\/1.1.7 2021."},{"key":"e_1_3_2_1_18_1","unstructured":"\"Primitive Type slice \" https:\/\/doc.rust-lang.org\/std\/primitive.slice.html."},{"key":"e_1_3_2_1_19_1","unstructured":"\"syn \" https:\/\/docs.rs\/syn\/latest\/syn\/ 2022."},{"key":"e_1_3_2_1_20_1","unstructured":"\"What's the difference between references and pointers in Rust?\" https:\/\/ntietz.com\/blog\/rust-references-vs-pointers\/ 2023."},{"key":"e_1_3_2_1_21_1","unstructured":"\"Basic-Topic-String-and-string-Slice \" https:\/\/users.rust-lang.org\/t\/basic-topic-string-and-string-slice\/41479 2020."},{"key":"e_1_3_2_1_22_1","unstructured":"\"HashMap in std::collections - Rust \" https:\/\/doc.rust-lang.org\/std\/collections\/struct.HashMap.html 2022."},{"key":"e_1_3_2_1_23_1","unstructured":"\"HashSet in std::collections - Rust \" https:\/\/doc.rust-lang.org\/std\/collections\/hash_set\/struct.HashSet.html 2022."},{"key":"e_1_3_2_1_24_1","unstructured":"\"Strategy - Rust Design Patterns \" https:\/\/rust-unofficial.github.io\/patterns\/patterns\/behavioural\/strategy.html 2022."},{"key":"e_1_3_2_1_25_1","volume-title":"Rust Package Registry,\" https:\/\/crates.io","year":"2022","unstructured":"\"crates.io: Rust Package Registry,\" https:\/\/crates.io, 2022."},{"key":"e_1_3_2_1_26_1","unstructured":"\"Coreutils - GNU core utilities \" https:\/\/www.gnu.org\/software\/coreutils\/ 2022."},{"key":"e_1_3_2_1_27_1","unstructured":"\"Proptest Book \" https:\/\/altsysrq.github.io\/proptest-book\/intro.html 2022."},{"key":"e_1_3_2_1_28_1","unstructured":"\"clap - Rust \" https:\/\/docs.rs\/clap\/latest\/clap\/ 2022."},{"key":"e_1_3_2_1_29_1","unstructured":"\"\"timeout\" needs better error message \" https:\/\/github.com\/uutils\/coreutils\/issues\/3040 2022."},{"key":"e_1_3_2_1_30_1","first-page":"1143","volume-title":"ICSE '12","author":"Kim Y.","year":"2012","unstructured":"Y. Kim, M. Kim, Y. Kim, and Y. Jang, \"Industrial application of concolic testing approach: A case study on libexif by using crest-bv and klee,\" in Proceedings of the 34th International Conference on Software Engineering, ser. ICSE '12. IEEE Press, 2012, pp. 1143--1152."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771818"},{"key":"e_1_3_2_1_32_1","first-page":"205","volume-title":"Studying the influence of standard compiler optimizations on symbolic execution,\" in 2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE)","author":"Dong S.","year":"2015","unstructured":"S. Dong, O. Olivo, L. Zhang, and S. Khurshid, \"Studying the influence of standard compiler optimizations on symbolic execution,\" in 2015 IEEE 26th International Symposium on Software Reliability Engineering (ISSRE), 2015, pp. 205--215."},{"key":"e_1_3_2_1_33_1","first-page":"601","volume-title":"ASE '17","author":"Liew D.","year":"2017","unstructured":"D. Liew, D. Schemmel, C. Cadar, A. F. Donaldson, R. Z\u00e4hl, and K. Wehrle, \"Floatingpoint symbolic execution: A case study in n-version programming,\" in Proceedings of the 32nd IEEE\/ACM International Conference on Automated Software Engineering, ser. ASE '17. IEEE Press, 2017, pp. 601--612."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31157-5_3"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2018.2866469"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534384"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2022.111269"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2023.111629"},{"key":"e_1_3_2_1_39_1","first-page":"106","volume-title":"Smack: Decoupling source language details from verifier implementations,\" in International Conference on Computer Aided Verification","author":"Rakamari\u0107 Z.","year":"2014","unstructured":"Z. Rakamari\u0107 and M. Emmi, \"Smack: Decoupling source language details from verifier implementations,\" in International Conference on Computer Aided Verification. Springer, 2014, pp. 106--113."},{"key":"e_1_3_2_1_40_1","first-page":"75","volume-title":"IEEE","author":"Toman J.","year":"2015","unstructured":"J. Toman, S. Pernsteiner, and E. Torlak, \"Crust: a bounded verifier for rust (n),\" in 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE). IEEE, 2015, pp. 75--80."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_1_42_1","first-page":"321","volume-title":"Verifying dynamic trait objects in rust,\" in 2022 IEEE\/ACM 44th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP)","author":"VanHattum A.","year":"2022","unstructured":"A. VanHattum, D. Schwartz-Narbonne, N. Chong, and A. Sampson, \"Verifying dynamic trait objects in rust,\" in 2022 IEEE\/ACM 44th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), 2022, pp. 321--330."},{"key":"e_1_3_2_1_43_1","unstructured":"Facebook \"MIRAI \" https:\/\/github.com\/facebookexperimental\/MIRAI 2019."},{"key":"e_1_3_2_1_44_1","unstructured":"\"Crux-MIR \" https:\/\/github.com\/GaloisInc\/crucible\/blob\/master\/crux-mir 2020."},{"key":"e_1_3_2_1_45_1","first-page":"168","volume-title":"A tool for checking ansi-c programs,\" in Tools and Algorithms for the Construction and Analysis of Systems","author":"Clarke E.","year":"2004","unstructured":"E. Clarke, D. Kroening, and F. Lerda, \"A tool for checking ansi-c programs,\" in Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, pp. 168--176."},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_2"},{"key":"e_1_3_2_1_47_1","first-page":"364","volume-title":"F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P","author":"Barnett M.","year":"2006","unstructured":"M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino, \"Boogie: A modular reusable verifier for object-oriented programs,\" in Formal Methods for Components and Objects, F. S. de Boer, M. M. Bonsangue, S. Graf, and W.-P. de Roever, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2006, pp. 364--387."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"e_1_3_2_1_50_1","unstructured":"\"Seahorn \" https:\/\/github.com\/seahorn\/seahorn 2011."}],"event":{"name":"ICSE-SEIP '24: 46th International Conference on Software Engineering: Software Engineering in Practice","location":"Lisbon Portugal","acronym":"ICSE-SEIP '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS","Faculty of Engineering of University of Porto"]},"container-title":["Proceedings of the 46th International Conference on Software Engineering: Software Engineering in Practice"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3639477.3639714","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3639477.3639714","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3639477.3639714","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:44:31Z","timestamp":1750290271000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3639477.3639714"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,14]]},"references-count":50,"alternative-id":["10.1145\/3639477.3639714","10.1145\/3639477"],"URL":"https:\/\/doi.org\/10.1145\/3639477.3639714","relation":{},"subject":[],"published":{"date-parts":[[2024,4,14]]},"assertion":[{"value":"2024-05-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}