Product Details
Z3-Noodler: A String Solver
Created: 2024
Czech title
Z3-Noodler: Řetězcový Řešič
Type
software
License
no - free
Authors
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Chocholatý David, Ing. (FIT BUT)
Lengál Ondřej, doc. Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Chen Yu-Fang (ASIN)
Chocholatý David, Ing. (FIT BUT)
Lengál Ondřej, doc. Ing., Ph.D. (DITS FIT BUT)
Síč Juraj, Mgr. (DITS FIT BUT)
Keywords
string solving
noodlification
automata
Description
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.
Location
Licence
Open source software under the MIT license https://raw.githubusercontent.com/vhavlena/ranker/master/LICENSE
Projects
Efficient Finite Automata for Automated Reasoning (LL1908)
Reliable, Secure, and Intelligent Computer Systems (FIT-S-23-8151)
Representing Boolean Functions by a Self-Adaptable Data Structure (GA23-07565S)
Reliable, Secure, and Intelligent Computer Systems (FIT-S-23-8151)
Representing Boolean Functions by a Self-Adaptable Data Structure (GA23-07565S)
Research groups
Automata@FIT (VZ Automata@FIT)
Automated Analysis and Verification Research Group - VeriFIT (VZ VERIFIT)
Automated Analysis and Verification Research Group - VeriFIT (VZ VERIFIT)
Departments
Department of Intelligent Systems FIT BUT (DITS FIT BUT)