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

This program is tentative and subject to change.

Thu 16 Oct 2025 11:00 - 11:15 at Orchid West - Theory

We propose a compositional approach to combine and scale automated reasoning in the static analysis of decentralized system security, such as blockchains. Our focus lies in the game-theoretic security analysis of such systems, allowing us to examine economic incentives behind user actions. In this context, it is particularly important to certify that deviating from the intended, honest behavior of the decentralized protocol is not beneficial: as long as users follow the protocol, they cannot be financially harmed, regardless of how others behave. Such an economic analysis of blockchain protocols can be encoded as an automated reasoning problem in the first-order theory of real arithmetic, reducing game-theoretic reasoning to satisfiability modulo theories (SMT). However, analyzing an entire game-theoretic model (called a game) as a single SMT instance does not scale to protocols with millions of interactions. We address this challenge and propose a divide-and-conquer security analysis based on compositional reasoning over games. Our compositional analysis is incremental: we divide games into subgames such that changes to one subgame do not necessitate re-analyzing the entire game, but only the ancestor nodes. Our approach is sound, complete and effective: combining the security properties of subgames yields security of the entire game. Experimental results show that compositional reasoning discovers intra-game properties and errors while scaling to games with millions of nodes, enabling security analysis of large protocols.

This program is tentative and subject to change.

Thu 16 Oct

Displayed time zone: Perth change

10:30 - 12:15
10:30
15m
Talk
Automated Discovery of Tactic Libraries for Interactive Theorem Proving
OOPSLA
Yutong Xin The University of Texas at Austin, Jimmy Xin The University of Texas at Austin, Gabriel Poesia Stanford University, Noah D. Goodman Stanford University, Jocelyn Qiaochu Chen New York University, University of Alberta, Işıl Dillig University of Texas at Austin
10:45
15m
Talk
Choreographic Quick Changes: First-Class Location (Set) Polymorphism
OOPSLA
Ashley Samuelson University of Wisconsin-Madison, Andrew K. Hirsch University at Buffalo, SUNY, Ethan Cecchetti University of Wisconsin-Madison
11:00
15m
Talk
Divide and Conquer: A Compositional Approach to Game-Theoretic Security
OOPSLA
Ivana Bocevska TU Wien, Anja Petković Komel TU Wien, Vienna, Austria, Laura Kovács TU Wien, Sophie Rain Argot Collective, Michael Rawson University of Southampton
11:15
15m
Talk
Efficient Decrease-And-Conquer Linearizability Monitoring
OOPSLA
Zheng Han Lee National University of Singapore, Singapore, Umang Mathur National University of Singapore
Pre-print
11:30
15m
Talk
Liberating Merges via Apartness and Guarded Subtyping
OOPSLA
Han Xu Princeton University, Xuejing Huang IRIF, Bruno C. d. S. Oliveira University of Hong Kong
11:45
15m
Talk
The Simple Essence of Monomorphization
OOPSLA
Matthew Lutze Aarhus University, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen
12:00
15m
Talk
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
OOPSLA
Yichen Xu EPFL, Oliver Bračevac EPFL, LAMP, Nguyen Pham EPFL, LAMP, Martin Odersky EPFL
Pre-print