SPLASH 2026
Sun 4 - Fri 9 October 2026 Oakland, California, United States
co-located with SPLASH/ISSTA 2026

This program is tentative and subject to change.

Mon 5 Oct 2026 10:48 - 11:06 at Junior Ballroom 1&2 - Synthesis and Specification Chair(s): Jocelyn Qiaochu Chen

Control problems for embedded systems like cars and trains can be modeled by two-player hybrid games. Control envelopes, which are families of safe control solutions, correspond to nondeterministic policies that ensure a player following them will not lose. Each deterministic, finite specialization of the nondeterministic policy is a control solution. This paper synthesizes control envelopes for hybrid games that are as permissive as possible. It introduces subvalue maps, a compositional representation of such policies that enables verification and synthesis along the structure of the game. An inductive logical characterization in differential game logic (dGL) checks whether a subvalue map induces a sound control envelope which ensures that the player never loses, no matter what actions the opponent plays. The maximal subvalue map, which allows the most action options while still winning, is shown to exist and satisfy a logical characterization. An inductive subvalue map synthesis framework is obtained from the soundness characterization. An evaluation of the framework uses the significant expressivity of dGL to model and solve a broad range of control challenges.

This program is tentative and subject to change.

Mon 5 Oct

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

10:30 - 12:00
Synthesis and SpecificationOOPSLA at Junior Ballroom 1&2
Chair(s): Jocelyn Qiaochu Chen University of Alberta
10:30
18m
Talk
Grammar Repair with Examples and Tree Automata
OOPSLA
Yunjeong Lee National University of Singapore, Gokul Rajiv National University of Singapore, Ilya Sergey National University of Singapore
DOI
10:48
18m
Talk
Hybrid Game Control Envelope Synthesis
OOPSLA
Aditi Kabra Carnegie Mellon University, Jonathan Laurent KIT, Stefan Mitsch DePaul University, André Platzer KIT
DOI
11:06
18m
Talk
P4-SpecTec: Integrating a Language Mechanization Framework into the Real-World P4 Specification
OOPSLA
DOI
11:24
18m
Talk
Commit-Window Observation Contracts for Reactive Entity-Component Systems
OOPSLA
Tomoyuki Aotani Shibaura Institute of Technology, Tetsuo Kamina Oita University
DOI
11:42
18m
Talk
Incremental Program Synthesis from Event Logs
OOPSLA
Jinwoo Kim University of California at San Diego, Victor Nicolet Amazon, Joey Dodds Amazon, Loris D'Antoni University of California at San Diego
DOI
Hide past events