Parikh's Theorem Made Symbolic - POPL'24

Explore a conference talk that delves into an innovative approach to Parikh's Theorem for symbolic automata and grammars. Learn how this fundamental result in automata theory is adapted to handle large finite or infinite alphabets, a crucial advancement for real-world applications in software verification, cryptographic protocol verification, and database querying. Discover a new construction that avoids exponential blowup in formula size, allowing for polynomial-time computation of existential formulas over Presburger and base theories. Gain insights into the extension of this algorithm to parametric symbolic grammars, one of the most expressive models for languages over infinite alphabets. Understand the practical implications of this research through an implementation that demonstrates its effectiveness in solving complex string constraints.