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

This program is tentative and subject to change.

Fri 17 Oct 2025 16:15 - 16:30 at Orchid East - Verification 1

Data replication is crucial for enabling fault tolerance and uniform low latency in modern decentralized applications. Replicated Data Types (RDTs) have emerged as a principled approach for developing replicated implementations of basic data structures such as counter, flag, set, map, etc. While correctness of RDTs is generally specified using the notion of strong eventual consistency–which guarantees that replicas which have received the same set of updates would converge to the same state–a more expressive specification which relates the converged state to updates received at a replica would be more beneficial to RDT users. Replication-aware linearizability is one such specification, which requires all replicas to always be in a state which can be obtained by linearizing the updates received at the replica. In this work, we develop a novel fully automated technique for verifying replication-aware linearizability for Mergeable Replicated Data Types (MRDTs). We identify novel algebraic properties for MRDT operations and the merge function which are sufficient for proving an implementation to be linearizable and which go beyond the standard notions of commutativity, associativity and idempotence. We also develop a novel inductive technique called bottom-up linearization to automatically verify the required algebraic properties. Our technique can be used to verify both MRDTs and state-based CRDTs. We have successfully applied our approach on a number of complex MRDT and CRDT implementations including a novel JSON MRDT.

This program is tentative and subject to change.

Fri 17 Oct

Displayed time zone: Perth change

16:00 - 17:30
Verification 1OOPSLA at Orchid East
16:00
15m
Talk
A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
OOPSLA
Ameer Hamza Florida State University, Lucas Zavalia Florida State University Tallahassee, Arie Gurfinkel University of Waterloo, Jorge A. Navas Certora, Grigory Fedyukovich Florida State University
16:15
15m
Talk
Automatically Verifying Replication-aware Linearizability
OOPSLA
Vimala Soundarapandian IIT Madras, Kartik Nagar IIT Madras, Aseem Rastogi Microsoft Research, KC Sivaramakrishnan IIT Madras and Tarides
16:30
15m
Talk
On the Impact of Formal Verification on Software Development
OOPSLA
Eric Mugnier University of California San Diego, Zhou Yuanyuan UCSD, Ranjit Jhala University of California at San Diego, Michael Coblenz University of California, San Diego
16:45
15m
Talk
Towards Verifying Crash Consistency
OOPSLA
Keonho Lee University of California, Irvine, Conan Truong University of California, Irvine, Brian Demsky University of California at Irvine
17:00
15m
Talk
TraceLinking Implementations with their Verified Designs
OOPSLA
Finn Hackett University of British Columbia, Ivan Beschastnikh The University of British Columbia
Pre-print
17:15
15m
Talk
Pyrosome: Verified Compilation for Modular Metatheory
OOPSLA
Dustin Jamner MIT CSAIL, Gabriel Kammer MIT, Ritam Nag MIT, Adam Chlipala MIT CSAIL