An SMT solver for regular expressions and linear arithmetic over string length

DOI10.1007/978-3-030-81688-9_14zbMath1493.68182arXiv2010.07253OpenAlexW3186328512MaRDI QIDQ832270

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

Publication date: 25 March 2022

Full work available at URL: https://arxiv.org/abs/2010.07253

zbMATH Keywords

regular expressionsSMT solversstring solvers

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Algorithms on strings (68W32) Formalization of mathematics in connection with theorem provers (68V20)

Related Items

String theories involving regular membership predicates: from practice to theory and back, Towards more efficient methods for solving regular-expression heavy string constraints, Word equations in synergy with regular constraints, Verified verifying: SMT-LIB for strings in Isabelle

Uses Software

• SMT-LIB
• z3
• Stranger
• CVC4
• HAMPI
• GitHub
• Jalangi
• Z3str3
• Z3str2
• StringFuzz

Cites Work

• Unnamed Item
• Automata-based model counting for string constraints
• The satisfiability of word equations: decidable and undecidable theories
• String theories involving regular membership predicates: from practice to theory and back
• String solving with word equations and transducers: towards a logic for analysing mutation XSS
• An efficient algorithm for solving word equations
• A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings
• Satisfiability of word equations with constants is in PSPACE
• Path Feasibility Analysis for String-Manipulating Programs
• Progressive Reasoning over Recursively-Defined Strings
• Derivatives of Regular Expressions
• Quadratic word equations with length constraints, counter systems, and Presburger arithmetic with divisibility
• Makanin's algorithm for word equations-two improvements and a generalization