Solvable Tuple Patterns and Their Applications to Program Verification
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Thu 18 JunDisplayed time zone: Mountain Time (US & Canada) change
10:30 - 12:10 | |||
10:30 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 | ||
10:50 20mTalk | Towards Efficient Matching of Regexes with Backreferences using Register Set Automata PLDI Research Papers Vojtěch Havlena Brno University of Technology, Lukáš Holík Brno University of Technology; Aalborg University, Ondřej Lengál Brno University of Technology, Jan Vašák Brno University of Technology, Sabína Gulčíková Brno University of Technology DOI | ||
11:10 20mTalk | An Efficient Algorithm for Streaming BPE Tokenization PLDI Research Papers DOI | ||
11:30 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 | ||
11:50 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 | ||