{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:14:43Z","timestamp":1770275683294,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,11,29]],"date-time":"2022-11-29T00:00:00Z","timestamp":1669680000000},"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":[[2022,11,29]]},"DOI":"10.1145\/3563822.3568015","type":"proceedings-article","created":{"date-parts":[[2022,12,1]],"date-time":"2022-12-01T21:17:50Z","timestamp":1669929470000},"page":"68-79","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Synchronous Programming and Refinement Types in Robotics: From Verification to Implementation"],"prefix":"10.1145","author":[{"given":"Jiawei","family":"Chen","sequence":"first","affiliation":[{"name":"University of Michigan at Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jos\u00e9 Luiz","family":"Vargas de Mendon\u00e7a","sequence":"additional","affiliation":[{"name":"University of Michigan at Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shayan","family":"Jalili","sequence":"additional","affiliation":[{"name":"University of Michigan at Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bereket","family":"Ayele","sequence":"additional","affiliation":[{"name":"Addis Ababa Institute of Technology, Ethiopia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bereket Ngussie","family":"Bekele","sequence":"additional","affiliation":[{"name":"Addis Ababa Institute of Technology, Ethiopia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhemin","family":"Qu","sequence":"additional","affiliation":[{"name":"University of Michigan at Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pranjal","family":"Sharma","sequence":"additional","affiliation":[{"name":"University of Michigan at Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tigist","family":"Shiferaw","sequence":"additional","affiliation":[{"name":"Addis Ababa Institute of Technology, Ethiopia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yicheng","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Michigan at Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Baptiste","family":"Jeannin","sequence":"additional","affiliation":[{"name":"University of Michigan at Ann Arbor, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,12]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57318-6_30"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728630"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_3"},{"key":"e_1_3_2_1_6_1","unstructured":"BeagleBoard. [n. d.]. Robot Control. https:\/\/github.com\/beagleboard\/librobotcontrol\/releases accessed 09\/12\/2022. \t\t\t\t  BeagleBoard. [n. d.]. Robot Control. https:\/\/github.com\/beagleboard\/librobotcontrol\/releases accessed 09\/12\/2022."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2018.2858016"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038664"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-79707-4_2"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192406"},{"key":"e_1_3_2_1_12_1","volume-title":"10th European Congress on Embedded Real Time Software and Systems (ERTS","author":"Bourbouh Hamza","year":"2020","unstructured":"Hamza Bourbouh , Pierre-Lo\u00efc Garoche , Thomas Loquen , \u00c9ric Noulard , and Claire Pagetti . 2020 . CoCoSim, a code generation framework for control\/command applications An overview of CoCoSim for multi-periodic discrete Simulink models . In 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020). Toulouse, France. https:\/\/hal.archives-ouvertes.fr\/hal-02441334 Hamza Bourbouh, Pierre-Lo\u00efc Garoche, Thomas Loquen, \u00c9ric Noulard, and Claire Pagetti. 2020. CoCoSim, a code generation framework for control\/command applications An overview of CoCoSim for multi-periodic discrete Simulink models. In 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020). Toulouse, France. https:\/\/hal.archives-ouvertes.fr\/hal-02441334"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062358"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461348"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97299"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/41625.41641"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_29"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3427763.3432350"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176887.1176899"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2017.8285623"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45309-1_16"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67531-2_11"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498701"},{"key":"e_1_3_2_1_26_1","unstructured":"Federal Highway Administration. 2014. Guidelines for the Use of Variable Speed Limit Systems in Wet Weather - Safety. https:\/\/safety.fhwa.dot.gov\/speedmgt\/ref_mats\/fhwasa12022\/chap_2.cfm accessed 08\/10\/2022. \t\t\t\t  Federal Highway Administration. 2014. Guidelines for the Use of Variable Speed Limit Systems in Wet Weather - Safety. https:\/\/safety.fhwa.dot.gov\/speedmgt\/ref_mats\/fhwasa12022\/chap_2.cfm accessed 08\/10\/2022."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428300"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA40945.2020.9196513"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.97300"},{"key":"e_1_3_2_1_32_1","volume-title":"Refinement Types: A Tutorial. arXiv:2010.07763 [cs] (Oct.","author":"Jhala Ranjit","year":"2020","unstructured":"Ranjit Jhala and Niki Vazou . 2020 . Refinement Types: A Tutorial. arXiv:2010.07763 [cs] (Oct. 2020). http:\/\/arxiv.org\/abs\/2010.07763 arXiv: 2010.07763. Ranjit Jhala and Niki Vazou. 2020. Refinement Types: A Tutorial. arXiv:2010.07763 [cs] (Oct. 2020). http:\/\/arxiv.org\/abs\/2010.07763 arXiv: 2010.07763."},{"key":"e_1_3_2_1_33_1","unstructured":"Temesghen Kahsai Hamza Bourbouh and Daniel Larraz. 2022. Zustre. https:\/\/github.com\/coco-team\/zustre accessed 09\/11\/2022. \t\t\t\t  Temesghen Kahsai Hamza Bourbouh and Daniel Larraz. 2022. Zustre. https:\/\/github.com\/coco-team\/zustre accessed 09\/11\/2022."},{"key":"e_1_3_2_1_34_1","unstructured":"LCM Project. [n. d.]. Lightweight Communications and Marshalling. https:\/\/lcm-proj.github.io\/index.html accessed 11\/22\/2021. \t\t\t\t  LCM Project. [n. d.]. Lightweight Communications and Marshalling. https:\/\/lcm-proj.github.io\/index.html accessed 11\/22\/2021."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21437-0_6"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SOSCYPS.2016.7580000"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2015.7170931"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039482"},{"key":"e_1_3_2_1_40_1","unstructured":"Open Robotics. [n. d.]. ROS - Robot Operating System. https:\/\/www.ros.org accessed 11\/22\/2021. \t\t\t\t  Open Robotics. [n. d.]. ROS - Robot Operating System. https:\/\/www.ros.org accessed 11\/22\/2021."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375602"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034811"},{"key":"e_1_3_2_1_44_1","unstructured":"The Coq Team. [n. d.]. The Coq Proof Assistant. https:\/\/coq.inria.fr\/ https:\/\/coq.inria.fr\/ accessed 09\/11\/2022. \t\t\t\t  The Coq Team. [n. d.]. The Coq Proof Assistant. https:\/\/coq.inria.fr\/ https:\/\/coq.inria.fr\/ accessed 09\/11\/2022."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633366"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628161"},{"key":"e_1_3_2_1_47_1","volume-title":"Ashcroft","author":"Wadge William W.","year":"1985","unstructured":"William W. Wadge and Edward A . Ashcroft . 1985 . Lucid, the Dataflow Programming Language. Academic Press London . http:\/\/prog.vub.ac.be\/~tjdhondt\/ESL\/Lucid_files\/Lucid, William W. Wadge and Edward A. Ashcroft. 1985. Lucid, the Dataflow Programming Language. Academic Press London. http:\/\/prog.vub.ac.be\/~tjdhondt\/ESL\/Lucid_files\/Lucid,"}],"event":{"name":"FTSCS '22: 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems","location":"Auckland New Zealand","acronym":"FTSCS '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563822.3568015","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563822.3568015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:07Z","timestamp":1750186807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563822.3568015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,29]]},"references-count":47,"alternative-id":["10.1145\/3563822.3568015","10.1145\/3563822"],"URL":"https:\/\/doi.org\/10.1145\/3563822.3568015","relation":{},"subject":[],"published":{"date-parts":[[2022,11,29]]},"assertion":[{"value":"2022-12-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}