SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 14:20 - 14:35 at Zurich G - OOPSLA and Onward! 2020 Papers 2 Chair(s): Michael Coblenz

A robot’s code needs to sense the environment, control the hardware, and communicate with other robots. Cur- rent programming languages do not provide the necessary hardware platform-independent abstractions, and therefore, developing robot applications require detailed knowledge of signal processing, control, path plan- ning, network protocols, and various platform-specific details. Further, porting applications across hardware platforms becomes tedious. We present Koord—a domain specific language for distributed robotics—which abstracts platform-specific functions for sensing, communication, and low-level control. Koord makes the platform-independent control and coordination code portable and modularly verifiable. It 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 formation flight and distributed delivery 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.

Wed 20 Oct

Displayed time zone: Central Time (US & Canada) change

13:50 - 15:10
OOPSLA and Onward! 2020 Papers 2SIGPLAN Papers at Zurich G
Chair(s): Michael Coblenz University of Maryland at College Park
13:50
15m
Talk
Programming and Reasoning with Partial Observability
SIGPLAN Papers
Eric Atkinson Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology
14:05
15m
Talk
Pomsets with Preconditions: A Simple Model of Relaxed Memory
SIGPLAN Papers
Radha Jagadeesan DePaul University, Alan Jeffrey Roblox, James Riely DePaul University
14:20
15m
Talk
Koord: a language for programming and verifying distributed robotics applications
SIGPLAN Papers
Ritwika Ghosh University of Illinois at Urbana-Champaign, Chiao Hsieh University of Illinois at Urbana-Champaign, Sasa Misailovic University of Illinois at Urbana-Champaign, Sayan Mitra University of Illinois at Urbana-Champaign
14:35
15m
Paper
Demystifying Dependence
SIGPLAN Papers
James Koppel Massachusetts Institute of Technology, USA, Daniel Jackson MIT
Link to publication Pre-print
14:50
20m
Live Q&A
Discussion, Questions and Answers
SIGPLAN Papers