Detail publikace

Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation

CHOCHOLATÝ David, HAVLENA Vojtěch, HOLÍK Lukáš, HRANIČKA Jan, LENGÁL Ondřej a SÍČ Juraj. Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation. In: Proceedings of TACAS'25. Hamilton: Springer Verlag, 2025, s. 22. ISSN 0302-9743.
Název česky
Z3-Noodler 1.3: Navádění rozhodovacích procedur pro řetězce s generováním modelu
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Chocholatý David, Ing. (UITS FIT VUT)
Havlena Vojtěch, Ing., Ph.D. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Hranička Jan, Bc. (FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Síč Juraj, Mgr. (UITS FIT VUT)
Klíčová slova

SMT, řetězcová omezení, nudlifikace, automaty, řešič SMT

Abstrakt

Tento článek přináší nástroj Z3-Noodler, řetězcový řešič založený na automatech, odvozený z nástroje Z3, nyní s podporou generování modelu a výběru vhodné rozhodovací procedury.

Rok
2025 (v tisku)
Strany
22
Časopis
Lecture Notes in Computer Science, ISSN 0302-9743
Sborník
Proceedings of TACAS'25
Konference
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems --- TACAS'25, Hamilton, CA
Vydavatel
Springer Verlag
Místo
Hamilton, CA
BibTeX 
@INPROCEEDINGS{FITPUB13351,
   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",
   pages = 22,
   booktitle = "Proceedings of TACAS'25",
   journal = "Lecture Notes in Computer Science",
   year = 2025,
   location = "Hamilton, CA",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/13351"
}
Nahoru