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 OctDisplayed 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 18mTalk | 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 18mTalk | 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 18mTalk | 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 18mTalk | 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 18mTalk | RAT-CAT-SAT: Model Checking Memory Consistency Models OOPSLA DOI | ||