{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:23:48Z","timestamp":1763054628941,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3764860.3768326","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T13:54:43Z","timestamp":1759326883000},"page":"51-59","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Debug, Execute, Verify! Development-Verification Co-Design Made Practical"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8177-1322","authenticated-orcid":false,"given":"Franti\u0161ek","family":"Farka","sequence":"first","affiliation":[{"name":"Barkhausen Institute, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8562-8750","authenticated-orcid":false,"given":"Carmine","family":"Abate","sequence":"additional","affiliation":[{"name":"Barkhausen Institute, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4132-2626","authenticated-orcid":false,"given":"Shuanglong","family":"Kan","sequence":"additional","affiliation":[{"name":"Barkhausen Institute, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-3953-9810","authenticated-orcid":false,"given":"Sebastian","family":"Ertel","sequence":"additional","affiliation":[{"name":"Barkhausen Institute, Dresden, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,13]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. The Rust Reference. https:\/\/doc.rust-lang.org\/stable\/reference"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872371"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"e_1_3_2_1_4_1","unstructured":"Hanno Becker Nathan Chong Robert Dockins Jim Grundy Jason Z. S. Hu Ike Mulder Dominic P. Mulligan Paul Mure Lawrence C. Paulson and Konrad Slind. 2025. AutoCorrode software verification framework for Isabelle\/HOL. https:\/\/github.com\/awslabs\/autocorrode."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_5"},{"key":"e_1_3_2_1_6_1","volume-title":"Franziskus Kiefer, Jonas Schneider-Bensch, and Bas Spitters.","author":"Bhargavan Karthikeyan","year":"2025","unstructured":"Karthikeyan Bhargavan, Maxime Buyse, Lucas Franceschino, Lasse Letager Hansen, Franziskus Kiefer, Jonas Schneider-Bensch, and Bas Spitters. 2025. hax: Verifying Security-Critical Rust Software using Multiple Provers. Cryptology ePrint Archive (2025)."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477132.3483540"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/390016.808445"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_3_2_1_12_1","volume-title":"Proceedings of the 2020 USENIX Annual Technical Conference, USENIX ATC 2020","author":"Conway Alexander","year":"2020","unstructured":"Alexander Conway, Abhishek Gupta, Vijay Chidambaram, Martin Farach-Colton, Richard P. Spillane, Amy Tai, and Rob Johnson. 2020. SplinterDB: Closing the Bandwidth Gap for NVMe Key-Value Stores. In Proceedings of the 2020 USENIX Annual Technical Conference, USENIX ATC 2020, July 15-17, 2020, Ada Gavrilovska and Erez Zadok (Eds.). USENIX Association, 49--63. https:\/\/www.usenix.org\/conference\/atc20\/presentation\/conway"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.558708"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-17244-1_6"},{"volume-title":"Program Verification: Fundamental Issues in Computer Science","author":"Floyd Robert W","key":"e_1_3_2_1_15_1","unstructured":"Robert W Floyd. 1993. Assigning meanings to programs. In Program Verification: Fundamental Issues in Computer Science. Springer, 65--81."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656422"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"volume-title":"MiniRust: A core language for specifying Rust. Talk presented at the RustWeek NL","author":"Jung Ralf","key":"e_1_3_2_1_19_1","unstructured":"Ralf Jung. 2025. MiniRust: A core language for specifying Rust. Talk presented at the RustWeek NL. Utrecht, The Netherlands."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"volume-title":"The Rust Programming Language","author":"Klabnik Steve","key":"e_1_3_2_1_23_1","unstructured":"Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press, USA."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586037"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591283"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451167"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSEC.2022.3158196"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211968"},{"key":"e_1_3_2_1_31_1","volume-title":"ACE: Confidential Computing for Embedded RISC-V Systems. https:\/\/arxiv.org\/pdf\/2505.12995.","author":"Ozga Wojciech","year":"2025","unstructured":"Wojciech Ozga, Guerney D. H. Hunt, Michael V. Le, Gaeher Lennard, Avraham Shinnar, Elaine R. Palmer, Hani Jamjoom, and Silvio Dragone. 2025. ACE: Confidential Computing for Embedded RISC-V Systems. https:\/\/arxiv.org\/pdf\/2505.12995."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623652.3623668"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.262"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510457.3513031"}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Seoul Republic of Korea","acronym":"SOSP '25"},"container-title":["Proceedings of the 13th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768326","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:20:43Z","timestamp":1763054443000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764860.3768326"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,13]]},"references-count":35,"alternative-id":["10.1145\/3764860.3768326","10.1145\/3764860"],"URL":"https:\/\/doi.org\/10.1145\/3764860.3768326","relation":{},"subject":[],"published":{"date-parts":[[2025,10,13]]},"assertion":[{"value":"2025-10-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}