An SMT solver for regular expressions and linear arithmetic over string length
From MaRDI portal
(Redirected from Publication:832270)
Abstract: We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insight that underpins our algorithm is that real-world instances contain a wealth of information about upper and lower bounds on lengths of strings under constraints, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present a number of novel general heuristics, such as the prefix/suffix method, that can be used in conjunction with a variety of regex solving algorithms, making them more efficient. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this benchmark, in particular achieving a 2.4x speedup over CVC4, 4.4x speedup over Z3seq, 6.4x speedup over Z3-Trau, 9.1x speedup over Z3str3, and 13x speedup over OSTRICH.
Recommendations
- An efficient SMT solver for string constraints
- A decision procedure for string logic with quadratic equations, regular expressions and length constraints
- Symbolic solving of extended regular expression inequalities
- Extended regular expressions: succinctness and decidability
- Extended Regular Expressions: Succinctness and Decidability
- A Compact Proof of Decidability for Regular Expression Equivalence
- Towards more efficient methods for solving regular-expression heavy string constraints
Cites work
- scientific article; zbMATH DE number 3577484 (Why is no real title available?)
- A decision procedure for regular membership and length constraints over unbounded strings
- An efficient algorithm for solving word equations
- Automata-based model counting for string constraints
- Derivatives of Regular Expressions
- Makanin's algorithm for word equations-two improvements and a generalization
- Path Feasibility Analysis for String-Manipulating Programs
- Progressive reasoning over recursively-defined strings
- Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
- Satisfiability of word equations with constants is in PSPACE
- 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 satisfiability of word equations: decidable and undecidable theories
Cited in
(9)- String theories involving regular membership predicates: from practice to theory and back
- A closer look at the expressive power of logics based on word equations
- Towards more efficient methods for solving regular-expression heavy string constraints
- Word equations in synergy with regular constraints
- Incremental dead state detection in logarithmic time
- Solving string constraints using SAT
- Verified verifying: SMT-LIB for strings in Isabelle
- Solving String Theories Involving Regular Membership Predicates Using SAT
- Z3str2: an efficient solver for strings, regular expressions, and length constraints
Describes a project that uses
Uses Software
This page was built for publication: An SMT solver for regular expressions and linear arithmetic over string length
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832270)
