Z3-Noodler: A String Solver

Z3-Noodler: Řetězcový Řešič

software

Use of the result by another entity is possible without acquiring a license (the result is not licensed)

The licensor does not require a license fee for the result

Havlena Vojtěch, Ing., Ph.D. (DITS)
Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Chocholatý David, Ing. (DITS)
Lengál Ondřej, Ing., Ph.D. (DITS)
Síč Juraj, Mgr. (DITS)
Chen Yu-Fang

string solving noodlification automata

Z3-Noodler is a fork of the SMT solver Z3, replacing its string theory solver with a custom solver implementing the recently introduced stabilization-based algorithm for solving word equations with regular constraints.

https://github.com/VeriFIT/z3-noodler

Open source software under the MIT license https://raw.githubusercontent.com/vhavlena/ranker/master/LICENSE

Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, 2020-2024, running
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, 2023-2026, running
Representing Boolean Functions by a Self-Adaptable Data Structure, GACR, Standardní projekty, GA23-07565S, 2023-2025, running

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)