Parikh's Theorem Made Symbolic
summary
Construction converts symbolic automata and parametric symbolic grammars into compact numeric abstractions: an algorithm computes polynomial-time existential Presburger formulas (over quantifier-free Presburger plus the base theory) that count how often user-given predicates hold, avoiding the exponential blowup of naive encodings. Implementation solves hard SMT string benchmarks by discharging many constraints via integers; unsatisfiable results remain sound while satisfiable outcomes can be spurious, and effectiveness depends on chosen predicate partitions for large or infinite alphabets and on integration with existing SMT-backed string solving.
AI-written summary · about
chapters (13)
- 0:00Parikh’s Theorem and symbolic automata
- 1:03Parikh images for string verification
- 3:07Undecidability in string analysis
- 4:11Parikh images via integer vectors
- 5:55Symbolic encoding with Parikh images
- 7:59Alphabet size in Parikh encoding
- 8:41Parametric automata
- 9:45Parametric grammars and pushdown systems
- 11:16Generalizing Parikh images
- 12:38Efficient SMT encoding
- 13:22Experimental evaluation
- 14:26Future work
- 15:12Q&A
related talks
41mOptimizing Relational Programs I
15mSpeeding up Symbolic Reasoning for Relational Queries
01h 06mSemiring Semantics
01h 08mAlgebraic Structures in Logic and Query Evaluation 4
45mProblem Solved! Using Logic Programming to Find Answers
20mPolygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
01h 05mAlgebraic Structures in Logic and Query Evaluation 2
01h 24mIntroduction to Constraint Logic Programming