An SMT solver for regular expressions and linear arithmetic over string length
From MaRDI portal
Publication:832270
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
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 (4)
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
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
This page was built for publication: An SMT solver for regular expressions and linear arithmetic over string length
