Z3str2: an efficient solver for strings, regular expressions, and length constraints

DOI10.1007/s10703-016-0263-6zbMath1360.68773OpenAlexW2565985959MaRDI QIDQ526767

Omer Tripp, Murphy Berzish, Yunhui Zheng, Julian Dolby, Sanu Subramanian, Vijay Ganesh, 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

zbMATH Keywords

string analysisSMT solverstring constraint solver

Mathematics Subject Classification ID

Algorithms on strings (68W32)

Related Items

String theories involving regular membership predicates: from practice to theory and back ⋮ Variants and satisfiability in the infinitary unification wonderland ⋮ A solver for arrays with concatenation ⋮ Z3str2 ⋮ Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

Uses Software

• SMT-LIB
• z3
• KLEE
• Stranger
• HAMPI
• Z3-str
• JST
• S3
• PASS
• GitHub
• SymJS

Cites Work

• Unnamed Item
• Unnamed Item
• An efficient algorithm for solving word equations
• Satisfiability of word equations with constants is in PSPACE
• Path Feasibility Analysis for String-Manipulating Programs
• Symbolic String Verification: Combining String Analysis and Size Analysis
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• The expressibility of languages and relations by word equations
• Recompression: Word Equations and Beyond
• A Decision Procedure for Bit-Vectors and Arrays
• Makanin's algorithm for word equations-two improvements and a generalization