Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Watch this 15-minute conference presentation from OOPSLA 2025 that introduces an innovative approach to automated hypersafety verification of infinite-state recursive programs. Learn how researchers Ruotong Cheng and Azadeh Farzan from the University of Toronto propose an infinite class of product programs specifically designed to handle recursion, reducing hypersafety verification to standard safety verification. Discover how the presentation combines insights from language theory and concurrency theory to construct recursive product programs that maintain syntactic program alignments using visibly pushdown languages theory. Explore how techniques from concurrency theory are generalized to define product programs based on parallel composition of individual recursive programs, enabling selection of sound alignments that preserve hypersafety properties. Understand the practical applications through a family of parametric canonical product constructions that serve as intuitive building blocks for programmers to specify recursive product programs for relational and hypersafety verification. See experimental results demonstrating the effectiveness of these techniques through implementation and promising performance outcomes, with accompanying artifacts that have been evaluated as reusable and results reproduced.
