SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Sat 18 Oct 2025 16:00 - 16:15 at Orchid West - Verification 4 Chair(s): Jieung Kim

We study the problem of automated hypersafety verification of infinite-state recursive programs. We propose an infinite class of product programs, specifically designed with recursion in mind, that reduce the hypersafety verification of a recursive program to standard safety verification. For this, we combine insights from language theory and concurrency theory to propose an algorithmic solution for constructing an infinite class of recursive product programs. One key insight is that, using the simple theory of visibly pushdown languages, one can maintain the recursive structure of syntactic program alignments which is vital to constructing a new product program that can be viewed as a classic recursive program — that is, one that can be executed on a single stack. Another key insight is that techniques from concurrency theory can be generalized to help define product programs based on the view that the parallel composition of individual recursive programs includes all possible alignments from which a sound set of alignments that faithfully preserve the satisfaction of the hypersafety property can be selected. On the practical side, we formulate a family of parametric canonical product constructions that are intuitive to programmers and can be used as building blocks to specify recursive product programs for the purpose of relational and hypersafety verification, with the idea that the right product program can be verified automatically using existing techniques. We demonstrate the effectiveness of these techniques through an implementation and highly promising experimental results.

Sat 18 Oct

Displayed time zone: Perth change

16:00 - 17:30
Verification 4OOPSLA at Orchid West
Chair(s): Jieung Kim Yonsei University
16:00
15m
Talk
Products of Recursive Programs for Hypersafety Verification
OOPSLA
Ruotong Cheng University of Toronto, Azadeh Farzan University of Toronto
16:15
15m
Talk
Embedding Quantum Program Verification into Dafny
OOPSLA
Feifei Cheng Iowa State University, Sushen Vangeepuram Iowa State University, Henry Allard Iowa State University, Seyed Mohammad Reza Jafari Iowa State University, Alex Potanin Australian National University, Liyi Li Iowa State University
16:30
15m
Talk
Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
OOPSLA
Kevin Guan Cornell University, Marcelo d'Amorim North Carolina State University, Owolabi Legunsen Cornell University
16:45
15m
Talk
Interactive Bit Vector Reasoning using Verified Bitblasting
OOPSLA
Henrik Böving Lean FRO, Siddharth Bhat University of Cambridge, Alex Keizer University of Cambridge, Luisa Cicolini University of Cambridge, Leon Frenot ENS Lyon, Abdalrhman Mohamed Stanford University, Leo Stefanesco University of Cambridge, Harun Khan Stanford University, Josh Clune Carnegie Mellon University, Clark Barrett Stanford University, Tobias Grosser University of Cambridge