Towards more efficient methods for solving regular-expression heavy string constraints

DOI10.1016/J.TCS.2022.12.009MaRDI QIDQ2680985zbMATH OpenOpenAlexFDO

Authors Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, Dirk Nowotka

Publication date 5 January 2023

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.tcs.2022.12.009

zbMATH Keywords

heuristicslinear length constraintsregular expressionsSMT solvingstring constraintsstring solving

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• An SMT solver for regular expressions and linear arithmetic over string length
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Solving String Theories Involving Regular Membership Predicates Using SAT
• Even Faster Conflicts and Lazier Reductions for String Solvers
• An efficient SMT solver for string constraints

Cites work

• A decision procedure for regular membership and length constraints over unbounded strings
• A Survey on Fooling Sets as Effective Tools for Lower Bounds on Nondeterministic Complexity
• An SMT solver for regular expressions and linear arithmetic over string length
• Automata-based model counting for string constraints
• Chrobak normal form revisited, with applications
• Finite automata and unary languages
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1979550 (Why is no real title available?)
• scientific article; zbMATH DE number 1737190 (Why is no real title available?)
• Path Feasibility Analysis for String-Manipulating Programs
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• String theories involving regular membership predicates: from practice to theory and back
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• The satisfiability of word equations: decidable and undecidable theories
• Word equations in nondeterministic linear space

Cited in

(13)

• Symbolic automata constraint solving
• Z3str2: an efficient solver for strings, regular expressions, and length constraints
• Unbounded model-checking with interpolation for regular language constraints
• Even Faster Conflicts and Lazier Reductions for String Solvers
• Solving string constraints using SAT
• Algorithms for checking intersection non-emptiness of regular expressions
• Formal languages and arithmetic theories: recent results and open problems
• On the decidability and expressive power of several theories based on string constraints
• Semënov arithmetic, affine \{VASS\}, and string constraints
• Satisfiability of context-free string constraints with subword-ordering and transducers
• Incremental algorithms for solving regular expression intersection non-emptiness
• Title not available (Why is no real title available?)
• An SMT solver for regular expressions and linear arithmetic over string length

Describes a project that uses

Uses Software

• StringFuzz
• ZaligVinder
• z3
• JavaScript
• Stranger
• CVC4
• HAMPI
• S3
• Norn
• Z3str3
• Z3str2
• Saner

This page was built for publication: Towards more efficient methods for solving regular-expression heavy string constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2680985)