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

DOI10.1007/S10703-016-0263-6MaRDI QIDQ526767zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

string analysisSMT solverstring constraint solver

Mathematics Subject Classification ID

Algorithms on strings (68W32)

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

• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 2090837 (Why is no real title available?)
• A Decision Procedure for Bit-Vectors and Arrays
• An efficient algorithm for solving word equations
• Makanin's algorithm for word equations-two improvements and a generalization
• Path Feasibility Analysis for String-Manipulating Programs
• Recompression: word equations and beyond
• Satisfiability of word equations with constants is in PSPACE
• 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

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
• Z3str2
• Towards more efficient methods for solving regular-expression heavy string constraints
• Even Faster Conflicts and Lazier Reductions for String Solvers
• Constraint solving on bounded string variables
• Variants and satisfiability in the infinitary unification wonderland
• Dashed strings for string constraint solving
• Solving string constraints using SAT
• An efficient SMT solver for string constraints
• Equational unification and matching, and symbolic reachability analysis in Maude 3.2 (system description)

Describes a project that uses

Uses Software

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

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)