SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Sat 18 Oct 2025 11:15 - 11:30 at Orchid Plenary Ballroom - Synthesis 1 Chair(s): Yingfei Xiong

Augmented reality (AR) seamlessly overlays virtual objects onto the real world, enabling an exciting new range of applications. Multiple users view and interact with virtual objects, which are replicated and shown on each user’s display. A key requirement of AR is that the replicas should be quickly updated and converge to the same state; otherwise, users may have laggy or inconsistent views of the virtual object, which negatively affects their experience. A second key requirement is that the movements of virtual objects in space should preserve certain integrity properties either due to physical boundaries in the real world, or privacy and safety preferences of the user. For example, a virtual cup should not sink into a table, or a private virtual whiteboard should stay within an office. The challenge tackled in this paper is the coordination of virtual objects with low latency, spatial integrity properties and convergence. We introduce ``well-organized'' replicated data types that guarantee these two properties. Importantly, they capture a local notion of conflict that supports more concurrency and lower latency. To implement well-organized virtual objects, we introduce a credit scheme and replication protocol that further facilitate local execution, and prove the protocol’s correctness. Given an AR environment, we automatically derive conflicting actions through constraint solving, and statically instantiate the protocol to synthesize custom coordination. We evaluate our implementation, Bazi, on off-the-shelf Android AR devices and show a latency reduction of 30.5-88.4% and a location staleness reduction of 35.6-75.6%, compared to three baselines, for varying numbers of devices, AR environments, request loads, and network conditions.

Sat 18 Oct

Displayed time zone: Perth change

10:30 - 12:15
Synthesis 1OOPSLA at Orchid Plenary Ballroom
Chair(s): Yingfei Xiong Peking University
10:30
15m
Talk
Abstraction Refinement-guided Program Synthesis for Robot Learning from Demonstrations
OOPSLA
Guofeng Cui Rutgers University, Yuning Wang Rutgers University, Wensen Mao Rutgers University, Yuanlin Duan Rutgers University, He Zhu Rutgers University, USA
10:45
15m
Talk
API-guided Dataset Synthesis to Finetune Large Code Models
OOPSLA
Li Zongjie Hong Kong University of Science and Technology, Daoyuan Wu Lingnan University, Shuai Wang Hong Kong University of Science and Technology, Zhendong Su ETH Zurich
11:00
15m
Talk
Fast Constraint Synthesis for C++ Function Templates
OOPSLA
Shuo Ding Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology
11:15
15m
Talk
Hambazi: Spatial Coordination Synthesis for Augmented Reality
OOPSLA
Yi-Zhen Tsai University of California, Riverside, Jiasi Chen University of Michigan, Mohsen Lesani University of California at Santa Cruz
11:30
15m
Talk
Inductive Synthesis of Inductive Heap Predicates
OOPSLA
Ziyi Yang National University of Singapore, Ilya Sergey National University of Singapore
11:45
15m
Talk
LOUD: Synthesizing Strongest and Weakest Specifications
OOPSLA
Kanghee Park University of Wisconsin-Madison, Xuanyu Peng University of California, San Diego, Loris D'Antoni University of California at San Diego
12:00
15m
Talk
Metamorph: Synthesizing Large Objects from Dafny Specifications
OOPSLA
Aleksandr Fedchin Tufts University, Alexander Bai New York University, Jeffrey S. Foster Tufts University