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, Bc. (FIT BUT)
Lengál Ondřej, 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, Bc. (FIT BUT)
Lengál Ondřej, 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)