Z3str2: an efficient solver for strings, regular expressions, and length constraints
From MaRDI portal
Publication:526767
DOI10.1007/S10703-016-0263-6zbMATH Open1360.68773OpenAlexW2565985959MaRDI QIDQ526767FDOQ526767
Authors: Yunhui Zheng, Vijay Ganesh, S. Subramanian, Omer Tripp, Murphy Berzish, Julian Dolby, Xiangyu Zhang 
Publication date: 15 May 2017
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-016-0263-6
Recommendations
- Towards more efficient methods for solving regular-expression heavy string constraints
- An SMT solver for regular expressions and linear arithmetic over string length
- An efficient SMT solver for string constraints
- Even Faster Conflicts and Lazier Reductions for String Solvers
- Scaling up DPLL(T) string solvers using context-dependent simplification
Cites Work
- A Decision Procedure for Bit-Vectors and Arrays
- An efficient algorithm for solving word equations
- Satisfiability of word equations with constants is in PSPACE
- Title not available (Why is that?)
- THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
- Makanin's algorithm for word equations-two improvements and a generalization
- Symbolic String Verification: Combining String Analysis and Size Analysis
- Path Feasibility Analysis for String-Manipulating Programs
- Title not available (Why is that?)
- The expressibility of languages and relations by word equations
- Recompression: word equations and beyond
Cited In (16)
- Symbolic String Verification: Combining String Analysis and Size Analysis
- A decision procedure for regular membership and length constraints over unbounded strings
- Path Feasibility Analysis for String-Manipulating Programs
- A solver for arrays with concatenation
- Progressive reasoning over recursively-defined strings
- String theories involving regular membership predicates: from practice to theory and back
- A symbolic algorithm for the case-split rule in string constraint solving
- Towards more efficient methods for solving regular-expression heavy string constraints
- Z3str2
- Even Faster Conflicts and Lazier Reductions for String Solvers
- Constraint solving on bounded string variables
- Variants and satisfiability in the infinitary unification wonderland
- Solving string constraints using SAT
- Dashed strings for string constraint solving
- An efficient SMT solver for string constraints
- Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)
Uses Software
This page was built for publication: Z3str2: an efficient solver for strings, regular expressions, and length constraints
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q526767)
