{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T10:38:07Z","timestamp":1791455887530,"version":"4.3.4"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,20]],"date-time":"2021-11-20T00:00:00Z","timestamp":1637366400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,20]]},"DOI":"10.1145\/3487212.3487347","type":"proceedings-article","created":{"date-parts":[[2021,12,21]],"date-time":"2021-12-21T20:01:45Z","timestamp":1640116905000},"page":"89-97","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Verified functional programming of an IoT operating system's bootloader"],"prefix":"10.1145","author":[{"given":"Shenghao","family":"Yuan","sequence":"first","affiliation":[{"name":"INRIA, IRISA, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jean-Pierre","family":"Talpin","sequence":"additional","affiliation":[{"name":"INRIA, IRISA, Rennes, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2021,12,21]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Verified Software Toolchain. In European Symposium on Programming","author":"Appel Andrew W.","year":"2011","unstructured":"Andrew W. Appel . 2011 . Verified Software Toolchain. In European Symposium on Programming ( Saarbr\u00fccken, Germany) (ESOP'11\/ETAPS'11). Springer-Verlag, Berlin, Heidelberg, 1--17. Andrew W. Appel. 2011. Verified Software Toolchain. In European Symposium on Programming (Saarbr\u00fccken, Germany) (ESOP'11\/ETAPS'11). Springer-Verlag, Berlin, Heidelberg, 1--17."},{"key":"e_1_3_2_1_2_1","unstructured":"ARM. 2021. Arm Trusted Firmware. https:\/\/github.com\/ARM-software\/arm-trusted-firmware  ARM. 2021. Arm Trusted Firmware. https:\/\/github.com\/ARM-software\/arm-trusted-firmware"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290384"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/JIOT.2018.2815038"},{"key":"e_1_3_2_1_5_1","volume-title":"Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2013. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions . Springer Science & Business Media , Berlin, Heidelberg . Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media, Berlin, Heidelberg."},{"key":"e_1_3_2_1_6_1","volume-title":"Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium (USENIX Security 17)","author":"Bond Barry","year":"2017","unstructured":"Barry Bond , Chris Hawblitzel , Manos Kapritsos , K. Rustan M. Leino , Jacob R. Lorch , Bryan Parno , Ashay Rane , Srinath Setty , and Laure Thompson . 2017 . Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium (USENIX Security 17) . USENIX Association, Vancouver, BC, 917--934. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond Barry Bond, Chris Hawblitzel, Manos Kapritsos, K. Rustan M. Leino, Jacob R. Lorch, Bryan Parno, Ashay Rane, Srinath Setty, and Laure Thompson. 2017. Vale: Verifying High-Performance Cryptographic Assembly Code. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC, 917--934. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/bond"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"e_1_3_2_1_9_1","volume-title":"25th USENIX Security Symposium USENIX Security 16)","author":"Costan Victor","year":"2016","unstructured":"Victor Costan , Ilia Lebedev , and Srinivas Devadas . 2016 . Sanctum: Minimal hardware extensions for strong software isolation . In 25th USENIX Security Symposium USENIX Security 16) . USENIX Association, Austin, TX, 857--874. Victor Costan, Ilia Lebedev, and Srinivas Devadas. 2016. Sanctum: Minimal hardware extensions for strong software isolation. In 25th USENIX Security Symposium USENIX Security 16). USENIX Association, Austin, TX, 857--874."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_6"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290376"},{"key":"e_1_3_2_1_12_1","unstructured":"GOOGLE. 2021. Verifying Boot. https:\/\/source.android.com\/security\/verifiedboot\/verified-boot.html  GOOGLE. 2021. Verifying Boot. https:\/\/source.android.com\/security\/verifiedboot\/verified-boot.html"},{"key":"e_1_3_2_1_13_1","unstructured":"MIT PLV Group. 2021. riscv-coq:RISC-V Specification in Coq. https:\/\/github.com\/mit-plv\/riscv-coq  MIT PLV Group. 2021. riscv-coq:RISC-V Specification in Coq. https:\/\/github.com\/mit-plv\/riscv-coq"},{"key":"e_1_3_2_1_14_1","unstructured":"hacspec. 2021. A specification language for crypto primitives in Rust. https:\/\/github.com\/hacspec\/hacspec  hacspec. 2021. A specification language for crypto primitives in Rust. https:\/\/github.com\/hacspec\/hacspec"},{"key":"e_1_3_2_1_15_1","unstructured":"Inria. 2021. RIOT-fp. https:\/\/future-proof-iot.github.io\/RIOT-fp\/about  Inria. 2021. RIOT-fp. https:\/\/future-proof-iot.github.io\/RIOT-fp\/about"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_1_19_1","unstructured":"Xavier Leroy. 2020. The CompCert C verified compiler: Documentation and user's manual. Intern report. Inria. 1--78 pages.  Xavier Leroy. 2020. The CompCert C verified compiler: Documentation and user's manual. Intern report. Inria. 1--78 pages."},{"key":"e_1_3_2_1_20_1","unstructured":"ARM Limited. 2016. ARM Compiler armasm User Guide v5.06. https:\/\/developer.arm.com\/documentation\/dui0473\/m  ARM Limited. 2016. ARM Compiler armasm User Guide v5.06. https:\/\/developer.arm.com\/documentation\/dui0473\/m"},{"key":"e_1_3_2_1_21_1","volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C Paulson , and Markus Wenzel . 2002. Isabelle\/HOL : a proof assistant for higher-order logic . Vol. 2283 . Springer Science & Business Media , Berlin, Heidelberg . Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Vol. 2283. Springer Science & Business Media, Berlin, Heidelberg."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110261"},{"key":"e_1_3_2_1_23_1","volume-title":"BootStomp: On the Security of Bootloaders in Mobile Devices. In 26th USENIX Security Symposium (USENIX Security 17)","author":"Redini Nilo","year":"2017","unstructured":"Nilo Redini , Aravind Machiry , Dipanjan Das , Yanick Fratantonio , Antonio Bianchi , Eric Gustafson , Yan Shoshitaishvili , Christopher Kruegel , and Giovanni Vigna . 2017 . BootStomp: On the Security of Bootloaders in Mobile Devices. In 26th USENIX Security Symposium (USENIX Security 17) . USENIX Association, Vancouver, BC, 781--798. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/redini Nilo Redini, Aravind Machiry, Dipanjan Das, Yanick Fratantonio, Antonio Bianchi, Eric Gustafson, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2017. BootStomp: On the Security of Bootloaders in Mobile Devices. In 26th USENIX Security Symposium (USENIX Security 17). USENIX Association, Vancouver, BC, 781--798. https:\/\/www.usenix.org\/conference\/usenixsecurity17\/technical-sessions\/presentation\/redini"},{"key":"e_1_3_2_1_24_1","unstructured":"RIoT. 2021. RIOT-OS. https:\/\/github.com\/RIOT-OS\/RIOT  RIoT. 2021. RIOT-OS. https:\/\/github.com\/RIOT-OS\/RIOT"},{"key":"e_1_3_2_1_25_1","unstructured":"RIoT. 2021. RIOT-rs. https:\/\/github.com\/future-proof-iot\/RIOT-rs  RIoT. 2021. RIOT-rs. https:\/\/github.com\/future-proof-iot\/RIOT-rs"},{"key":"e_1_3_2_1_26_1","unstructured":"RIoT. 2021. riotboot. https:\/\/github.com\/RIOT-OS\/RIOT\/tree\/master\/bootloaders\/riotboot  RIoT. 2021. riotboot. https:\/\/github.com\/RIOT-OS\/RIOT\/tree\/master\/bootloaders\/riotboot"},{"key":"e_1_3_2_1_27_1","unstructured":"RIoT. 2021. riotboot-rs. https:\/\/github.com\/kaspar030\/riotboot-rs  RIoT. 2021. riotboot-rs. https:\/\/github.com\/kaspar030\/riotboot-rs"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034811"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2019.8715067"},{"key":"e_1_3_2_1_32_1","unstructured":"FStar Team. 2021. KreMLin. https:\/\/github.com\/FStarLang\/kremlin  FStar Team. 2021. KreMLin. https:\/\/github.com\/FStarLang\/kremlin"},{"key":"e_1_3_2_1_33_1","unstructured":"The Coreboot Development Team. 2021. Coreboot. https:\/\/www.coreboot.org\/  The Coreboot Development Team. 2021. Coreboot. https:\/\/www.coreboot.org\/"},{"key":"e_1_3_2_1_34_1","unstructured":"Shenghao YUAN and Jean-Pierre Talpin. 2021. verified riotboot in FStar. https:\/\/gitlab.inria.fr\/syuan\/verified-riotboot  Shenghao YUAN and Jean-Pierre Talpin. 2021. verified riotboot in FStar. https:\/\/gitlab.inria.fr\/syuan\/verified-riotboot"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.23919\/PEMWN50727.2020.9293081"}],"event":{"name":"MEMOCODE '21: 19th ACM-IEEE International Conference on Formal Methods and Models for System Design","location":"Virtual Event China","acronym":"MEMOCODE '21","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","SIGDA ACM Special Interest Group on Design Automation","IEEE CAS","IEEE CEDA"]},"container-title":["Proceedings of the 19th ACM-IEEE International Conference on Formal Methods and Models for System Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487212.3487347","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3487212.3487347","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:47Z","timestamp":1750191527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3487212.3487347"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,20]]},"references-count":32,"alternative-id":["10.1145\/3487212.3487347","10.1145\/3487212"],"URL":"https:\/\/doi.org\/10.1145\/3487212.3487347","relation":{},"subject":[],"published":{"date-parts":[[2021,11,20]]},"assertion":[{"value":"2021-12-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}