An automata-based SMT solver for string constraints
Home · Installation · Usage · Publications · Playground
If you use Z3-Noodler in your work, please cite the tool paper:
Y.-F. Chen, D. Chocholatý, V. Havlena, L. Holík, O. Lengál and J. Síč. Z3-Noodler: An Automata-based String Solver. In Proc. of TACAS’24, volume 14570 of LNCS, pages 24-33, 2024. Springer.
@inproceedings{z3noodler-tacas24,
author = {Yu-Fang Chen and David Chocholat{\'y} and Vojt{\v{e}}ch Havlena and Luk{\'a}{\v{s}} Hol{\'i}k and Ond{\v{r}}ej Leng{\'a}l and Juraj S{\'i}{\v{c}}},
title = {{Z3-Noodler}: An Automata-based String Solver},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2024)},
editor = {Bernd Finkbeiner and Laura Kov{\'a}cs},
series = {Lecture Notes in Computer Science},
volume = {14570},
pages = {24--33},
publisher = {Springer},
year = {2024},
doi = {10.1007/978-3-031-57246-3_2}
}
For the current version of Z3-Noodler, with its portfolio of decision procedures and model generation, please also cite:
D. Chocholatý, V. Havlena, L. Holík, J. Hranička, O. Lengál and J. Síč. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. In Proc. of TACAS’25, volume 15697 of LNCS, pages 23-44, 2025. Springer.
@inproceedings{z3noodler13-tacas25,
author = {David Chocholat{\'y} and Vojt{\v{e}}ch Havlena and Luk{\'a}{\v{s}} Hol{\'i}k and Jan Hrani{\v{c}}ka and Ond{\v{r}}ej Leng{\'a}l and Juraj S{\'i}{\v{c}}},
title = {{Z3-Noodler} 1.3: Shepherding Decision Procedures for Strings with Model Generation},
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025)},
editor = {Arie Gurfinkel and Marijn Heule},
series = {Lecture Notes in Computer Science},
volume = {15697},
pages = {23--44},
publisher = {Springer},
year = {2025},
doi = {10.1007/978-3-031-90653-4_2}
}
The automata library behind Z3-Noodler:
Short overviews of the solver as it entered the SMT competition: 2026, 2025, 2024, 2023.
@inproceedings{transducers-cav26,
author = {David Chocholat{\'y} and Vojt{\v{e}}ch Havlena and Luk{\'a}{\v{s}} Hol{\'i}k and Juraj S{\'i}{\v{c}} and Michal {\v{S}}ed{\'y}},
title = {String Solving with Stabilization and Transducers},
booktitle = {Computer Aided Verification (CAV 2026)},
editor = {Eva Darulova and Anthony W. Lin and Philipp R{\"u}mmer},
series = {Lecture Notes in Computer Science},
volume = {16683},
pages = {50--74},
publisher = {Springer},
year = {2026},
doi = {10.1007/978-3-032-32526-6_3}
}
@article{position-pldi25,
author = {Yu-Fang Chen and Vojt{\v{e}}ch Havlena and Michal He{\v{c}}ko and Luk{\'a}{\v{s}} Hol{\'i}k and Ond{\v{r}}ej Leng{\'a}l},
title = {A Uniform Framework for Handling Position Constraints in String Solving},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
pages = {550--575},
year = {2025},
publisher = {ACM},
doi = {10.1145/3729273}
}
@inproceedings{conversions-sat24,
author = {Vojt{\v{e}}ch Havlena and Luk{\'a}{\v{s}} Hol{\'i}k and Ond{\v{r}}ej Leng{\'a}l and Juraj S{\'i}{\v{c}}},
title = {Cooking String-Integer Conversions with Noodles},
booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {305},
pages = {14:1--14:19},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
year = {2024},
doi = {10.4230/LIPIcs.SAT.2024.14}
}
@article{stabilization-oopsla23,
author = {Yu-Fang Chen and David Chocholat{\'y} and Vojt{\v{e}}ch Havlena and Luk{\'a}{\v{s}} Hol{\'i}k and Ond{\v{r}}ej Leng{\'a}l and Juraj S{\'i}{\v{c}}},
title = {Solving String Constraints with Lengths by Stabilization},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
pages = {2112--2141},
year = {2023},
publisher = {ACM},
doi = {10.1145/3622872}
}
@inproceedings{synergy-fm23,
author = {Franti{\v{s}}ek Blahoudek and Yu-Fang Chen and David Chocholat{\'y} and Vojt{\v{e}}ch Havlena and Luk{\'a}{\v{s}} Hol{\'i}k and Ond{\v{r}}ej Leng{\'a}l and Juraj S{\'i}{\v{c}}},
title = {Word Equations in Synergy with Regular Constraints},
booktitle = {Formal Methods (FM 2023)},
editor = {Marsha Chechik and Joost-Pieter Katoen and Martin Leucker},
series = {Lecture Notes in Computer Science},
volume = {14000},
pages = {403--423},
publisher = {Springer},
year = {2023},
doi = {10.1007/978-3-031-27481-7_23}
}