{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:26:06Z","timestamp":1750220766804,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,6,16]],"date-time":"2020-06-16T00:00:00Z","timestamp":1592265600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Emergence(s) program of the City of Paris"},{"name":"Inria IPL ZEP"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,6,16]]},"DOI":"10.1145\/3372799.3394365","type":"proceedings-article","created":{"date-parts":[[2020,5,29]],"date-time":"2020-05-29T15:04:12Z","timestamp":1590764652000},"page":"85-96","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Intermittent Computing with Peripherals, Formally Verified"],"prefix":"10.1145","author":[{"given":"Gautier","family":"Berthou","sequence":"first","affiliation":[{"name":"Univ. Lyon, INSA-Lyon, Inria, CITI, Villeurbanne, France"}]},{"given":"Pierre-\u00c9variste","family":"Dagand","sequence":"additional","affiliation":[{"name":"Sorbonne Universit\u00e9, CNRS, Inria Paris, LIP6, Paris, France"}]},{"given":"Delphine","family":"Demange","sequence":"additional","affiliation":[{"name":"Univ Rennes, Inria, CNRS, IRISA, Rennes, France"}]},{"given":"R\u00e9mi","family":"Oudin","sequence":"additional","affiliation":[{"name":"Sorbonne Universit\u00e9, CNRS, Inria Paris, LIP6, Paris, France"}]},{"given":"Tanguy","family":"Risset","sequence":"additional","affiliation":[{"name":"Univ. Lyon, INSA-Lyon, Inria, CITI, Villeurbanne, France"}]}],"member":"320","published-online":{"date-parts":[[2020,6,16]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3316482.3326357"},{"key":"e_1_3_2_2_2_1","first-page":"172","article-title":"RESTOP","volume":"18","author":"Arreola Alberto Rodriguez","year":"2018","unstructured":"Alberto Rodriguez Arreola , Domenico Balsamo , Geoff V. Merrett , and Alex S. Weddell . 2018 . RESTOP : Retaining External Peripheral State in Intermittently-Powered Sensor Systems. Sensors , Vol. 18 , 1 (2018), 172 . https:\/\/doi.org\/10.3390\/s18010172 10.3390\/s18010172 Alberto Rodriguez Arreola, Domenico Balsamo, Geoff V. Merrett, and Alex S. Weddell. 2018. RESTOP: Retaining External Peripheral State in Intermittently-Powered Sensor Systems. Sensors, Vol. 18, 1 (2018), 172. https:\/\/doi.org\/10.3390\/s18010172","journal-title":"Retaining External Peripheral State in Intermittently-Powered Sensor Systems. Sensors"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LES.2014.2371494"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Gautier Berthou Pierre-Evariste Dagand Delphine Demange R\u00e9mi Oudin and Tanguy Risset. 2020. Intermittent Computing with Peripherals Formally Verified -- Companion Coq Development. https:\/\/gabertho.gitlabpages.inria.fr\/icp-model\/  Gautier Berthou Pierre-Evariste Dagand Delphine Demange R\u00e9mi Oudin and Tanguy Risset. 2020. Intermittent Computing with Peripherals Formally Verified -- Companion Coq Development. https:\/\/gabertho.gitlabpages.inria.fr\/icp-model\/","DOI":"10.1145\/3372799.3394365"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/GIOTS.2017.8016243"},{"key":"e_1_3_2_2_6_1","first-page":"9","article-title":"Sytare","volume":"68","author":"Berthou Gautier","year":"2019","unstructured":"Gautier Berthou , Tristan Delizy , Kevin Marquet , Tanguy Risset , and Guillaume Salagnac . 2019 . Sytare : A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems. IEEE Trans. Comput. , Vol. 68 , 9 (Sep. 2019), 1390--1403. Gautier Berthou, Tristan Delizy, Kevin Marquet, Tanguy Risset, and Guillaume Salagnac. 2019. Sytare: A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems. IEEE Trans. Comput., Vol. 68, 9 (Sep. 2019), 1390--1403.","journal-title":"A Lightweight Kernel for NVRAM-Based Transiently-Powered Systems. IEEE Trans. Comput."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3055031.3055082"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3241624.2926704"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3356250.3360033"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2714064.2660224"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2831090.2831111"},{"key":"e_1_3_2_2_14_1","volume-title":"Non-Volatile Memories. SIGARCH Comput. Archit. News","volume":"39","author":"Coburn Joel","year":"2011","unstructured":"Joel Coburn , Adrian M. Caulfield , Ameen Akel , Laura M. Grupp , Rajesh K. Gupta , Ranjit Jhala , and Steven Swanson . 2011 . NV-Heaps: Making Persistent Objects Fast and Safe with next-Generation , Non-Volatile Memories. SIGARCH Comput. Archit. News , Vol. 39 , 1 (March 2011), 105--118. Joel Coburn, Adrian M. Caulfield, Ameen Akel, Laura M. Grupp, Rajesh K. Gupta, Ranjit Jhala, and Steven Swanson. 2011. NV-Heaps: Making Persistent Objects Fast and Safe with next-Generation, Non-Volatile Memories. SIGARCH Comput. Archit. News, Vol. 39, 1 (March 2011), 105--118."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3173162.3173210"},{"volume-title":"Formal Methods -- The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N","author":"Derrick John","key":"e_1_3_2_2_16_1","unstructured":"John Derrick , Simon Doherty , Brijesh Dongol , Gerhard Schellhorn , and Heike Wehrheim . 2019 Verifying Correctness of Persistent Concurrent Data Structures . In Formal Methods -- The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N . Oliveira (Eds.). Springer International Publishing , Cham, Switzerland , 179--195. John Derrick, Simon Doherty, Brijesh Dongol, Gerhard Schellhorn, and Heike Wehrheim. 2019 Verifying Correctness of Persistent Concurrent Data Structures. In Formal Methods -- The Next 30 Years, Maurice H. ter Beek, Annabelle McIver, and Jos\u00e9 N. Oliveira (Eds.). Springer International Publishing, Cham, Switzerland, 179--195."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131672.3131673"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140659.3080238"},{"key":"e_1_3_2_2_19_1","volume-title":"Scott","author":"Izraelevitz Joseph","year":"2016","unstructured":"Joseph Izraelevitz , Hammurabi Mendes , and Michael L . Scott . 2016 . Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. In Distributed Computing, Cyril Gavoille and David Ilcinkas (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg, 313--327. Joseph Izraelevitz, Hammurabi Mendes, and Michael L. Scott. 2016. Linearizability of Persistent Memory Objects Under a Full-System-Crash Failure Model. In Distributed Computing, Cyril Gavoille and David Ilcinkas (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 313--327."},{"key":"e_1_3_2_2_20_1","volume-title":"Woo Suk Lee, and Vijay Raghunathan","author":"Jayakumar Hrishikesh","year":"2015","unstructured":"Hrishikesh Jayakumar , Arnab Raha , Woo Suk Lee, and Vijay Raghunathan . 2015 . QuickRecall: A HW\/SW Approach for Computing across Power Cycles in Transiently Powered Computers. JETC , Vol. 12 , 1 (2015), 8:1--8:19. https:\/\/doi.org\/10.1145\/2700249 10.1145\/2700249 Hrishikesh Jayakumar, Arnab Raha, Woo Suk Lee, and Vijay Raghunathan. 2015. QuickRecall: A HW\/SW Approach for Computing across Power Cycles in Transiently Powered Computers. JETC, Vol. 12, 1 (2015), 8:1--8:19. https:\/\/doi.org\/10.1145\/2700249"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837648"},{"key":"e_1_3_2_2_22_1","unstructured":"Leslie Lamport. 2008. Computation and state machines.  Leslie Lamport. 2008. Computation and state machines."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSSC.2012.2221233"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737978"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0060"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133920"},{"key":"e_1_3_2_2_28_1","volume-title":"Adaptive Dynamic Checkpointing for Safe Efficient Intermittent Computing. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018","author":"Maeng Kiwan","year":"2018","unstructured":"Kiwan Maeng and Brandon Lucia . 2018 . Adaptive Dynamic Checkpointing for Safe Efficient Intermittent Computing. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018 , Carlsbad, CA, USA, October 8--10 , 2018. USENIX Association, Carlsbad, CA, 129--144. Kiwan Maeng and Brandon Lucia. 2018. Adaptive Dynamic Checkpointing for Safe Efficient Intermittent Computing. In 13th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2018, Carlsbad, CA, USA, October 8--10, 2018. USENIX Association, Carlsbad, CA, 129--144."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314613"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2618128.2618136"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950386"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314583"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIM.2008.925019"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3237009.3237027"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360609"},{"key":"#cr-split#-e_1_3_2_2_36_1.1","unstructured":"The Coq Development Team. 2018. The Coq Proof Assistant version 8.8.0. https:\/\/doi.org\/10.5281\/zenodo.1219885 10.5281\/zenodo.1219885"},{"key":"#cr-split#-e_1_3_2_2_36_1.2","unstructured":"The Coq Development Team. 2018. The Coq Proof Assistant version 8.8.0. https:\/\/doi.org\/10.5281\/zenodo.1219885"},{"key":"e_1_3_2_2_37_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016","author":"van der Woude Joel","year":"2016","unstructured":"Joel van der Woude and Matthew Hicks . 2016 . Intermittent Computation without Hardware Support or Programmer Intervention . In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016 , Savannah, GA, USA, November 2--4 , 2016. USENIX Association, Savannah, GA, 17--32. Joel van der Woude and Matthew Hicks. 2016. Intermittent Computation without Hardware Support or Programmer Intervention. In 12th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2016, Savannah, GA, USA, November 2--4, 2016. USENIX Association, Savannah, GA, 17--32."}],"event":{"name":"LCTES '20: 21st ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGBED ACM Special Interest Group on Embedded Systems"],"location":"London United Kingdom","acronym":"LCTES '20"},"container-title":["The 21st ACM SIGPLAN\/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372799.3394365","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372799.3394365","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372799.3394365"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,6,16]]},"references-count":38,"alternative-id":["10.1145\/3372799.3394365","10.1145\/3372799"],"URL":"https:\/\/doi.org\/10.1145\/3372799.3394365","relation":{},"subject":[],"published":{"date-parts":[[2020,6,16]]},"assertion":[{"value":"2020-06-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}