SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Sat 18 Oct 2025 15:15 - 15:30 at Orchid Small - Proofs

A microservice-based application is composed of multiple self-contained components called microservices, and controlling inter-service communication is key to enforcing safety properties. Presently, inter-service communication is configured using microservice deployment tools. However, such tools only support a limited class of single-hop policies, which can be overly permissive because they ignore the rich service tree structure of microservice calls. Policies that can express the service tree structure can offer development and security teams more fine-grained control over communication patterns.

To this end, we design an expressive policy language to specify service tree structures, and we develop a visibly pushdown automata-based dynamic enforcement mechanism to enforce service tree policies. Our technique is non-invasive: it does not require any changes to service implementations, and does not require access to microservice code. To realize our method, we build a runtime monitor on top of a service mesh, an emerging network infrastructure layer that can control inter-service communication during deployment. In particular, we employ the programmable network traffic filtering capabilities of Istio, a popular service mesh implementation, to implement an online and distributed monitor. Our experiments show that our monitor can enforce rich safety properties while adding minimal latency overhead on the order of milliseconds.

This program is tentative and subject to change.

Sat 18 Oct

Displayed time zone: Perth change

13:45 - 15:30
13:45
15m
Talk
Adaptive Shielding via Parametric Safety Proofs
OOPSLA
Yao Feng Tsinghua University, Jun Zhu Nankai University, André Platzer Karlsruhe Institute of Technology (KIT), Jonathan Laurent Carnegie Mellon University / Karlsruhe Institute of Technology
14:00
15m
Talk
Certified Decision Procedures for Width-Independent Bitvector Predicates
OOPSLA
Siddharth Bhat University of Cambridge, Leo Stefanesco University of Cambridge, Chris Hughes Independent Researcher, Tobias Grosser University of Cambridge
14:15
15m
Talk
Checking $\delta$-Satisfiability of Reals with Integrals
OOPSLA
Cody Rivera University of Illinois, Urbana-Champaign, Bishnu Bhusal University of Missouri, Rohit Chadha University of Missouri, A. Prasad Sistla University of Illinois at Chicago, Mahesh Viswanathan University of Illinois at Urbana-Champaign
14:30
15m
Talk
Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
OOPSLA
John C. Kolesar Yale University, Shan Ali Yale University, Timos Antonopoulos Yale University, Ruzica Piskac Yale University
14:45
15m
Talk
Incremental Certified Programming
OOPSLA
Tomás Diaz University of Chile, Kenji Maillard Inria – LS2N, Université de Nantes, Nicolas Tabareau Inria, Éric Tanter University of Chile
15:00
15m
Talk
Pathological Cases for a Class of Reachability-Based Garbage Collectors
OOPSLA
Matthew Sotoudeh Stanford University
Link to publication
15:15
15m
Talk
SafeTree: Expressive Tree Policies for Microservices
OOPSLA
Karuna Grewal , Brighten Godfrey UIUC and Broadcom, Justin Hsu Cornell University