Solvable Tuple Patterns and Their Applications to Program Verification
summary
Introduces solvable tuple patterns (STPs) and conjunctive STPs as a representation for relations among sequences that are learnable from only positive samples and have a simple inference algorithm that runs linear in the input sample size; shows a sound-and-complete characterization (solvability) and existence of small characteristic examples that uniquely identify patterns; reduces verification to CHC solving over words using STP/CSTP inference, leverages pure word-equation reasoning with PSPACE decidability for satisfiability, and ships a CHC solver Shuko that won the ADT-LIN category of CHC‑COMP 2025 by a significant margin.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:34List manipulation example
- 3:20Solvable tuple patterns
- 6:33Learnability of patterns
- 10:33Algorithmic properties
- 10:56Application to automated verification
- 13:30Verification with STP
- 14:35STP with arithmetic
- 16:02Experimental results
- 16:24Related work
- 17:25Conclusion
- 17:52Q&A
related talks
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
28mFormalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
15mClosing Remarks
13mConsistency-Preserving Propagation for SMT Solving of Concurrent Program Verification
58mA New Perspective on Commutativity in Verification
18mAutomated Catamorphism Synthesis for Solving Constrained Horn Clauses over Algebraic(…)
35mThe Mastermind behind Refinement Types