SPLASH 2026
Sun 4 - Fri 9 October 2026 Oakland, California, United States
co-located with SPLASH/ISSTA 2026
Tue 6 Oct 2026 14:24 - 14:42 at Junior Ballroom 3&4 - Verifying Real Systems Chair(s): Bor-Yuh Evan Chang

Proving properties of programs that manipulate compound data structures requires both disjunctive reasoning (e.g., a pointer may target different arrays) and relational reasoning. Existing abstract interpreters struggle to combine both: non-relational designs support modular composition of abstract domains but lose relations, while assignment-based relational designs capture relations but hinder modularity and reuse. We introduce open lattices and abstract abstract datatypes (AADT), a new foundation for building precise and reusable abstract domains for structured values. Open lattices generalize classical lattices by introducing shared symbolic values constrained by an abstract valuation domain, enabling relational reasoning across independently defined abstractions. AADTs are compositional transformers over open lattices that mirror the structure of concrete data types: addresses, records, unions, variants, arrays, and their arbitrary nesting. Because each AADT closely follows the concrete datatype definition, abstract domain operations are modular and easy to reuse or extend. Most AADT transformers that we provide are exact: when the abstract valuation domain is exact, the resulting abstraction is a precise translation of the concrete semantics. This enables applications beyond static analysis, such as counter-example generation. We formalize open lattices and AADTs, present key instances, and implement them in a framework for the analysis of C and binary programs. Our experiments show precision gains over state-of-the-art abstract interpreters, while maintaining comparable analysis times.

Tue 6 Oct

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

13:30 - 15:00
Verifying Real SystemsOOPSLA at Junior Ballroom 3&4
Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder; Amazon
13:30
18m
Talk
Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications
OOPSLA
Shenghao Yuan Zhejiang University, Yazhou Tang Zhejiang University, Tianci Cao Zhejiang University, Frédéric Besson Inria Rennes, Jean-Pierre Talpin Inria, Mingshuai Chen Zhejiang University
DOI File Attached
13:48
18m
Talk
ZSafe: Proving the Safety of Proprietary Hardware Designs in Zero Knowledge
OOPSLA
Zhaoxiang Liu Kansas State University, James Parker Ossa Network, Ning Luo University of Illinois at Urbana-Champaign
DOI
14:06
18m
Talk
Equivalence Checking of ML GPU Kernels
OOPSLA
Benjamin Driscoll Stanford University, Kshitij Dubey Microsoft Research, Anjiang Wei Stanford University, Neeraj Kayal Microsoft Research, Rahul Sharma Google DeepMind, Alex Aiken Stanford University
DOI
14:24
18m
Talk
AADT: Abstract Abstract Data Types
OOPSLA
Julien Simonnet Université Paris-Saclay - CEA LIST, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Mihaela Sighireanu Université Paris-Saclay - ENS Paris-Saclay - CNRS - LMF
DOI
14:42
18m
Talk
RAT-CAT-SAT: Model Checking Memory Consistency Models
OOPSLA
Jan Grünke TU Braunschweig, Thomas Haas TU Braunschweig, Roland Meyer TU Braunschweig
DOI