Result Details
Z3-Noodler: A String Solver
Created: 2024
Type
software
Language
English
Authors
Havlena Vojtěch, Ing., Ph.D., DITS (FIT)
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Chocholatý David, Ing., FIT (FIT), DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Síč Juraj, Mgr., DITS (FIT)
Chen Yu-Fang
Holík Lukáš, doc. Mgr., Ph.D., DITS (FIT)
Chocholatý David, Ing., FIT (FIT), DITS (FIT)
Lengál Ondřej, doc. Ing., Ph.D., DITS (FIT)
Síč Juraj, Mgr., DITS (FIT)
Chen Yu-Fang
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.
Keywords
string solving
noodlification
automata
URL
License
Use of the result by another entity is possible without acquiring a license (the result is not licensed)
License Fee
The licensor does not require a license fee for the result
License Conditions
Open source software under the MIT license https://raw.githubusercontent.com/vhavlena/ranker/master/LICENSE
Projects
Efficient Finite Automata for Automated Reasoning, MŠMT, ERC CZ, LL1908, start: 2020-01-01, end: 2024-12-31, completed
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running
Representing Boolean Functions by a Self-Adaptable Data Structure, GACR, Standardní projekty, GA23-07565S, start: 2023-01-01, end: 2025-12-31, running
Reliable, Secure, and Intelligent Computer Systems, BUT, Vnitřní projekty VUT, FIT-S-23-8151, start: 2023-03-01, end: 2026-02-28, running
Representing Boolean Functions by a Self-Adaptable Data Structure, GACR, Standardní projekty, GA23-07565S, start: 2023-01-01, end: 2025-12-31, running
Research groups
Automata@FIT (RG Automata@FIT)
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments