{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:37:41Z","timestamp":1767897461648,"version":"3.49.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2020,11,13]],"date-time":"2020-11-13T00:00:00Z","timestamp":1605225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["1629949, 1544901"],"award-info":[{"award-number":["1629949, 1544901"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["1846354"],"award-info":[{"award-number":["1846354"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"<jats:p>A robot\u2019s code needs to sense the environment, control the hardware, and communicate with other robots. Current programming languages do not provide suitable abstractions that are independent of hardware platforms. Currently, developing robot applications requires detailed knowledge of signal processing, control, path planning, network protocols, and various platform-specific details. Further, porting applications across hardware platforms remains tedious. We present Koord\u2014a domain specific language for distributed robotics\u2014which abstracts platform-specific functions for sensing, communication, and low-level control. Koord makes the platform-independent control and coordination code portable and modularly verifiable. Koord raises the level of abstraction in programming by providing distributed shared memory for coordination and port interfaces for sensing and control. We have developed the formal executable semantics of Koord in the K framework. With this symbolic execution engine, we can identify assumptions (proof obligations) needed for gaining high assurance from Koord applications. We illustrate the power of Koord through three applications: formation flight, distributed delivery, and distributed mapping. We also use the three applications to demonstrate how platform-independent proof obligations can be discharged using the Koord Prover while platform-specific proof obligations can be checked by verifying the obligations using physics-based models and hybrid verification tools.<\/jats:p>","DOI":"10.1145\/3428300","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Koord: a language for programming and verifying distributed robotics application"],"prefix":"10.1145","volume":"4","author":[{"given":"Ritwika","family":"Ghosh","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8339-9915","authenticated-orcid":false,"given":"Chiao","family":"Hsieh","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sasa","family":"Misailovic","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.546611"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/0471478210"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049808"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/IECON.2016.7793638"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192406"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2016.06.002"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.406967"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1294261.1294281"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462184"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3055004.3055022"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993565"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658604"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2018.2799804"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_22"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/JRA.1987.1087141"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/WF-IoT.2014.6803166"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA40945.2020.9196513"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3231104.3231958"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1201\/b17224"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46024-6"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TVT.2012.2203362"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01379320"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/225058.225162"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISECon.2017.7910242"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24743-2_30"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1773912.1773922"},{"key":"e_1_2_2_33_1","volume-title":"Distributed Algorithms","author":"Lynch Nancy A.","unstructured":"Nancy A. Lynch . 1996. Distributed Algorithms . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA. Nancy A. Lynch. 1996. Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34327-8_36"},{"key":"e_1_2_2_35_1","unstructured":"Aleksandar Milicevic Damien Zuferey and Martin Rinard. 2015. The REACT language for robotics. https:\/\/github.com\/ aleksandarmilicevic\/react-lang  Aleksandar Milicevic Damien Zuferey and Martin Rinard. 2015. The REACT language for robotics. https:\/\/github.com\/ aleksandarmilicevic\/react-lang"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCSE.2014.58"},{"key":"e_1_2_2_37_1","volume-title":"Dhiraj Gandhi, Lerrel Pinto, Saurabh Gupta, and Abhinav Gupta.","author":"Murali Adithyavairavan","year":"2019","unstructured":"Adithyavairavan Murali , Tao Chen , Kalyan Vasudev Alwala , Dhiraj Gandhi, Lerrel Pinto, Saurabh Gupta, and Abhinav Gupta. 2019 . PyRobot: An Open-source Robotics Framework for Research and Benchmarking . ( 2019 ). arXiv:arXiv: 1906.08236 Adithyavairavan Murali, Tao Chen, Kalyan Vasudev Alwala, Dhiraj Gandhi, Lerrel Pinto, Saurabh Gupta, and Abhinav Gupta. 2019. PyRobot: An Open-source Robotics Framework for Research and Benchmarking. ( 2019 ). arXiv:arXiv: 1906.08236"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.84877"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11900-7_17"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2017.7989200"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2016.7759558"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0736-5845(99)00039-3"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_2_2_44_1","volume-title":"Distributed Shared Memory: Concepts and Systems","author":"Protic Jelica","unstructured":"Jelica Protic , Milo Tomasevic , and Veljko Milutinovic . 1997. Distributed Shared Memory: Concepts and Systems . IEEE Computer Society Press . Jelica Protic, Milo Tomasevic, and Veljko Milutinovic. 1997. Distributed Shared Memory: Concepts and Systems. IEEE Computer Society Press."},{"key":"e_1_2_2_45_1","volume-title":"Proc. of the IEEE Intl. Conf. on Robotics and Automation (ICRA) Workshop on Open Source Robotics","author":"Quigley Morgan","unstructured":"Morgan Quigley , Ken Conley , Brian P. Gerkey , Josh Faust , Tully Foote , Jeremy Leibs , Rob Wheeler , and Andrew Y. Ng . 2009. ROS: an open-source Robot Operating System . In Proc. of the IEEE Intl. Conf. on Robotics and Automation (ICRA) Workshop on Open Source Robotics ( Kobe, Japan). IEEE. http:\/\/www.willowgarage.com\/sites\/default\/files\/icraoss09-ROS.pdf Morgan Quigley, Ken Conley, Brian P. Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, and Andrew Y. Ng. 2009. ROS: an open-source Robot Operating System. In Proc. of the IEEE Intl. Conf. on Robotics and Automation (ICRA) Workshop on Open Source Robotics (Kobe, Japan). IEEE. http:\/\/www.willowgarage.com\/sites\/default\/files\/icraoss09-ROS.pdf"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.25165\/j.ijabe.20181104.4278"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.05.002"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1103\/PhysRevE.84.041929"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_10"},{"key":"e_1_2_2_50_1","volume-title":"Guannan Li, Ivan Svogor, and Giovanni Beltrame.","author":"St-Onge David","year":"2017","unstructured":"David St-Onge , Vivek Shankar Varadharajan , Guannan Li, Ivan Svogor, and Giovanni Beltrame. 2017 . ROS and Buzz : consensus-based behaviors for heterogeneous teams. ( 2017 ). arXiv:arXiv:1710.08843 David St-Onge, Vivek Shankar Varadharajan, Guannan Li, Ivan Svogor, and Giovanni Beltrame. 2017. ROS and Buzz: consensus-based behaviors for heterogeneous teams. ( 2017 ). arXiv:arXiv:1710.08843"},{"key":"e_1_2_2_51_1","volume-title":"Robotic Mapping: A Survey","author":"Thrun Sebastian","year":"2003","unstructured":"Sebastian Thrun . 2003 . Robotic Mapping: A Survey . Morgan Kaufmann Publishers Inc ., San Francisco, CA, USA, 1-35. Sebastian Thrun. 2003. Robotic Mapping: A Survey. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1-35."},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805828"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328467"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428300","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428300","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428300","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:02:58Z","timestamp":1750197778000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428300"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":51,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428300"],"URL":"https:\/\/doi.org\/10.1145\/3428300","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}