Solvable Tuple Patterns and Their Applications to Program Verification
Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We introduce solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel formalisms for expressing and inferring invariants between list-like recursive data structures. A distinguishing feature of STPs is that they can be efficiently inferred from only a small number of positive samples; no negative samples are required. After presenting properties and inference algorithms of STPs and CSTPs, we show how to incorporate the CSTP inference into a CHC (Constrained Horn Clauses) solver supporting list-like data structures, which serves as a uniform backend for automated program verification tools. A CHC solver incorporating the (C)STP inference has won the ADT-LIN category of CHC-COMP 2025 by a significant margin.
Thu 18 JunDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:20 | Symbolic Methods for Verification and MatchingPLDI Research Papers at Flatirons 2 Chair(s): Jeffrey S. Foster Tufts University | ||
11:00 20mTalk | Solvable Tuple Patterns and Their Applications to Program Verification PLDI Research Papers Naoki Kobayashi University of Tokyo, Ryosuke Sato Tokyo University of Agriculture and Technology, Ayumi Shinohara Tohoku University, Ryo Yoshinaka Tohoku University DOI | ||
11:20 20mTalk | An Efficient Algorithm for Streaming BPE Tokenization PLDI Research Papers DOI | ||
11:40 20mTalk | Scalable Floating-Point Satisfiability via Staged Optimization PLDI Research Papers Yuanzhuo Zhang Virginia Tech, Zhoulai Fu SUNY Korea; Virginia Tech; Stony Brook University, Binoy Ravindran Virginia Tech DOI | ||
12:00 20mTalk | EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination PLDI Research Papers Ekaterina Zhuchko Tallinn University of Technology, Ian Erik Varatalu Tallinn University of Technology, Margus Veanes Microsoft Research, Nikolaj Bjørner Microsoft Research DOI | ||