{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T01:54:09Z","timestamp":1773194049989,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":81,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,3,30]],"date-time":"2025-03-30T00:00:00Z","timestamp":1743292800000},"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":[[2025,3,30]]},"DOI":"10.1145\/3689031.3696093","type":"proceedings-article","created":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T06:25:20Z","timestamp":1742970320000},"page":"76-93","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Efeu: generating efficient, verified, hybrid hardware\/software drivers for I2C devices"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4412-9004","authenticated-orcid":false,"given":"Daniel","family":"Schwyn","sequence":"first","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-5411-9785","authenticated-orcid":false,"given":"Zikai","family":"Liu","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8298-1126","authenticated-orcid":false,"given":"Timothy","family":"Roscoe","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,3,30]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"2","article-title":"Design and On-Orbit Performance of the Electrical Power System for the Quetzal-1 CubeSat","volume":"12","author":"Aguilar-Nadalini Aldo","year":"2023","unstructured":"Aldo Aguilar-Nadalini, Kuk H Chung, Cecilia Marsicovetere, Juan F Medrano, Emilio Miranda, V\u00edctor Ayerdi, and Luis Zea. 2023. Design and On-Orbit Performance of the Electrical Power System for the Quetzal-1 CubeSat. Journal of Small Satelites 12, 2 (May 2023), 1201--1229.","journal-title":"Journal of Small Satelites"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3262410"},{"key":"e_1_3_2_1_3_1","unstructured":"AMD 2012. LogiCORE IP AXI IIC bus interface data sheet. AMD."},{"key":"e_1_3_2_1_4_1","unstructured":"AMD 2022. Zynq UltraScale+ MPSoC Data Sheet: Overview (DS891). AMD. https:\/\/www.amd.com\/content\/dam\/xilinx\/support\/documents\/data_sheets\/ds891-zynq-ultrascale-plus-overview.pdf"},{"key":"e_1_3_2_1_5_1","unstructured":"Arm 2022. Learn the architecture - An introduction to AMBA AXI. Arm."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1965724.1965743"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04570-7_18"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12567-016-0138-0"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.46586\/tches.v2023.i2.1-23"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/502059.502042"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.1992"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/224841.225052"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/224486.224491"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3503222.3507742"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/998300.997169"},{"key":"e_1_3_2_1_17_1","unstructured":"Albert Danial. 2024. cloc: v2.00. GitHub. https:\/\/github.com\/AlDanial\/cloc"},{"key":"e_1_3_2_1_18_1","unstructured":"The Linux development community. 2024. Device-Tree bindings for I2C GPIO driver. https:\/\/www.kernel.org\/doc\/Documentation\/devicetree\/bindings\/i2c\/i2c-gpio.txt Accessed on 2024-05-12."},{"key":"e_1_3_2_1_19_1","unstructured":"The Linux development community. 2024. linux\/drivers\/i2c\/busses\/i2c-gpio.c at Linux v5.15. https:\/\/github.com\/torvalds\/linux\/blob\/v5.15\/drivers\/i2c\/busses\/i2c-gpio.c Accessed on 2024-05-12."},{"key":"e_1_3_2_1_20_1","unstructured":"The Linux development community. 2024. linux\/drivers\/media\/i2c\/ks0127.c at Linux v5.15. https:\/\/github.com\/torvalds\/linux\/blob\/v5.15\/drivers\/media\/i2c\/ks0127.c Accessed on 2024-05-08."},{"key":"e_1_3_2_1_21_1","unstructured":"The Linux development community. 2024. linux\/drivers\/pci\/quirks.c at Linux v6.9. https:\/\/github.com\/torvalds\/linux\/blob\/v6.9\/drivers\/pci\/quirks.c Accessed on 2024-05-17."},{"key":"e_1_3_2_1_22_1","unstructured":"The OpenBMC development community. 2024. OpenBMC. https:\/\/github.com\/openbmc\/openbmc Accessed: 2022-09-08."},{"key":"e_1_3_2_1_23_1","volume-title":"Promela Manual page","author":"The SPIN","unstructured":"The SPIN development community. 2012. Promela Manual page. http:\/\/spinroot.com\/spin\/Man\/promela.html Accessed: 2023-08-02."},{"key":"e_1_3_2_1_24_1","unstructured":"Shuying Fan and Supriya Velagapudi. 2023. Implementing Next-Generation Data Center Platform Management Using Agilex 3 and Agilex 5 Devices. https:\/\/www.intel.com\/content\/www\/us\/en\/content-details\/787067\/implementing-next-generation-data-center-platform-management-using-agilex-5-devices.html Accessed on 2024-05-21."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593856.3595903"},{"key":"e_1_3_2_1_26_1","unstructured":"A. Ganapathi Viji Ganapathi and D. Patterson. 2006. Windows XP Kernel Crash Analysis. In LiSA. USENIX Association Berkeley CA USA 149--159. https:\/\/www.usenix.org\/legacy\/events\/lisa06\/tech\/ganapathi.html"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/WF-"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_8"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-84629-9_10"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4218\/etrij.11.0110.0654"},{"key":"e_1_3_2_1_32_1","unstructured":"Ke Jiang. 2009. Model Checking C Programs by Translating C to Promela. Master's thesis. Uppsala Universitet Uppsala Sweden. http:\/\/www.diva- portal.org\/smash\/get\/diva2:235718\/FULLTEXT01.pdf"},{"key":"e_1_3_2_1_33_1","unstructured":"kaedros. 2022. Raspberry Pi I2C clock-stretching bug GitHub Issue. https:\/\/github.com\/raspberrypi\/linux\/issues\/4884 Accessed on 2024-09-05."},{"key":"e_1_3_2_1_34_1","unstructured":"Keysight Technologies Inc. 2020. Keysight InfiniiVision 3000T X-Series Oscilloscopes User's Guide. Accessed on 2023-08-08."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_12"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2189750.2151011"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-60750-065-0-105"},{"key":"e_1_3_2_1_39_1","volume-title":"The art of computer programming","author":"Knuth Donald","unstructured":"Donald E.Knuth. 1997. The art of computer programming, volume 1 (3rd ed.): fundamental algorithms. Addison Wesley Longman Publishing Co., Inc., USA.","edition":"3"},{"key":"e_1_3_2_1_40_1","unstructured":"Hans-J\u00fcrgen Koch. 2006. https:\/\/www.kernel.org\/doc\/html\/latest\/driver-api\/uio-howto.html Accessed on 2024-05-21."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_44"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340466"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.3929\/ethz-b-000632755"},{"key":"e_1_3_2_1_46_1","volume-title":"24th International Workshop on Logic & Synthesis. IWLS","author":"Long Jiang","year":"2016","unstructured":"Jiang Long and Robert Brayton. 2016. A Simple C to Verilog Compilation Procedure for Hardware\/Software Verification. In 24th International Workshop on Logic & Synthesis. IWLS, Mountain View, CA, USA, 99--106."},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439916"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10256-6"},{"key":"e_1_3_2_1_49_1","volume-title":"Raspberry Pi I2C clock-stretching bug","author":"Advamation","unstructured":"Advamation mechatronic. 2013. Raspberry Pi I2C clock-stretching bug. http:\/\/www.advamation.com\/knowhow\/raspberrypi\/rpi-i2c-bug.html Accessed on 2023-11-30."},{"key":"e_1_3_2_1_50_1","volume-title":"Fourth Symposium on Operating Systems Design and Implementation (OSDI 2000","author":"M\u00e9rillon Fabrice","year":"2000","unstructured":"Fabrice M\u00e9rillon, Laurent R\u00e9veill\u00e8re, Charles Consel, Renaud Marlet, and Gilles Muller. 2000. Devil: An {IDL} for Hardware Programming. In Fourth Symposium on Operating Systems Design and Implementation (OSDI 2000). USENIX Association, San Diego, CA, 14 pages. https:\/\/www.usenix.org\/conference\/osdi-2000\/devil-idl-hardware-programming"},{"key":"e_1_3_2_1_51_1","unstructured":"Microchip 2021. 24AA512\/24LC512\/24FC512 512K I2C Serial EEPROM. Microchip."},{"key":"e_1_3_2_1_52_1","unstructured":"NIST. 2024. NVD - CVE-2024-26593. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2024-26593 Accessed on 2024-05-05."},{"key":"e_1_3_2_1_53_1","unstructured":"NXP Semiconductors 2021. I2C-bus specification and user manual. NXP Semiconductors."},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011246731756"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/288548.289067"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623759.3624544"},{"key":"e_1_3_2_1_57_1","unstructured":"Nadav Rotem. 2010. C-to-Verilog.Com: High-Level Synthesis Using LLVM."},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629583"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685101"},{"key":"e_1_3_2_1_60_1","unstructured":"Samsung Electronics 1998. KS0127 Data Sheet. Samsung Electronics. https:\/\/alltransistors.com\/superdatasheets\/_pdf\/09\/ks0127.pdf"},{"key":"e_1_3_2_1_61_1","unstructured":"Samsung Electronics 2000. KS0127B Data Sheet. Samsung Electronics. https:\/\/alltransistors.com\/superdatasheets\/_pdf\/09\/ks0127b.pdf"},{"key":"e_1_3_2_1_62_1","unstructured":"SBS Implementers Forum. 2000. System Management Bus (SMBus) Specification. Technical Report. http:\/\/smbus.org\/specs\/index.html"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950382"},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462183"},{"key":"e_1_3_2_1_65_1","unstructured":"Antmicro Open Source. 2020. ARTIX DC-SCM. https:\/\/opensource.antmicro.com\/projects\/artix-dc-scm\/ Accessed on 2024-05-16."},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086230"},{"key":"e_1_3_2_1_67_1","unstructured":"System Management Interface Forum Inc. 2015. PMBus Power System Management Protocol Specification Part I - General Requirements Transport And Electrical Interface. Technical Report. https:\/\/pmbusprod.wpenginepowered.com\/wp-content\/uploads\/2022\/01\/PMBus-Specification-Rev-1-3-1-Part-I-20150313.pdf"},{"key":"e_1_3_2_1_68_1","unstructured":"System Management Interface Forum Inc. 2015. PMBus Power System Management Protocol Specification Part II - Command Language. Technical Report. https:\/\/pmbusprod.wpenginepowered.com\/wp-content\/uploads\/2022\/01\/PMBus-Specification-Rev-1-3-1-Part-N-20150313.pdf"},{"key":"e_1_3_2_1_69_1","volume-title":"Clang: C Language Family Frontend for LLVM. https:\/\/clang.llvm.org\/ Accessed on 2024-05-21.","author":"Team The Clang","year":"2024","unstructured":"The Clang Team. 2024. Clang: C Language Family Frontend for LLVM. https:\/\/clang.llvm.org\/ Accessed on 2024-05-21."},{"key":"e_1_3_2_1_70_1","volume-title":"Clang: Clang::DiagnosticsEngine Class Reference. https:\/\/clang.llvm.org\/doxygen\/classclang_1_1DiagnosticsEngine.html Accessed on 2024-05-21.","author":"Team The Clang","year":"2024","unstructured":"The Clang Team. 2024. Clang: Clang::DiagnosticsEngine Class Reference. https:\/\/clang.llvm.org\/doxygen\/classclang_1_1DiagnosticsEngine.html Accessed on 2024-05-21."},{"key":"e_1_3_2_1_71_1","unstructured":"The Clang Team. 2024. clang: clang::Rewriter Class Reference. https:\/\/clang.llvm.org\/doxygen\/classclang_1_1Rewriter.html Accessed on 2024-05-21."},{"key":"e_1_3_2_1_72_1","unstructured":"The Clang Team. 2024. ClangFormat. https:\/\/clang.llvm.org\/docs\/ClangFormat.html"},{"key":"e_1_3_2_1_73_1","unstructured":"The LLVM development community. 2024. The LLVM Compiler Infrastructure Project. https:\/\/llvm.org\/ Accessed on 2024-05-21."},{"key":"e_1_3_2_1_74_1","unstructured":"The LLVM development community. 2024. LLVM Language Reference Manual. https:\/\/llvm.org\/docs\/LangRef.html Accessed on 2024-05-21."},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00209910"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2015.2455034"},{"key":"e_1_3_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623759.3624545"},{"key":"e_1_3_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/MPEL.2014.2330492"},{"key":"e_1_3_2_1_79_1","unstructured":"Xilinx 2020. Zynq UltraScale+ Device Technical Reference Manual. Xilinx."},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/11802167_75"},{"key":"e_1_3_2_1_81_1","volume-title":"Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI '06)","author":"Zhou Feng","year":"2006","unstructured":"Feng Zhou, Jeremy Condit, Zachary Anderson, Ilya Bagrak, Rob Ennals, Matthew Harren, George Necula, and Eric Brewer. 2006. SafeDrive: Safe and Recoverable Extensions Using Language-Based Techniques. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation (OSDI '06). USENIX Association, USA, 45--60."}],"event":{"name":"EuroSys '25: Twentieth European Conference on Computer Systems","location":"Rotterdam Netherlands","acronym":"EuroSys '25","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the Twentieth European Conference on Computer Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689031.3696093","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689031.3696093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T11:22:39Z","timestamp":1755775359000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689031.3696093"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,30]]},"references-count":81,"alternative-id":["10.1145\/3689031.3696093","10.1145\/3689031"],"URL":"https:\/\/doi.org\/10.1145\/3689031.3696093","relation":{},"subject":[],"published":{"date-parts":[[2025,3,30]]},"assertion":[{"value":"2025-03-30","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}