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

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

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

Publication date: 25 March 2022

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

zbMATH Keywords

regular expressions; SMT solvers; string solvers

Mathematics Subject Classification ID

68Q45: Formal languages and automata

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

68W32: Algorithms on strings

68V20: Formalization of mathematics in connection with theorem provers

Uses Software

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