Solving String Constraints with Regex-Dependent Functions through Transducers wi
summary
Introduces a new automata model, prioritized streaming string transducers, that encodes JavaScript-style regex features (greedy/lazy star, capturing groups, backreferences) and proves pre-images of regular languages under PSSTs are regular, with an exponential construction. Implements the theory in the solver Ostrich, validates semantics on 1,110 nontrivial regexes, solves over 195,000 real-world constraints, reports up to 18× speedups versus refinement-based baselines, shows general undecidability but completeness for the straight-line fragment.
AI-written summary · about
chapters (17)
- 0:00Intro
- 1:42Background
- 2:47Motivation
- 5:41Nonstandard Semantics
- 6:54Real-world Regular Expression
- 9:41Construction of PSST
- 10:41Validation
- 11:32Table of Content
- 11:43Our String Logic
- 12:56Decidability
- 13:32Sequent Calculus for STR
- 15:09Regularity-Preserving Property
- 16:51Straight-line Fragment
- 17:43Decision Procedure for STREL
- 19:26Our String Solver
- 20:02Evaluation
- 20:57Takeaway
related talks
23mLinear Matching of JavaScript Regular Expressions
25mFormal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics(…)
01h 13m/ Reg (exp) {2} lained / Demystifying Regular Expressions
22mStatic Analysis for Checking the Disambiguation Robustness of Regular Expressions
22mTwo Problems: Regular Expressions for Revolutionaries
17mWhen Chomsky Met JavaScript: Exploring the Linguistics(...)
01h 06mEverybody stands back! I know regular expressions
37mAll About Regular Expressions