{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:09:20Z","timestamp":1770271760184,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T00:00:00Z","timestamp":1701302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1901136"],"award-info":[{"award-number":["1901136"]}],"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":[[2023,11,30]]},"DOI":"10.1145\/3611643.3613863","type":"proceedings-article","created":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T23:14:38Z","timestamp":1701386078000},"page":"1903-1913","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["PropProof: Free Model-Checking Harnesses from PBT"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9274-8953","authenticated-orcid":false,"given":"Yoshiki","family":"Takashima","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,11,30]]},"reference":[{"key":"e_1_3_2_2_1_1","unstructured":"2023. crates.io: Rust Package Registry. https:\/\/crates.io\/"},{"key":"e_1_3_2_2_2_1","unstructured":"2023. Explaining BSON With Examples. https:\/\/www.mongodb.com\/basics\/bson"},{"key":"e_1_3_2_2_3_1","unstructured":"2023. Servo. https:\/\/servo.org\/"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"e_1_3_2_2_5_1","volume-title":"Proceedings of SAT Race 2019","author":"Biere Armin","year":"2019","unstructured":"Armin Biere. 2019. CADICAL at the SAT Race 2019. In Proceedings of SAT Race 2019. B-2019-1, 8\u20139."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351266"},{"key":"e_1_3_2_2_8_1","volume-title":"Creusot: a Foundry for the Deductive Verification of Rust Programs","author":"Denis Xavier","unstructured":"Xavier Denis, Jacques-Henri Jourdan, and Claude March\u00e9. 2022. Creusot: a Foundry for the Deductive Verification of Rust Programs. Springer Verlag. https:\/\/hal.inria.fr\/hal-03737878"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_12"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31862-0_25"},{"key":"e_1_3_2_2_11_1","unstructured":"Wedson Almeida Filho. 2021. Rust in the Linux kernel. https:\/\/security.googleblog.com\/2021\/04\/rust-in-linux-kernel.html"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3547647"},{"key":"e_1_3_2_2_13_1","unstructured":"Matthew Hughes. 2021. The Fuchsia is now. Google\u2019s operating system lands on real-world consumer devices starting with 2018\u2019s Nest Hub. https:\/\/www.theregister.com\/2021\/05\/25\/google_fuchsia_lands_on_nest\/"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2207.04034"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3462205"},{"key":"e_1_3_2_2_19_1","unstructured":"Shane Miller and Carl Lerche. 2022. Sustainability with Rust | AWS Open Source Blog. https:\/\/aws.amazon.com\/blogs\/opensource\/sustainability-with-rust\/ Section: Developer Tools."},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_22"},{"key":"e_1_3_2_2_21_1","volume-title":"Towards making formal methods normal: meeting developers where they are. arxiv:2010.16345. https:\/\/research.google\/pubs\/pub49713\/ Accepted at HATRA","author":"Reid Alastair","year":"2020","unstructured":"Alastair Reid, Luke Church, Shaked Flur, Sarah de Haas, Maritza Johnson, and Ben Laurie. 2020. Towards making formal methods normal: meeting developers where they are. arxiv:2010.16345. https:\/\/research.google\/pubs\/pub49713\/ Accepted at HATRA 2020."},{"key":"e_1_3_2_2_22_1","unstructured":"Daniel Schwartz-Narbonne. 2022. Use Kani action in CI by danielsn \u00b7 Pull Request #1556 \u00b7 aws\/s2n-quic. https:\/\/github.com\/aws\/s2n-quic\/pull\/1556"},{"key":"e_1_3_2_2_23_1","unstructured":"Yoshiki Takashima. 2022. Return Error If Overflow by YoshikiTakashima \u00b7 Pull Request #686 \u00b7 tokio-rs\/prost. https:\/\/github.com\/tokio-rs\/prost\/pull\/686"},{"key":"e_1_3_2_2_24_1","unstructured":"Yoshiki Takashima. 2023. Add Kani to CI. by YoshikiTakashima \u00b7 Pull Request #798 \u00b7 tokio-rs\/prost. https:\/\/github.com\/tokio-rs\/prost\/pull\/798"},{"key":"e_1_3_2_2_25_1","unstructured":"The proptest developers. 2023. Proptest. https:\/\/github.com\/proptest-rs\/proptest original-date: 2017-06-18T17:38:03Z."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510457.3513031"},{"key":"e_1_3_2_2_27_1","unstructured":"Steven J. Vaughan-Nichols. [n.d.]. Linux kernel 6.1: Rusty release could be a game-changer. https:\/\/www.theregister.com\/2022\/12\/09\/linux_kernel_61_column\/"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485522"}],"event":{"name":"ESEC\/FSE '23: 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"San Francisco CA USA","acronym":"ESEC\/FSE '23","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3613863","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611643.3613863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:10Z","timestamp":1750178230000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3613863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,30]]},"references-count":28,"alternative-id":["10.1145\/3611643.3613863","10.1145\/3611643"],"URL":"https:\/\/doi.org\/10.1145\/3611643.3613863","relation":{},"subject":[],"published":{"date-parts":[[2023,11,30]]},"assertion":[{"value":"2023-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}