PICoSo: An SMT Solver for String Constraints

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F19%3APR32651" target="_blank" >RIV/00216305:26230/19:PR32651 - isvavai.cz</a>
Result on the web
<a href="https://www.fit.vut.cz/research/product/620/" target="_blank" >https://www.fit.vut.cz/research/product/620/</a>
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
PICoSo: An SMT Solver for String Constraints
Original language description
PICoSo contains an extended decision procedure for the straight-line fragment. In contrast to Sloth, PICoSo is able to solve constraints combining concatenation, regular expressions, transduction and length constraints. PICoSo uses a refined version of the Parikh image abstraction of finite automata to resolve string length constraints.
Czech name
—
Czech description
—

Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2019
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Internal product ID
PICoSo
Technical parameters
Pro informace o licenčních podmínkách prosím kontaktujte: Mgr. Radka Báčová, Výzkumné centrum informačních technologií, Fakulta informačních technologií VUT v Brně, Božetěchova 2, 612 66 Brno, 541 141 473.
Economical parameters
Software je volně dostupný včetně zdrojových textů.
Owner IČO
—
Owner name
Fakulta informačních technologií

Similar results(10)