SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 11:00 - 11:20 at OOPSLA/ECOOP - T-3
Tue 17 Nov 2020 23:00 - 23:20 at OOPSLA/ECOOP - T-3

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.

Tue 17 Nov
Times are displayed in time zone: Central Time (US & Canada) change

11:00 - 12:20: T-3OOPSLA at OOPSLA/ECOOP +12h
11:00 - 11:20
Talk
OOPSLA
Ritwika GhoshUIUC, Chiao HsiehUniversity of Illinois at Urbana-Champaign, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, sayan mitraUniversity of Illinois at Urbana-Champaign
Pre-print
11:20 - 11:40
Talk
OOPSLA
Suvam MukherjeeMicrosoft Research India, Pantazis DeligiannisMicrosoft Research, Arpita BiswasIndian Institute of Science, Akash LalMicrosoft Research India
11:40 - 12:00
Talk
OOPSLA
Umar FarooqUniversity of California Riverside, Zhijia ZhaoUC Riverside, Manu SridharanUniversity of California Riverside, Iulian NeamtiuNew Jersey Institute of Technology
Pre-print
12:00 - 12:20
Talk
OOPSLA
Aayan KumarMicrosoft Research India, Vivek SeshadriMicrosoft Research, India, Rahul SharmaMicrosoft Research
23:00 - 00:20: T-3OOPSLA at OOPSLA/ECOOP
23:00 - 23:20
Talk
OOPSLA
Ritwika GhoshUIUC, Chiao HsiehUniversity of Illinois at Urbana-Champaign, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, sayan mitraUniversity of Illinois at Urbana-Champaign
Pre-print
23:20 - 23:40
Talk
OOPSLA
Suvam MukherjeeMicrosoft Research India, Pantazis DeligiannisMicrosoft Research, Arpita BiswasIndian Institute of Science, Akash LalMicrosoft Research India
23:40 - 00:00
Talk
OOPSLA
Umar FarooqUniversity of California Riverside, Zhijia ZhaoUC Riverside, Manu SridharanUniversity of California Riverside, Iulian NeamtiuNew Jersey Institute of Technology
Pre-print
00:00 - 00:20
Talk
OOPSLA
Aayan KumarMicrosoft Research India, Vivek SeshadriMicrosoft Research, India, Rahul SharmaMicrosoft Research