SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Tue 17 Nov 2020 11:00 - 11:20 at SPLASH-I - T-3 Chair(s): Olivier Tardieu, Burcu Kulahcioglu Ozkan
Tue 17 Nov 2020 23:00 - 23:20 at SPLASH-I - T-3 Chair(s): Chengyu Zhang, Ting Cao

A robot’s 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—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. 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.

Tue 17 Nov

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

11:00 - 12:20
T-3OOPSLA at SPLASH-I +12h
Chair(s): Olivier Tardieu IBM Research, Burcu Kulahcioglu Ozkan MPI-SWS
11:00
20m
Talk
Koord: A Language for Programming and Verifying Distributed Robotics Application
OOPSLA
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
Link to publication DOI Pre-print Media Attached
11:20
20m
Talk
Learning-Based Controlled Concurrency Testing
OOPSLA
Suvam Mukherjee Microsoft Research, Pantazis Deligiannis Microsoft Research, Arpita Biswas IISc Bangalore, Akash Lal Microsoft Research
Link to publication DOI Pre-print Media Attached
11:40
20m
Talk
LiveDroid: Identifying and Preserving Mobile App State in Volatile Runtime Environments
OOPSLA
Umar Farooq University of California at Riverside, Zhijia Zhao University of California at Riverside, Manu Sridharan University of California at Riverside, Iulian Neamtiu New Jersey Institute of Technology
Link to publication DOI Pre-print Media Attached
12:00
20m
Talk
Shiftry: RNN Inference in 2KB of RAM
OOPSLA
Aayan Kumar Microsoft Research, Vivek Seshadri Microsoft Research, Rahul Sharma Microsoft Research
Link to publication DOI Media Attached
23:00 - 00:20
T-3OOPSLA at SPLASH-I
Chair(s): Chengyu Zhang East China Normal University, Ting Cao Microsoft Research
23:00
20m
Talk
Koord: A Language for Programming and Verifying Distributed Robotics Application
OOPSLA
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
Link to publication DOI Pre-print Media Attached
23:20
20m
Talk
Learning-Based Controlled Concurrency Testing
OOPSLA
Suvam Mukherjee Microsoft Research, Pantazis Deligiannis Microsoft Research, Arpita Biswas IISc Bangalore, Akash Lal Microsoft Research
Link to publication DOI Pre-print Media Attached
23:40
20m
Talk
LiveDroid: Identifying and Preserving Mobile App State in Volatile Runtime Environments
OOPSLA
Umar Farooq University of California at Riverside, Zhijia Zhao University of California at Riverside, Manu Sridharan University of California at Riverside, Iulian Neamtiu New Jersey Institute of Technology
Link to publication DOI Pre-print Media Attached
00:00
20m
Talk
Shiftry: RNN Inference in 2KB of RAM
OOPSLA
Aayan Kumar Microsoft Research, Vivek Seshadri Microsoft Research, Rahul Sharma Microsoft Research
Link to publication DOI Media Attached